Group :: Engineering
RPM: yosys
Navigation
Main Changelog Spec Patches Sources Download Gear Bugs and FR Repocop
Patch: yosys-0.32-alt1.patch
Download
Download
yosys-config.1 | 53 +++++++++++++++++++++++
yosys-filterlib.1 | 48 +++++++++++++++++++++
yosys-smtbmc.1 | 64 +++++++++++++++++++++++++++
yosys.1 | 126 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
4 files changed, 291 insertions(+)
diff --git a/yosys-config.1 b/yosys-config.1
new file mode 100644
index 000000000..f8d45b1bc
--- /dev/null
+++ b/yosys-config.1
@@ -0,0 +1,53 @@
+.\" Hey, EMACS: -*- nroff -*-
+.\" First parameter, NAME, should be all caps
+.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
+.\" other parameters are allowed: see man(7), man(1)
+.TH YOSYS-CONFIG 1 "October 16, 2014"
+.\" Please adjust this date whenever revising the manpage.
+.\"
+.\" Some roff macros, for reference:
+.\" .nh disable hyphenation
+.\" .hy enable hyphenation
+.\" .ad l left justify
+.\" .ad b justify to both left and right margins
+.\" .nf disable filling
+.\" .fi enable filling
+.\" .br insert line break
+.\" .sp <n> insert n+1 empty lines
+.\" for manpage-specific macros, see man(7)
+.SH NAME
+yosys-config \- Yosys Open SYnthesis Suite Config
+.SH SYNOPSIS
+.B yosys-config
+.RI "[ -exec ] [ --prefix pf ]" " args"
+.br
+.SH DESCRIPTION
+This manual page documents briefly the
+.B yosys-config
+command.
+.PP
+.\" TeX users may be more comfortable with the \fB<whatever>\fP and
+.\" \fI<whatever>\fP escape sequences to invode bold face and italics,
+.\" respectively.
+\fByosys-config\fP is a shell script which can be used to query compiler options and other information needed for building loadable modules for yosys. It is similar in behaviour to pkg-config.
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B \-\-cxx
+.TP
+.B \-\-cxxflag
+.TP
+.B \-\-ldflags
+.TP
+.B \-\-ldlibs
+.TP
+.B \-\-bindir
+.TP
+.B \-\-datdir
+.SH SEE ALSO
+yosys(1), yosys-filterlib(1)
+.SH AUTHOR
+yosys-config was written by Clifford Wolf <clifford@clifford.at>.
+.PP
+This manual page was written by Ruben Undheim <ruben.undheim@gmail.com>,
+for the Debian project (and may be used by others).
diff --git a/yosys-filterlib.1 b/yosys-filterlib.1
new file mode 100644
index 000000000..457159e7a
--- /dev/null
+++ b/yosys-filterlib.1
@@ -0,0 +1,48 @@
+.\" Hey, EMACS: -*- nroff -*-
+.\" First parameter, NAME, should be all caps
+.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
+.\" other parameters are allowed: see man(7), man(1)
+.TH YOSYS-FILTERLIB 1 "October 16, 2014"
+.\" Please adjust this date whenever revising the manpage.
+.\"
+.\" Some roff macros, for reference:
+.\" .nh disable hyphenation
+.\" .hy enable hyphenation
+.\" .ad l left justify
+.\" .ad b justify to both left and right margins
+.\" .nf disable filling
+.\" .fi enable filling
+.\" .br insert line break
+.\" .sp <n> insert n+1 empty lines
+.\" for manpage-specific macros, see man(7)
+.SH NAME
+yosys-filterlib \- Yosys Open SYnthesis Suite Filterlib
+.SH SYNOPSIS
+.B yosys-filterlib
+.RI "[ rules-files [liberty-file]]"
+.br
+.SH DESCRIPTION
+This manual page documents briefly the
+.B yosys-filterlib
+command.
+.PP
+.\" TeX users may be more comfortable with the \fB<whatever>\fP and
+.\" \fI<whatever>\fP escape sequences to invode bold face and italics,
+.\" respectively.
+\fByosys-filterlib\fP is a program used to strip sensitive information from Liberty files.
+
+Occasionally Liberty files contain trade secrets (such as sensitive timing information) that cannot be shared
+freely. This complicates processes such as reporting bugs in the tools involved. When the information in
+the Liberty file used by Yosys and ABC are not part of the sensitive information, this tool
+yosys-filterlib can be used to strip the sensitive information from the Liberty file.
+.\".SH OPTIONS
+.\"A summary of options is included below.
+.\"#.TP
+.\"a
+.SH SEE ALSO
+yosys(1), yosys-config(1)
+.SH AUTHOR
+yosys-filterlib was written by Clifford Wolf <clifford@clifford.at>.
+.PP
+This manual page was written by Ruben Undheim <ruben.undheim@gmail.com>,
+for the Debian project (and may be used by others).
diff --git a/yosys-smtbmc.1 b/yosys-smtbmc.1
new file mode 100644
index 000000000..7eda1a11a
--- /dev/null
+++ b/yosys-smtbmc.1
@@ -0,0 +1,64 @@
+.\" Text automatically generated by txt2man
+.TH YOSYS-SMTBMC 1 "06 November 2016" "" ""
+.SH NAME
+\fByosys-smtbmc \fP- write design to SMT2-LIBv2 file
+\fB
+.SH SYNOPSIS
+.nf
+.fam C
+\fByosys-smtbmc\fP [\fIoptions\fP] <yosys_smt2_output>
+
+.fam T
+.fi
+.fam T
+.fi
+.SH OPTIONS
+
+.TP
+.B
+\fB-t\fP [<skip_steps>:]<num_steps>
+default: skip_steps=0, num_steps=20
+.TP
+.B
+\fB-u\fP <start_step>
+assume asserts in skipped steps in BMC
+.TP
+.B
+\fB-S\fP <step_size>
+proof <step_size> time steps at once
+.TP
+.B
+\fB-c\fP <vcd_filename>
+write counter-example to this VCD file (hint: use 'write_smt2
+\fB-wires\fP' for maximum coverage of signals in generated VCD file)
+.TP
+.B
+\fB-i\fP
+instead of BMC run temporal induction
+.TP
+.B
+\fB-m\fP <module_name>
+name of the top module
+.TP
+.B
+\fB-s\fP <solver>
+Set SMT solver: z3, cvc4, yices, mathsat. default: z3
+.TP
+.B
+\fB-v\fP
+enable debug output
+.TP
+.B
+\fB-p\fP
+disable timer display during solving
+.TP
+.B
+\fB-d\fP <filename>
+write smt2 statements to file
+.RE
+.PP
+
+.SH AUTHOR
+
+This manual page was written by Sebastian Kuzminsky <seb@highlab.com>
+for the Debian project (and may be used by others).
diff --git a/yosys.1 b/yosys.1
new file mode 100644
index 000000000..fbfb0aa0a
--- /dev/null
+++ b/yosys.1
@@ -0,0 +1,126 @@
+.\" Hey, EMACS: -*- nroff -*-
+.\" First parameter, NAME, should be all caps
+.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
+.\" other parameters are allowed: see man(7), man(1)
+.TH YOSYS 1 "November 04, 2016"
+.\" Please adjust this date whenever revising the manpage.
+.\"
+.\" Some roff macros, for reference:
+.\" .nh disable hyphenation
+.\" .hy enable hyphenation
+.\" .ad l left justify
+.\" .ad b justify to both left and right margins
+.\" .nf disable filling
+.\" .fi enable filling
+.\" .br insert line break
+.\" .sp <n> insert n+1 empty lines
+.\" for manpage-specific macros, see man(7)
+.SH NAME
+yosys \- Yosys Open SYnthesis Suite
+.SH SYNOPSIS
+.B yosys
+.RI [ options ] " <infile>"
+.br
+.SH DESCRIPTION
+This manual page documents briefly the
+.B yosys
+command.
+.PP
+.\" TeX users may be more comfortable with the \fB<whatever>\fP and
+.\" \fI<whatever>\fP escape sequences to invode bold face and italics,
+.\" respectively.
+\fByosys\fP is a program that synthesizes RTL to gate-level logic.
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B \-Q
+suppress printing of banner (copyright, disclaimer, version)
+.TP
+.B \-T
+suppress printing of footer (log hash, version, timing statistics)
+.TP
+.B \-q
+quiet operation. only write error message to console
+use this option twice to also quiet warning messages
+.TP
+.B \-v <level>
+print log headers up to level <level> to the console. (implies \-q)
+.TP
+.B \-t
+annotate all log messages with a time stamp
+.TP
+.B \-d
+print more detailed timing stats at exit
+.TP
+.B \-l logfile
+write log messages to the specified file
+.TP
+.B \-L logfile
+like -l but open log file in line buffered mode
+.TP
+.B \-o outfile
+write the design to the specified file on exit
+.TP
+.B \-b backend
+use this backend for the output file specified on the command line
+.TP
+.B \-f frontend
+use the specified frontend for the input files on the command line
+.TP
+.B \-H
+print the command list
+.TP
+.B \-h command
+print the help message for the specified command
+.TP
+.B \-s scriptfile
+execute the commands in the script file
+.TP
+.B \-c tcl_scriptfile
+execute the commands in the tcl script file (see 'help tcl' for details)
+.TP
+.B \-p command
+execute the commands
+.TP
+.B \-m module_file
+load the specified module (aka plugin)
+.TP
+.B \-X
+enable tracing of core data structure changes. for debugging
+.TP
+.B \-M
+will slightly randomize allocated pointer addresses. for debugging
+.TP
+.B \-A
+will call abort() at the end of the script. for debugging
+.TP
+.B \-D <header_id>[:<filename>]
+dump the design when printing the specified log header to a file.
+yosys_dump_<header_id>.il is used as filename if none is specified.
+Use 'ALL' as <header_id> to dump at every header.
+.TP
+.B \-V
+print version information and exit
+.TP
+.B \-S
+The option \-S is an alias for the "synth" command, a default
+script for transforming the Verilog input to a gate-level netlist. For example:
+
+ yosys -o output.blif -S input.v
+
+.SH USAGE
+For more complex synthesis jobs it is recommended to use the read_* and write_*
+commands in a script file instead of specifying input and output files on the
+command line.
+
+When no commands, script files or input files are specified on the command
+line, yosys automatically enters the interactive command mode. Use the 'help'
+command to get information on the individual commands.
+
+.SH SEE ALSO
+berkeley-abc(1), yosys-config(1), yosys-filterlib(1)
+.SH AUTHOR
+yosys was written by Clifford Wolf <clifford@clifford.at>.
+.PP
+This manual page was written by Ruben Undheim <ruben.undheim@gmail.com>,
+for the Debian project (and may be used by others).