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 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\fP and +.\" \fI\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 . +.PP +This manual page was written by Ruben Undheim , +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 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\fP and +.\" \fI\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 . +.PP +This manual page was written by Ruben Undheim , +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] + +.fam T +.fi +.fam T +.fi +.SH OPTIONS + +.TP +.B +\fB-t\fP [:] +default: skip_steps=0, num_steps=20 +.TP +.B +\fB-u\fP +assume asserts in skipped steps in BMC +.TP +.B +\fB-S\fP +proof time steps at once +.TP +.B +\fB-c\fP +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 +name of the top module +.TP +.B +\fB-s\fP +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 +write smt2 statements to file +.RE +.PP + +.SH AUTHOR + +This manual page was written by Sebastian Kuzminsky +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 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 ] " " +.br +.SH DESCRIPTION +This manual page documents briefly the +.B yosys +command. +.PP +.\" TeX users may be more comfortable with the \fB\fP and +.\" \fI\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 +print log headers up to 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 [:] +dump the design when printing the specified log header to a file. +yosys_dump_.il is used as filename if none is specified. +Use 'ALL' as 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 . +.PP +This manual page was written by Ruben Undheim , +for the Debian project (and may be used by others).