diff options
Diffstat (limited to 'manual/command-reference-manual.tex')
-rw-r--r-- | manual/command-reference-manual.tex | 9592 |
1 files changed, 0 insertions, 9592 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex deleted file mode 100644 index 62183801d..000000000 --- a/manual/command-reference-manual.tex +++ /dev/null @@ -1,9592 +0,0 @@ -% Generated using the yosys 'help -write-tex-command-reference-manual' command. - -\section{abc -- use ABC for technology mapping} -\label{cmd:abc} -\begin{lstlisting}[numbers=left,frame=single] - abc [options] [selection] - -This pass uses the ABC tool [1] for technology mapping of yosys's internal gate -library to a target architecture. - - -exe <command> - use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script <file> - use the specified ABC script file instead of the default script. - - if <file> starts with a plus sign (+), then the rest of the filename - string is interpreted as the command string to be passed to ABC. The - leading plus sign is removed and all commas (,) in the string are - replaced with blanks before the string is passed to ABC. - - if no -script parameter is given, the following scripts are used: - - for -liberty/-genlib without -constr: - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - &get -n; &dch -f; &nf {D}; &put - - for -liberty/-genlib with -constr: - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; - dnsize {D}; stime -p - - for -lut/-luts (only one LUT size): - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - dch -f; if; mfs2; lutpack {S} - - for -lut/-luts (different LUT sizes): - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - dch -f; if; mfs2 - - for -sop: - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - dch -f; cover {I} {P} - - otherwise: - strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; - &get -n; &dch -f; &nf {D}; &put - - -fast - use different default scripts that are slightly faster (at the cost - of output quality): - - for -liberty/-genlib without -constr: - strash; dretime; map {D} - - for -liberty/-genlib with -constr: - strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; - stime -p - - for -lut/-luts: - strash; dretime; if - - for -sop: - strash; dretime; cover {I} {P} - - otherwise: - strash; dretime; map - - -liberty <file> - generate netlists for the specified cell library (using the liberty - file format). - - -genlib <file> - generate netlists for the specified cell library (using the SIS Genlib - file format). - - -constr <file> - pass this file with timing constraints to ABC. - use with -liberty/-genlib. - - a constr file contains two lines: - set_driving_cell <cell_name> - set_load <floating_point_number> - - the set_driving_cell statement defines which cell type is assumed to - drive the primary inputs and the set_load statement sets the load in - femtofarads for each primary output. - - -D <picoseconds> - set delay target. the string {D} in the default scripts above is - replaced by this option when used, and an empty string otherwise. - this also replaces 'dretime' with 'dretime; retime -o {D}' in the - default scripts above. - - -I <num> - maximum number of SOP inputs. - (replaces {I} in the default scripts above) - - -P <num> - maximum number of SOP products. - (replaces {P} in the default scripts above) - - -S <num> - maximum number of LUT inputs shared. - (replaces {S} in the default scripts above, default: -S 1) - - -lut <width> - generate netlist using luts of (max) the specified width. - - -lut <w1>:<w2> - generate netlist using luts of (max) the specified width <w2>. All - luts with width <= <w1> have constant cost. for luts larger than <w1> - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,.. - generate netlist using luts. Use the specified costs for luts with 1, - 2, 3, .. inputs. - - -sop - map to sum-of-product cells and inverters - - -g type1,type2,... - Map to the specified list of gate types. Supported gates types are: - AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX, - NMUX, AOI3, OAI3, AOI4, OAI4. - (The NOT gate is always added to this list automatically.) - - The following aliases can be used to reference common sets of gate - types: - simple: AND OR XOR MUX - cmos2: NAND NOR - cmos3: NAND NOR AOI3 OAI3 - cmos4: NAND NOR AOI3 OAI3 AOI4 OAI4 - cmos: NAND NOR AOI3 OAI3 AOI4 OAI4 NMUX MUX XOR XNOR - gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT - aig: AND NAND OR NOR ANDNOT ORNOT - - The alias 'all' represent the full set of all gate types. - - Prefix a gate type with a '-' to remove it from the list. For example - the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent. - - The default is 'all,-NMUX,-AOI3,-OAI3,-AOI4,-OAI4'. - - -dff - also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many - clock domains are automatically partitioned in clock domains and each - domain is passed through ABC independently. - - -clk [!]<clock-signal-name>[,[!]<enable-signal-name>] - use only the specified clock domain. this is like -dff, but only FF - cells that belong to the specified clock domain are used. - - -keepff - set the "keep" attribute on flip-flop output wires. (and thus preserve - them, for example for equivalence checking.) - - -nocleanup - when this option is used, the temporary files created by this pass - are not removed. this is useful for debugging. - - -showtmp - print the temp dir name in log. usually this is suppressed so that the - command output is identical across runs. - - -markgroups - set a 'abcgroup' attribute on all objects created by ABC. The value of - this attribute is a unique integer for each ABC process started. This - is useful for debugging the partitioning of clock domains. - - -dress - run the 'dress' command after all other ABC commands. This aims to - preserve naming by an equivalence check between the original and - post-ABC netlists (experimental). - -When no target cell library is specified the Yosys standard cell library is -loaded into ABC before the ABC script is executed. - -Note that this is a logic optimization pass within Yosys that is calling ABC -internally. This is not going to "run ABC on your design". It will instead run -ABC on logic snippets extracted from your design. You will not get any useful -output when passing an ABC script that writes a file. Instead write your full -design as BLIF file with write_blif and then load that into ABC externally if -you want to use ABC to convert your design into another format. - -[1] http://www.eecs.berkeley.edu/~alanmi/abc/ -\end{lstlisting} - -\section{abc9 -- use ABC9 for technology mapping} -\label{cmd:abc9} -\begin{lstlisting}[numbers=left,frame=single] - abc9 [options] [selection] - -This script pass performs a sequence of commands to facilitate the use of the -ABC tool [1] for technology mapping of the current design to a target FPGA -architecture. Only fully-selected modules are supported. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -exe <command> - use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script <file> - use the specified ABC script file instead of the default script. - - if <file> starts with a plus sign (+), then the rest of the filename - string is interpreted as the command string to be passed to ABC. The - leading plus sign is removed and all commas (,) in the string are - replaced with blanks before the string is passed to ABC. - - if no -script parameter is given, the following scripts are used: - &scorr; &sweep; &dc2; &dch -f; &ps; &if {C} {W} {D} {R} -v; &mfs - - -fast - use different default scripts that are slightly faster (at the cost - of output quality): - &if {C} {W} {D} {R} -v - - -D <picoseconds> - set delay target. the string {D} in the default scripts above is - replaced by this option when used, and an empty string otherwise - (indicating best possible delay). - - -lut <width> - generate netlist using luts of (max) the specified width. - - -lut <w1>:<w2> - generate netlist using luts of (max) the specified width <w2>. All - luts with width <= <w1> have constant cost. for luts larger than <w1> - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -lut <file> - pass this file with lut library to ABC. - - -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,.. - generate netlist using luts. Use the specified costs for luts with 1, - 2, 3, .. inputs. - - -maxlut <width> - when auto-generating the lut library, discard all luts equal to or - greater than this size (applicable when neither -lut nor -luts is - specified). - - -dff - also pass $_DFF_[NP]_ cells through to ABC. modules with many clock - domains are supported and automatically partitioned by ABC. - - -nocleanup - when this option is used, the temporary files created by this pass - are not removed. this is useful for debugging. - - -showtmp - print the temp dir name in log. usually this is suppressed so that the - command output is identical across runs. - - -box <file> - pass this file with box library to ABC. - -Note that this is a logic optimization pass within Yosys that is calling ABC -internally. This is not going to "run ABC on your design". It will instead run -ABC on logic snippets extracted from your design. You will not get any useful -output when passing an ABC script that writes a file. Instead write your full -design as an XAIGER file with `write_xaiger' and then load that into ABC -externally if you want to use ABC to convert your design into another format. - -[1] http://www.eecs.berkeley.edu/~alanmi/abc/ - - - check: - abc9_ops -check [-dff] (option if -dff) - - map: - abc9_ops -prep_hier [-dff] (option if -dff) - scc -specify -set_attr abc9_scc_id {} - abc9_ops -prep_bypass [-prep_dff] (option if -dff) - design -stash $abc9 - design -load $abc9_map - proc - wbflip - techmap -wb -map %$abc9 -map +/techmap.v A:abc9_flop - opt -nodffe -nosdff - abc9_ops -prep_dff_submod (only if -dff) - setattr -set submod "$abc9_flop" t:$_DFF_?_ %ci* %co* t:$_DFF_?_ %d (only if -dff) - submod (only if -dff) - setattr -mod -set whitebox 1 -set abc9_flop 1 -set abc9_box 1 *_$abc9_flop (only if -dff) - foreach module in design - rename <module-name>_$abc9_flop _TECHMAP_REPLACE_ (only if -dff) - abc9_ops -prep_dff_unmap (only if -dff) - design -copy-to $abc9 =*_$abc9_flop (only if -dff) - delete =*_$abc9_flop (only if -dff) - design -stash $abc9_map - design -load $abc9 - design -delete $abc9 - techmap -wb -max_iter 1 -map %$abc9_map -map +/abc9_map.v [-D DFF] (option if -dff) - design -delete $abc9_map - - pre: - read_verilog -icells -lib -specify +/abc9_model.v - abc9_ops -break_scc -prep_delays -prep_xaiger [-dff] (option for -dff) - abc9_ops -prep_lut <maxlut> (skip if -lut or -luts) - abc9_ops -prep_box (skip if -box) - design -stash $abc9 - design -load $abc9_holes - techmap -wb -map %$abc9 -map +/techmap.v - opt -purge - aigmap - design -stash $abc9_holes - design -load $abc9 - design -delete $abc9 - - exe: - aigmap - foreach module in selection - abc9_ops -write_lut <abc-temp-dir>/input.lut (skip if '-lut' or '-luts') - abc9_ops -write_box <abc-temp-dir>/input.box (skip if '-box') - write_xaiger -map <abc-temp-dir>/input.sym [-dff] <abc-temp-dir>/input.xaig - abc9_exe [options] -cwd <abc-temp-dir> -lut [<abc-temp-dir>/input.lut] -box [<abc-temp-dir>/input.box] - read_aiger -xaiger -wideports -module_name <module-name>$abc9 -map <abc-temp-dir>/input.sym <abc-temp-dir>/output.aig - abc9_ops -reintegrate [-dff] - - unmap: - techmap -wb -map %$abc9_unmap -map +/abc9_unmap.v - design -delete $abc9_unmap - design -delete $abc9_holes - delete =*_$abc9_byp - setattr -mod -unset abc9_box_id -\end{lstlisting} - -\section{abc9\_exe -- use ABC9 for technology mapping} -\label{cmd:abc9_exe} -\begin{lstlisting}[numbers=left,frame=single] - abc9_exe [options] - - -This pass uses the ABC tool [1] for technology mapping of the top module -(according to the (* top *) attribute or if only one module is currently -selected) to a target FPGA architecture. - - -exe <command> - use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script <file> - use the specified ABC script file instead of the default script. - - if <file> starts with a plus sign (+), then the rest of the filename - string is interpreted as the command string to be passed to ABC. The - leading plus sign is removed and all commas (,) in the string are - replaced with blanks before the string is passed to ABC. - - if no -script parameter is given, the following scripts are used: - &scorr; &sweep; &dc2; &dch -f; &ps; &if {C} {W} {D} {R} -v; &mfs - - -fast - use different default scripts that are slightly faster (at the cost - of output quality): - &if {C} {W} {D} {R} -v - - -D <picoseconds> - set delay target. the string {D} in the default scripts above is - replaced by this option when used, and an empty string otherwise - (indicating best possible delay). - - -lut <width> - generate netlist using luts of (max) the specified width. - - -lut <w1>:<w2> - generate netlist using luts of (max) the specified width <w2>. All - luts with width <= <w1> have constant cost. for luts larger than <w1> - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -lut <file> - pass this file with lut library to ABC. - - -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,.. - generate netlist using luts. Use the specified costs for luts with 1, - 2, 3, .. inputs. - - -showtmp - print the temp dir name in log. usually this is suppressed so that the - command output is identical across runs. - - -box <file> - pass this file with box library to ABC. - - -cwd <dir> - use this as the current working directory, inside which the 'input.xaig' - file is expected. temporary files will be created in this directory, and - the mapped result will be written to 'output.aig'. - -Note that this is a logic optimization pass within Yosys that is calling ABC -internally. This is not going to "run ABC on your design". It will instead run -ABC on logic snippets extracted from your design. You will not get any useful -output when passing an ABC script that writes a file. Instead write your full -design as BLIF file with write_blif and then load that into ABC externally if -you want to use ABC to convert your design into another format. - -[1] http://www.eecs.berkeley.edu/~alanmi/abc/ -\end{lstlisting} - -\section{abc9\_ops -- helper functions for ABC9} -\label{cmd:abc9_ops} -\begin{lstlisting}[numbers=left,frame=single] - abc9_ops [options] [selection] - -This pass contains a set of supporting operations for use during ABC technology -mapping, and is expected to be called in conjunction with other operations from -the `abc9' script pass. Only fully-selected modules are supported. - - -check - check that the design is valid, e.g. (* abc9_box_id *) values are - unique, (* abc9_carry *) is only given for one input/output port, etc. - - -prep_hier - derive all used (* abc9_box *) or (* abc9_flop *) (if -dff option) - whitebox modules. with (* abc9_flop *) modules, only those containing - $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC - limitation -- will be derived. - - -prep_bypass - create techmap rules in the '$abc9_map' and '$abc9_unmap' designs for - bypassing sequential (* abc9_box *) modules using a combinatorial box - (named *_$abc9_byp). bypassing is necessary if sequential elements (e.g. - $dff, $mem, etc.) are discovered inside so that any combinatorial paths - will be correctly captured. this bypass box will only contain ports that - are referenced by a simple path declaration ($specify2 cell) inside a - specify block. - - -prep_dff - select all (* abc9_flop *) modules instantiated in the design and store - in the named selection '$abc9_flops'. - - -prep_dff_submod - within (* abc9_flop *) modules, rewrite all edge-sensitive path - declarations and $setup() timing checks ($specify3 and $specrule cells) - that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port - to the DFF's 'D' port. this is to prepare such specify cells to be moved - into the flop box. - - -prep_dff_unmap - populate the '$abc9_unmap' design with techmap rules for mapping - *_$abc9_flop cells back into their derived cell types (where the rules - created by -prep_hier will then map back to the original cell with - parameters). - - -prep_delays - insert `$__ABC9_DELAY' blackbox cells into the design to account for - certain required times. - - -break_scc - for an arbitrarily chosen cell in each unique SCC of each selected - module (tagged with an (* abc9_scc_id = <int> *) attribute) interrupt - all wires driven by this cell's outputs with a temporary - $__ABC9_SCC_BREAKER cell to break the SCC. - - -prep_xaiger - prepare the design for XAIGER output. this includes computing the - topological ordering of ABC9 boxes, as well as preparing the - '$abc9_holes' design that contains the logic behaviour of ABC9 - whiteboxes. - - -dff - consider flop cells (those instantiating modules marked with - (* abc9_flop *)) during -prep_{delays,xaiger,box}. - - -prep_lut <maxlut> - pre-compute the lut library by analysing all modules marked with - (* abc9_lut=<area> *). - - -write_lut <dst> - write the pre-computed lut library to <dst>. - - -prep_box - pre-compute the box library by analysing all modules marked with - (* abc9_box *). - - -write_box <dst> - write the pre-computed box library to <dst>. - - -reintegrate - for each selected module, re-intergrate the module '<module-name>$abc9' - by first recovering ABC9 boxes, and then stitching in the remaining - primary inputs and outputs. -\end{lstlisting} - -\section{add -- add objects to the design} -\label{cmd:add} -\begin{lstlisting}[numbers=left,frame=single] - add <command> [selection] - -This command adds objects to the design. It operates on all fully selected -modules. So e.g. 'add -wire foo' will add a wire foo to all selected modules. - - - add {-wire|-input|-inout|-output} <name> <width> [selection] - -Add a wire (input, inout, output port) with the given name and width. The -command will fail if the object exists already and has different properties -than the object to be created. - - - add -global_input <name> <width> [selection] - -Like 'add -input', but also connect the signal between instances of the -selected modules. - - - add {-assert|-assume|-live|-fair|-cover} <name1> [-if <name2>] - -Add an $assert, $assume, etc. cell connected to a wire named name1, with its -enable signal optionally connected to a wire named name2 (default: 1'b1). - - - add -mod <name[s]> - -Add module[s] with the specified name[s]. -\end{lstlisting} - -\section{aigmap -- map logic to and-inverter-graph circuit} -\label{cmd:aigmap} -\begin{lstlisting}[numbers=left,frame=single] - aigmap [options] [selection] - -Replace all logic cells with circuits made of only $_AND_ and -$_NOT_ cells. - - -nand - Enable creation of $_NAND_ cells - - -select - Overwrite replaced cells in the current selection with new $_AND_, - $_NOT_, and $_NAND_, cells -\end{lstlisting} - -\section{alumacc -- extract ALU and MACC cells} -\label{cmd:alumacc} -\begin{lstlisting}[numbers=left,frame=single] - alumacc [selection] - -This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu -and $macc cells. -\end{lstlisting} - -\section{anlogic\_eqn -- Anlogic: Calculate equations for luts} -\label{cmd:anlogic_eqn} -\begin{lstlisting}[numbers=left,frame=single] - anlogic_eqn [selection] - -Calculate equations for luts since bitstream generator depends on it. -\end{lstlisting} - -\section{anlogic\_fixcarry -- Anlogic: fix carry chain} -\label{cmd:anlogic_fixcarry} -\begin{lstlisting}[numbers=left,frame=single] - anlogic_fixcarry [options] [selection] - -Add Anlogic adders to fix carry chain if needed. -\end{lstlisting} - -\section{assertpmux -- adds asserts for parallel muxes} -\label{cmd:assertpmux} -\begin{lstlisting}[numbers=left,frame=single] - assertpmux [options] [selection] - -This command adds asserts to the design that assert that all parallel muxes -($pmux cells) have a maximum of one of their inputs enable at any time. - - -noinit - do not enforce the pmux condition during the init state - - -always - usually the $pmux condition is only checked when the $pmux output - is used by the mux tree it drives. this option will deactivate this - additional constraint and check the $pmux condition always. -\end{lstlisting} - -\section{async2sync -- convert async FF inputs to sync circuits} -\label{cmd:async2sync} -\begin{lstlisting}[numbers=left,frame=single] - async2sync [options] [selection] - -This command replaces async FF inputs with sync circuits emulating the same -behavior for when the async signals are actually synchronized to the clock. - -This pass assumes negative hold time for the async FF inputs. For example when -a reset deasserts with the clock edge, then the FF output will still drive the -reset value in the next cycle regardless of the data-in value at the time of -the clock edge. -\end{lstlisting} - -\section{attrmap -- renaming attributes} -\label{cmd:attrmap} -\begin{lstlisting}[numbers=left,frame=single] - attrmap [options] [selection] - -This command renames attributes and/or maps key/value pairs to -other key/value pairs. - - -tocase <name> - Match attribute names case-insensitively and set it to the specified - name. - - -rename <old_name> <new_name> - Rename attributes as specified - - -map <old_name>=<old_value> <new_name>=<new_value> - Map key/value pairs as indicated. - - -imap <old_name>=<old_value> <new_name>=<new_value> - Like -map, but use case-insensitive match for <old_value> when - it is a string value. - - -remove <name>=<value> - Remove attributes matching this pattern. - - -modattr - Operate on module attributes instead of attributes on wires and cells. - -For example, mapping Xilinx-style "keep" attributes to Yosys-style: - - attrmap -tocase keep -imap keep="true" keep=1 \ - -imap keep="false" keep=0 -remove keep=0 -\end{lstlisting} - -\section{attrmvcp -- move or copy attributes from wires to driving cells} -\label{cmd:attrmvcp} -\begin{lstlisting}[numbers=left,frame=single] - attrmvcp [options] [selection] - -Move or copy attributes on wires to the cells driving them. - - -copy - By default, attributes are moved. This will only add - the attribute to the cell, without removing it from - the wire. - - -purge - If no selected cell consumes the attribute, then it is - left on the wire by default. This option will cause the - attribute to be removed from the wire, even if no selected - cell takes it. - - -driven - By default, attriburtes are moved to the cell driving the - wire. With this option set it will be moved to the cell - driven by the wire instead. - - -attr <attrname> - Move or copy this attribute. This option can be used - multiple times. -\end{lstlisting} - -\section{autoname -- automatically assign names to objects} -\label{cmd:autoname} -\begin{lstlisting}[numbers=left,frame=single] - autoname [selection] - -Assign auto-generated public names to objects with private names (the ones -with $-prefix). -\end{lstlisting} - -\section{blackbox -- convert modules into blackbox modules} -\label{cmd:blackbox} -\begin{lstlisting}[numbers=left,frame=single] - blackbox [options] [selection] - -Convert modules into blackbox modules (remove contents and set the blackbox -module attribute). -\end{lstlisting} - -\section{bmuxmap -- transform \$bmux cells to trees of \$mux cells} -\label{cmd:bmuxmap} -\begin{lstlisting}[numbers=left,frame=single] - bmuxmap [selection] - -This pass transforms $bmux cells to trees of $mux cells. -\end{lstlisting} - -\section{bugpoint -- minimize testcases} -\label{cmd:bugpoint} -\begin{lstlisting}[numbers=left,frame=single] - bugpoint [options] [-script <filename> | -command "<command>"] - -This command minimizes the current design that is known to crash Yosys with the -given script into a smaller testcase. It does this by removing an arbitrary part -of the design and recursively invokes a new Yosys process with this modified -design and the same script, repeating these steps while it can find a smaller -design that still causes a crash. Once this command finishes, it replaces the -current design with the smallest testcase it was able to produce. -In order to save the reduced testcase you must write this out to a file with -another command after `bugpoint` like `write_rtlil` or `write_verilog`. - - -script <filename> | -command "<command>" - use this script file or command to crash Yosys. required. - - -yosys <filename> - use this Yosys binary. if not specified, `yosys` is used. - - -grep "<string>" - only consider crashes that place this string in the log file. - - -fast - run `proc_clean; clean -purge` after each minimization step. converges - faster, but produces larger testcases, and may fail to produce any - testcase at all if the crash is related to dangling wires. - - -clean - run `proc_clean; clean -purge` before checking testcase and after - finishing. produces smaller and more useful testcases, but may fail to - produce any testcase at all if the crash is related to dangling wires. - -It is possible to constrain which parts of the design will be considered for -removal. Unless one or more of the following options are specified, all parts -will be considered. - - -modules - try to remove modules. modules with a (* bugpoint_keep *) attribute - will be skipped. - - -ports - try to remove module ports. ports with a (* bugpoint_keep *) attribute - will be skipped (useful for clocks, resets, etc.) - - -cells - try to remove cells. cells with a (* bugpoint_keep *) attribute will - be skipped. - - -connections - try to reconnect ports to 'x. - - -processes - try to remove processes. processes with a (* bugpoint_keep *) attribute - will be skipped. - - -assigns - try to remove process assigns from cases. - - -updates - try to remove process updates from syncs. - - -runner "<prefix>" - child process wrapping command, e.g., "timeout 30", or valgrind. -\end{lstlisting} - -\section{cd -- a shortcut for 'select -module <name>'} -\label{cmd:cd} -\begin{lstlisting}[numbers=left,frame=single] - cd <modname> - -This is just a shortcut for 'select -module <modname>'. - - - cd <cellname> - -When no module with the specified name is found, but there is a cell -with the specified name in the current module, then this is equivalent -to 'cd <celltype>'. - - - cd .. - -Remove trailing substrings that start with '.' in current module name until -the name of a module in the current design is generated, then switch to that -module. Otherwise clear the current selection. - - - cd - -This is just a shortcut for 'select -clear'. -\end{lstlisting} - -\section{check -- check for obvious problems in the design} -\label{cmd:check} -\begin{lstlisting}[numbers=left,frame=single] - check [options] [selection] - -This pass identifies the following problems in the current design: - - - combinatorial loops - - two or more conflicting drivers for one wire - - used wires that do not have a driver - -Options: - - -noinit - also check for wires which have the 'init' attribute set - - -initdrv - also check for wires that have the 'init' attribute set and are not - driven by an FF cell type - - -mapped - also check for internal cells that have not been mapped to cells of the - target architecture - - -allow-tbuf - modify the -mapped behavior to still allow $_TBUF_ cells - - -assert - produce a runtime error if any problems are found in the current design -\end{lstlisting} - -\section{chformal -- change formal constraints of the design} -\label{cmd:chformal} -\begin{lstlisting}[numbers=left,frame=single] - chformal [types] [mode] [options] [selection] - -Make changes to the formal constraints of the design. The [types] options -the type of constraint to operate on. If none of the following options are -given, the command will operate on all constraint types: - - -assert $assert cells, representing assert(...) constraints - -assume $assume cells, representing assume(...) constraints - -live $live cells, representing assert(s_eventually ...) - -fair $fair cells, representing assume(s_eventually ...) - -cover $cover cells, representing cover() statements - -Exactly one of the following modes must be specified: - - -remove - remove the cells and thus constraints from the design - - -early - bypass FFs that only delay the activation of a constraint - - -delay <N> - delay activation of the constraint by <N> clock cycles - - -skip <N> - ignore activation of the constraint in the first <N> clock cycles - - -assert2assume - -assume2assert - -live2fair - -fair2live - change the roles of cells as indicated. these options can be combined -\end{lstlisting} - -\section{chparam -- re-evaluate modules with new parameters} -\label{cmd:chparam} -\begin{lstlisting}[numbers=left,frame=single] - chparam [ -set name value ]... [selection] - -Re-evaluate the selected modules with new parameters. String values must be -passed in double quotes ("). - - - chparam -list [selection] - -List the available parameters of the selected modules. -\end{lstlisting} - -\section{chtype -- change type of cells in the design} -\label{cmd:chtype} -\begin{lstlisting}[numbers=left,frame=single] - chtype [options] [selection] - -Change the types of cells in the design. - - -set <type> - set the cell type to the given type - - -map <old_type> <new_type> - change cells types that match <old_type> to <new_type> -\end{lstlisting} - -\section{clean -- remove unused cells and wires} -\label{cmd:clean} -\begin{lstlisting}[numbers=left,frame=single] - clean [options] [selection] - -This is identical to 'opt_clean', but less verbose. - -When commands are separated using the ';;' token, this command will be executed -between the commands. - -When commands are separated using the ';;;' token, this command will be executed -in -purge mode between the commands. -\end{lstlisting} - -\section{clean\_zerowidth -- clean zero-width connections from the design} -\label{cmd:clean_zerowidth} -\begin{lstlisting}[numbers=left,frame=single] - clean_zerowidth [selection] - -Fixes the selected cells and processes to contain no zero-width connections. -Depending on the cell type, this may be implemented by removing the connection, -widening it to 1-bit, or removing the cell altogether. -\end{lstlisting} - -\section{clk2fflogic -- convert clocked FFs to generic \$ff cells} -\label{cmd:clk2fflogic} -\begin{lstlisting}[numbers=left,frame=single] - clk2fflogic [options] [selection] - -This command replaces clocked flip-flops with generic $ff cells that use the -implicit global clock. This is useful for formal verification of designs with -multiple clocks. - -This pass assumes negative hold time for the async FF inputs. For example when -a reset deasserts with the clock edge, then the FF output will still drive the -reset value in the next cycle regardless of the data-in value at the time of -the clock edge. -\end{lstlisting} - -\section{clkbufmap -- insert clock buffers on clock networks} -\label{cmd:clkbufmap} -\begin{lstlisting}[numbers=left,frame=single] - clkbufmap [options] [selection] - -Inserts clock buffers between nets connected to clock inputs and their drivers. - -In the absence of any selection, all wires without the 'clkbuf_inhibit' -attribute will be considered for clock buffer insertion. -Alternatively, to consider all wires without the 'buffer_type' attribute set to -'none' or 'bufr' one would specify: - 'w:* a:buffer_type=none a:buffer_type=bufr %u %d' -as the selection. - - -buf <celltype> <portname_out>:<portname_in> - Specifies the cell type to use for the clock buffers - and its port names. The first port will be connected to - the clock network sinks, and the second will be connected - to the actual clock source. - - -inpad <celltype> <portname_out>:<portname_in> - If specified, a PAD cell of the given type is inserted on - clock nets that are also top module's inputs (in addition - to the clock buffer, if any). - -At least one of -buf or -inpad should be specified. -\end{lstlisting} - -\section{connect -- create or remove connections} -\label{cmd:connect} -\begin{lstlisting}[numbers=left,frame=single] - connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr> - -Create a connection. This is equivalent to adding the statement 'assign -<lhs-expr> = <rhs-expr>;' to the Verilog input. Per default, all existing -drivers for <lhs-expr> are unconnected. This can be overwritten by using -the -nounset option. - - - connect [-nomap] -unset <expr> - -Unconnect all existing drivers for the specified expression. - - - connect [-nomap] [-assert] -port <cell> <port> <expr> - -Connect the specified cell port to the specified cell port. - - -Per default signal alias names are resolved and all signal names are mapped -the the signal name of the primary driver. Using the -nomap option deactivates -this behavior. - -The connect command operates in one module only. Either only one module must -be selected or an active module must be set using the 'cd' command. - -The -assert option verifies that the connection already exists, instead of -making it. - -This command does not operate on module with processes. -\end{lstlisting} - -\section{connect\_rpc -- connect to RPC frontend} -\label{cmd:connect_rpc} -\begin{lstlisting}[numbers=left,frame=single] - connect_rpc -exec <command> [args...] - connect_rpc -path <path> - -Load modules using an out-of-process frontend. - - -exec <command> [args...] - run <command> with arguments [args...]. send requests on stdin, read - responses from stdout. - - -path <path> - connect to Unix domain socket at <path>. (Unix) - connect to bidirectional byte-type named pipe at <path>. (Windows) - -A simple JSON-based, newline-delimited protocol is used for communicating with -the frontend. Yosys requests data from the frontend by sending exactly 1 line -of JSON. Frontend responds with data or error message by replying with exactly -1 line of JSON as well. - - -> {"method": "modules"} - <- {"modules": ["<module-name>", ...]} - <- {"error": "<error-message>"} - request for the list of modules that can be derived by this frontend. - the 'hierarchy' command will call back into this frontend if a cell - with type <module-name> is instantiated in the design. - - -> {"method": "derive", "module": "<module-name">, "parameters": { - "<param-name>": {"type": "[unsigned|signed|string|real]", - "value": "<param-value>"}, ...}} - <- {"frontend": "[rtlil|verilog|...]","source": "<source>"}} - <- {"error": "<error-message>"} - request for the module <module-name> to be derived for a specific set of - parameters. <param-name> starts with \ for named parameters, and with $ - for unnamed parameters, which are numbered starting at 1.<param-value> - for integer parameters is always specified as a binary string of - unlimited precision. the <source> returned by the frontend is - hygienically parsedby a built-in Yosys <frontend>, allowing the RPC - frontend to return anyconvenient representation of the module. the - derived module is cached,so the response should be the same whenever the - same set of parameters is provided. -\end{lstlisting} - -\section{connwrappers -- match width of input-output port pairs} -\label{cmd:connwrappers} -\begin{lstlisting}[numbers=left,frame=single] - connwrappers [options] [selection] - -Wrappers are used in coarse-grain synthesis to wrap cells with smaller ports -in wrapper cells with a (larger) constant port size. I.e. the upper bits -of the wrapper output are signed/unsigned bit extended. This command uses this -knowledge to rewire the inputs of the driven cells to match the output of -the driving cell. - - -signed <cell_type> <port_name> <width_param> - -unsigned <cell_type> <port_name> <width_param> - consider the specified signed/unsigned wrapper output - - -port <cell_type> <port_name> <width_param> <sign_param> - use the specified parameter to decide if signed or unsigned - -The options -signed, -unsigned, and -port can be specified multiple times. -\end{lstlisting} - -\section{coolrunner2\_fixup -- insert necessary buffer cells for CoolRunner-II architecture} -\label{cmd:coolrunner2_fixup} -\begin{lstlisting}[numbers=left,frame=single] - coolrunner2_fixup [options] [selection] - -Insert necessary buffer cells for CoolRunner-II architecture. -\end{lstlisting} - -\section{coolrunner2\_sop -- break \$sop cells into ANDTERM/ORTERM cells} -\label{cmd:coolrunner2_sop} -\begin{lstlisting}[numbers=left,frame=single] - coolrunner2_sop [options] [selection] - -Break $sop cells into ANDTERM/ORTERM cells. -\end{lstlisting} - -\section{copy -- copy modules in the design} -\label{cmd:copy} -\begin{lstlisting}[numbers=left,frame=single] - copy old_name new_name - -Copy the specified module. Note that selection patterns are not supported -by this command. -\end{lstlisting} - -\section{cover -- print code coverage counters} -\label{cmd:cover} -\begin{lstlisting}[numbers=left,frame=single] - cover [options] [pattern] - -Print the code coverage counters collected using the cover() macro in the Yosys -C++ code. This is useful to figure out what parts of Yosys are utilized by a -test bench. - - -q - Do not print output to the normal destination (console and/or log file) - - -o file - Write output to this file, truncate if exists. - - -a file - Write output to this file, append if exists. - - -d dir - Write output to a newly created file in the specified directory. - -When one or more pattern (shell wildcards) are specified, then only counters -matching at least one pattern are printed. - - -It is also possible to instruct Yosys to print the coverage counters on program -exit to a file using environment variables: - - YOSYS_COVER_DIR="{dir-name}" yosys {args} - - This will create a file (with an auto-generated name) in this - directory and write the coverage counters to it. - - YOSYS_COVER_FILE="{file-name}" yosys {args} - - This will append the coverage counters to the specified file. - - -Hint: Use the following AWK command to consolidate Yosys coverage files: - - gawk '{ p[$3] = $1; c[$3] += $2; } END { for (i in p) - printf "%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3 - - -Coverage counters are only available in Yosys for Linux. -\end{lstlisting} - -\section{cutpoint -- adds formal cut points to the design} -\label{cmd:cutpoint} -\begin{lstlisting}[numbers=left,frame=single] - cutpoint [options] [selection] - -This command adds formal cut points to the design. - - -undef - set cupoint nets to undef (x). the default behavior is to create a - $anyseq cell and drive the cutpoint net from that -\end{lstlisting} - -\section{debug -- run command with debug log messages enabled} -\label{cmd:debug} -\begin{lstlisting}[numbers=left,frame=single] - debug cmd - -Execute the specified command with debug log messages enabled -\end{lstlisting} - -\section{delete -- delete objects in the design} -\label{cmd:delete} -\begin{lstlisting}[numbers=left,frame=single] - delete [selection] - -Deletes the selected objects. This will also remove entire modules, if the -whole module is selected. - - - delete {-input|-output|-port} [selection] - -Does not delete any object but removes the input and/or output flag on the -selected wires, thus 'deleting' module ports. -\end{lstlisting} - -\section{deminout -- demote inout ports to input or output} -\label{cmd:deminout} -\begin{lstlisting}[numbers=left,frame=single] - deminout [options] [selection] - -"Demote" inout ports to input or output ports, if possible. -\end{lstlisting} - -\section{demuxmap -- transform \$demux cells to \$eq + \$mux cells} -\label{cmd:demuxmap} -\begin{lstlisting}[numbers=left,frame=single] - demuxmap [selection] - -This pass transforms $demux cells to a bunch of equality comparisons. -\end{lstlisting} - -\section{design -- save, restore and reset current design} -\label{cmd:design} -\begin{lstlisting}[numbers=left,frame=single] - design -reset - -Clear the current design. - - - design -save <name> - -Save the current design under the given name. - - - design -stash <name> - -Save the current design under the given name and then clear the current design. - - - design -push - -Push the current design to the stack and then clear the current design. - - - design -push-copy - -Push the current design to the stack without clearing the current design. - - - design -pop - -Reset the current design and pop the last design from the stack. - - - design -load <name> - -Reset the current design and load the design previously saved under the given -name. - - - design -copy-from <name> [-as <new_mod_name>] <selection> - -Copy modules from the specified design into the current one. The selection is -evaluated in the other design. - - - design -copy-to <name> [-as <new_mod_name>] [selection] - -Copy modules from the current design into the specified one. - - - design -import <name> [-as <new_top_name>] [selection] - -Import the specified design into the current design. The source design must -either have a selected top module or the selection must contain exactly one -module that is then used as top module for this command. - - - design -reset-vlog - -The Verilog front-end remembers defined macros and top-level declarations -between calls to 'read_verilog'. This command resets this memory. - - design -delete <name> - -Delete the design previously saved under the given name. -\end{lstlisting} - -\section{dffinit -- set INIT param on FF cells} -\label{cmd:dffinit} -\begin{lstlisting}[numbers=left,frame=single] - dffinit [options] [selection] - -This pass sets an FF cell parameter to the the initial value of the net it -drives. (This is primarily used in FPGA flows.) - - -ff <cell_name> <output_port> <init_param> - operate on the specified cell type. this option can be used - multiple times. - - -highlow - use the string values "high" and "low" to represent a single-bit - initial value of 1 or 0. (multi-bit values are not supported in this - mode.) - - -strinit <string for high> <string for low> - use string values in the command line to represent a single-bit - initial value of 1 or 0. (multi-bit values are not supported in this - mode.) - - -noreinit - fail if the FF cell has already a defined initial value set in other - passes and the initial value of the net it drives is not equal to - the already defined initial value. -\end{lstlisting} - -\section{dfflegalize -- convert FFs to types supported by the target} -\label{cmd:dfflegalize} -\begin{lstlisting}[numbers=left,frame=single] - dfflegalize [options] [selection] - -Converts FFs to types supported by the target. - - -cell <cell_type_pattern> <init_values> - specifies a supported group of FF cells. <cell_type_pattern> - is a yosys internal fine cell name, where ? characters can be - as a wildcard matching any character. <init_values> specifies - which initialization values these FF cells can support, and can - be one of: - - - x (no init value supported) - - 0 - - 1 - - r (init value has to match reset value, only for some FF types) - - 01 (both 0 and 1 supported). - - -mince <num> - specifies a minimum number of FFs that should be using any given - clock enable signal. If a clock enable signal doesn't meet this - threshold, it is unmapped into soft logic. - - -minsrst <num> - specifies a minimum number of FFs that should be using any given - sync set/reset signal. If a sync set/reset signal doesn't meet this - threshold, it is unmapped into soft logic. - -The following cells are supported by this pass (ie. will be ingested, -and can be specified as allowed targets): - -- $_DFF_[NP]_ -- $_DFFE_[NP][NP]_ -- $_DFF_[NP][NP][01]_ -- $_DFFE_[NP][NP][01][NP]_ -- $_ALDFF_[NP][NP]_ -- $_ALDFFE_[NP][NP][NP]_ -- $_DFFSR_[NP][NP][NP]_ -- $_DFFSRE_[NP][NP][NP][NP]_ -- $_SDFF_[NP][NP][01]_ -- $_SDFFE_[NP][NP][01][NP]_ -- $_SDFFCE_[NP][NP][01][NP]_ -- $_SR_[NP][NP]_ -- $_DLATCH_[NP]_ -- $_DLATCH_[NP][NP][01]_ -- $_DLATCHSR_[NP][NP][NP]_ - -The following transformations are performed by this pass: - -- upconversion from a less capable cell to a more capable cell, if the less - capable cell is not supported (eg. dff -> dffe, or adff -> dffsr) -- unmapping FFs with clock enable (due to unsupported cell type or -mince) -- unmapping FFs with sync reset (due to unsupported cell type or -minsrst) -- adding inverters on the control pins (due to unsupported polarity) -- adding inverters on the D and Q pins and inverting the init/reset values - (due to unsupported init or reset value) -- converting sr into adlatch (by tying D to 1 and using E as set input) -- emulating unsupported dffsr cell by adff + adff + sr + mux -- emulating unsupported dlatchsr cell by adlatch + adlatch + sr + mux -- emulating adff when the (reset, init) value combination is unsupported by - dff + adff + dlatch + mux -- emulating adlatch when the (reset, init) value combination is unsupported by -- dlatch + adlatch + dlatch + mux -If the pass is unable to realize a given cell type (eg. adff when only plain dff -is available), an error is raised. -\end{lstlisting} - -\section{dfflibmap -- technology mapping of flip-flops} -\label{cmd:dfflibmap} -\begin{lstlisting}[numbers=left,frame=single] - dfflibmap [-prepare] [-map-only] [-info] -liberty <file> [selection] - -Map internal flip-flop cells to the flip-flop cells in the technology -library specified in the given liberty file. - -This pass may add inverters as needed. Therefore it is recommended to -first run this pass and then map the logic paths to the target technology. - -When called with -prepare, this command will convert the internal FF cells -to the internal cell types that best match the cells found in the given -liberty file, but won't actually map them to the target cells. - -When called with -map-only, this command will only map internal cell -types that are already of exactly the right type to match the target -cells, leaving remaining internal cells untouched. - -When called with -info, this command will only print the target cell -list, along with their associated internal cell types, and the arguments -that would be passed to the dfflegalize pass. The design will not be -changed. -\end{lstlisting} - -\section{dffunmap -- unmap clock enable and synchronous reset from FFs} -\label{cmd:dffunmap} -\begin{lstlisting}[numbers=left,frame=single] - dffunmap [options] [selection] - -This pass transforms FF types with clock enable and/or synchronous reset into -their base type (with neither clock enable nor sync reset) by emulating the -clock enable and synchronous reset with multiplexers on the cell input. - - -ce-only - unmap only clock enables, leave synchronous resets alone. - - -srst-only - unmap only synchronous resets, leave clock enables alone. -\end{lstlisting} - -\section{dump -- print parts of the design in RTLIL format} -\label{cmd:dump} -\begin{lstlisting}[numbers=left,frame=single] - dump [options] [selection] - -Write the selected parts of the design to the console or specified file in -RTLIL format. - - -m - also dump the module headers, even if only parts of a single - module is selected - - -n - only dump the module headers if the entire module is selected - - -o <filename> - write to the specified file. - - -a <filename> - like -outfile but append instead of overwrite -\end{lstlisting} - -\section{echo -- turning echoing back of commands on and off} -\label{cmd:echo} -\begin{lstlisting}[numbers=left,frame=single] - echo on - -Print all commands to log before executing them. - - - echo off - -Do not print all commands to log before executing them. (default) -\end{lstlisting} - -\section{ecp5\_gsr -- ECP5: handle GSR} -\label{cmd:ecp5_gsr} -\begin{lstlisting}[numbers=left,frame=single] - ecp5_gsr [options] [selection] - -Trim active low async resets connected to GSR and resolve GSR parameter, -if a GSR or SGSR primitive is used in the design. - -If any cell has the GSR parameter set to "AUTO", this will be resolved -to "ENABLED" if a GSR primitive is present and the (* nogsr *) attribute -is not set, otherwise it will be resolved to "DISABLED". -\end{lstlisting} - -\section{edgetypes -- list all types of edges in selection} -\label{cmd:edgetypes} -\begin{lstlisting}[numbers=left,frame=single] - edgetypes [options] [selection] - -This command lists all unique types of 'edges' found in the selection. An 'edge' -is a 4-tuple of source and sink cell type and port name. -\end{lstlisting} - -\section{efinix\_fixcarry -- Efinix: fix carry chain} -\label{cmd:efinix_fixcarry} -\begin{lstlisting}[numbers=left,frame=single] - efinix_fixcarry [options] [selection] - -Add Efinix adders to fix carry chain if needed. -\end{lstlisting} - -\section{equiv\_add -- add a \$equiv cell} -\label{cmd:equiv_add} -\begin{lstlisting}[numbers=left,frame=single] - equiv_add [-try] gold_sig gate_sig - -This command adds an $equiv cell for the specified signals. - - - equiv_add [-try] -cell gold_cell gate_cell - -This command adds $equiv cells for the ports of the specified cells. -\end{lstlisting} - -\section{equiv\_induct -- proving \$equiv cells using temporal induction} -\label{cmd:equiv_induct} -\begin{lstlisting}[numbers=left,frame=single] - equiv_induct [options] [selection] - -Uses a version of temporal induction to prove $equiv cells. - -Only selected $equiv cells are proven and only selected cells are used to -perform the proof. - - -undef - enable modelling of undef states - - -seq <N> - the max. number of time steps to be considered (default = 4) - -This command is very effective in proving complex sequential circuits, when -the internal state of the circuit quickly propagates to $equiv cells. - -However, this command uses a weak definition of 'equivalence': This command -proves that the two circuits will not diverge after they produce equal -outputs (observable points via $equiv) for at least <N> cycles (the <N> -specified via -seq). - -Combined with simulation this is very powerful because simulation can give -you confidence that the circuits start out synced for at least <N> cycles -after reset. -\end{lstlisting} - -\section{equiv\_make -- prepare a circuit for equivalence checking} -\label{cmd:equiv_make} -\begin{lstlisting}[numbers=left,frame=single] - equiv_make [options] gold_module gate_module equiv_module - -This creates a module annotated with $equiv cells from two presumably -equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status' -to work with the created equivalent checking module. - - -inames - Also match cells and wires with $... names. - - -blacklist <file> - Do not match cells or signals that match the names in the file. - - -encfile <file> - Match FSM encodings using the description from the file. - See 'help fsm_recode' for details. - -Note: The circuit created by this command is not a miter (with something like -a trigger output), but instead uses $equiv cells to encode the equivalence -checking problem. Use 'miter -equiv' if you want to create a miter circuit. -\end{lstlisting} - -\section{equiv\_mark -- mark equivalence checking regions} -\label{cmd:equiv_mark} -\begin{lstlisting}[numbers=left,frame=single] - equiv_mark [options] [selection] - -This command marks the regions in an equivalence checking module. Region 0 is -the proven part of the circuit. Regions with higher numbers are connected -unproven subcricuits. The integer attribute 'equiv_region' is set on all -wires and cells. -\end{lstlisting} - -\section{equiv\_miter -- extract miter from equiv circuit} -\label{cmd:equiv_miter} -\begin{lstlisting}[numbers=left,frame=single] - equiv_miter [options] miter_module [selection] - -This creates a miter module for further analysis of the selected $equiv cells. - - -trigger - Create a trigger output - - -cmp - Create cmp_* outputs for individual unproven $equiv cells - - -assert - Create a $assert cell for each unproven $equiv cell - - -undef - Create compare logic that handles undefs correctly -\end{lstlisting} - -\section{equiv\_opt -- prove equivalence for optimized circuit} -\label{cmd:equiv_opt} -\begin{lstlisting}[numbers=left,frame=single] - equiv_opt [options] [command] - -This command uses temporal induction to check circuit equivalence before and -after an optimization pass. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to the start of the command list, and empty to - label is synonymous to the end of the command list. - - -map <filename> - expand the modules in this file before proving equivalence. this is - useful for handling architecture-specific primitives. - - -blacklist <file> - Do not match cells or signals that match the names in the file - (passed to equiv_make). - - -assert - produce an error if the circuits are not equivalent. - - -multiclock - run clk2fflogic before equivalence checking. - - -async2sync - run async2sync before equivalence checking. - - -undef - enable modelling of undef states during equiv_induct. - - -nocheck - disable running check before and after the command under test. - -The following commands are executed by this verification command: - - run_pass: - hierarchy -auto-top - design -save preopt - check -assert (unless -nocheck) - [command] - check -assert (unless -nocheck) - design -stash postopt - - prepare: - design -copy-from preopt -as gold A:top - design -copy-from postopt -as gate A:top - - techmap: (only with -map) - techmap -wb -D EQUIV -autoproc -map <filename> ... - - prove: - clk2fflogic (only with -multiclock) - async2sync (only with -async2sync) - equiv_make -blacklist <filename> ... gold gate equiv - equiv_induct [-undef] equiv - equiv_status [-assert] equiv - - restore: - design -load preopt -\end{lstlisting} - -\section{equiv\_purge -- purge equivalence checking module} -\label{cmd:equiv_purge} -\begin{lstlisting}[numbers=left,frame=single] - equiv_purge [options] [selection] - -This command removes the proven part of an equivalence checking module, leaving -only the unproven segments in the design. This will also remove and add module -ports as needed. -\end{lstlisting} - -\section{equiv\_remove -- remove \$equiv cells} -\label{cmd:equiv_remove} -\begin{lstlisting}[numbers=left,frame=single] - equiv_remove [options] [selection] - -This command removes the selected $equiv cells. If neither -gold nor -gate is -used then only proven cells are removed. - - -gold - keep gold circuit - - -gate - keep gate circuit -\end{lstlisting} - -\section{equiv\_simple -- try proving simple \$equiv instances} -\label{cmd:equiv_simple} -\begin{lstlisting}[numbers=left,frame=single] - equiv_simple [options] [selection] - -This command tries to prove $equiv cells using a simple direct SAT approach. - - -v - verbose output - - -undef - enable modelling of undef states - - -short - create shorter input cones that stop at shared nodes. This yields - simpler SAT problems but sometimes fails to prove equivalence. - - -nogroup - disabling grouping of $equiv cells by output wire - - -seq <N> - the max. number of time steps to be considered (default = 1) -\end{lstlisting} - -\section{equiv\_status -- print status of equivalent checking module} -\label{cmd:equiv_status} -\begin{lstlisting}[numbers=left,frame=single] - equiv_status [options] [selection] - -This command prints status information for all selected $equiv cells. - - -assert - produce an error if any unproven $equiv cell is found -\end{lstlisting} - -\section{equiv\_struct -- structural equivalence checking} -\label{cmd:equiv_struct} -\begin{lstlisting}[numbers=left,frame=single] - equiv_struct [options] [selection] - -This command adds additional $equiv cells based on the assumption that the -gold and gate circuit are structurally equivalent. Note that this can introduce -bad $equiv cells in cases where the netlists are not structurally equivalent, -for example when analyzing circuits with cells with commutative inputs. This -command will also de-duplicate gates. - - -fwd - by default this command performans forward sweeps until nothing can - be merged by forwards sweeps, then backward sweeps until forward - sweeps are effective again. with this option set only forward sweeps - are performed. - - -fwonly <cell_type> - add the specified cell type to the list of cell types that are only - merged in forward sweeps and never in backward sweeps. $equiv is in - this list automatically. - - -icells - by default, the internal RTL and gate cell types are ignored. add - this option to also process those cell types with this command. - - -maxiter <N> - maximum number of iterations to run before aborting -\end{lstlisting} - -\section{eval -- evaluate the circuit given an input} -\label{cmd:eval} -\begin{lstlisting}[numbers=left,frame=single] - eval [options] [selection] - -This command evaluates the value of a signal given the value of all required -inputs. - - -set <signal> <value> - set the specified signal to the specified value. - - -set-undef - set all unspecified source signals to undef (x) - - -table <signal> - create a truth table using the specified input signals - - -show <signal> - show the value for the specified signal. if no -show option is passed - then all output ports of the current module are used. -\end{lstlisting} - -\section{exec -- execute commands in the operating system shell} -\label{cmd:exec} -\begin{lstlisting}[numbers=left,frame=single] - exec [options] -- [command] - -Execute a command in the operating system shell. All supplied arguments are -concatenated and passed as a command to popen(3). Whitespace is not guaranteed -to be preserved, even if quoted. stdin and stderr are not connected, while -stdout is logged unless the "-q" option is specified. - - - -q - Suppress stdout and stderr from subprocess - - -expect-return <int> - Generate an error if popen() does not return specified value. - May only be specified once; the final specified value is controlling - if specified multiple times. - - -expect-stdout <regex> - Generate an error if the specified regex does not match any line - in subprocess's stdout. May be specified multiple times. - - -not-expect-stdout <regex> - Generate an error if the specified regex matches any line - in subprocess's stdout. May be specified multiple times. - - - Example: exec -q -expect-return 0 -- echo "bananapie" | grep "nana" -\end{lstlisting} - -\section{expose -- convert internal signals to module ports} -\label{cmd:expose} -\begin{lstlisting}[numbers=left,frame=single] - expose [options] [selection] - -This command exposes all selected internal signals of a module as additional -outputs. - - -dff - only consider wires that are directly driven by register cell. - - -cut - when exposing a wire, create an input/output pair and cut the internal - signal path at that wire. - - -input - when exposing a wire, create an input port and disconnect the internal - driver. - - -shared - only expose those signals that are shared among the selected modules. - this is useful for preparing modules for equivalence checking. - - -evert - also turn connections to instances of other modules to additional - inputs and outputs and remove the module instances. - - -evert-dff - turn flip-flops to sets of inputs and outputs. - - -sep <separator> - when creating new wire/port names, the original object name is suffixed - with this separator (default: '.') and the port name or a type - designator for the exposed signal. -\end{lstlisting} - -\section{extract -- find subcircuits and replace them with cells} -\label{cmd:extract} -\begin{lstlisting}[numbers=left,frame=single] - extract -map <map_file> [options] [selection] - extract -mine <out_file> [options] [selection] - -This pass looks for subcircuits that are isomorphic to any of the modules -in the given map file and replaces them with instances of this modules. The -map file can be a Verilog source file (*.v) or an RTLIL source file (*.il). - - -map <map_file> - use the modules in this file as reference. This option can be used - multiple times. - - -map %<design-name> - use the modules in this in-memory design as reference. This option can - be used multiple times. - - -verbose - print debug output while analyzing - - -constports - also find instances with constant drivers. this may be much - slower than the normal operation. - - -nodefaultswaps - normally builtin port swapping rules for internal cells are used per - default. This turns that off, so e.g. 'a^b' does not match 'b^a' - when this option is used. - - -compat <needle_type> <haystack_type> - Per default, the cells in the map file (needle) must have the - type as the cells in the active design (haystack). This option - can be used to register additional pairs of types that should - match. This option can be used multiple times. - - -swap <needle_type> <port1>,<port2>[,...] - Register a set of swappable ports for a needle cell type. - This option can be used multiple times. - - -perm <needle_type> <port1>,<port2>[,...] <portA>,<portB>[,...] - Register a valid permutation of swappable ports for a needle - cell type. This option can be used multiple times. - - -cell_attr <attribute_name> - Attributes on cells with the given name must match. - - -wire_attr <attribute_name> - Attributes on wires with the given name must match. - - -ignore_parameters - Do not use parameters when matching cells. - - -ignore_param <cell_type> <parameter_name> - Do not use this parameter when matching cells. - -This pass does not operate on modules with unprocessed processes in it. -(I.e. the 'proc' pass should be used first to convert processes to netlists.) - -This pass can also be used for mining for frequent subcircuits. In this mode -the following options are to be used instead of the -map option. - - -mine <out_file> - mine for frequent subcircuits and write them to the given RTLIL file - - -mine_cells_span <min> <max> - only mine for subcircuits with the specified number of cells - default value: 3 5 - - -mine_min_freq <num> - only mine for subcircuits with at least the specified number of matches - default value: 10 - - -mine_limit_matches_per_module <num> - when calculating the number of matches for a subcircuit, don't count - more than the specified number of matches per module - - -mine_max_fanout <num> - don't consider internal signals with more than <num> connections - -The modules in the map file may have the attribute 'extract_order' set to an -integer value. Then this value is used to determine the order in which the pass -tries to map the modules to the design (ascending, default value is 0). - -See 'help techmap' for a pass that does the opposite thing. -\end{lstlisting} - -\section{extract\_counter -- Extract GreenPak4 counter cells} -\label{cmd:extract_counter} -\begin{lstlisting}[numbers=left,frame=single] - extract_counter [options] [selection] - -This pass converts non-resettable or async resettable down counters to -counter cells. Use a target-specific 'techmap' map file to convert those cells -to the actual target cells. - - -maxwidth N - Only extract counters up to N bits wide (default 64) - - -minwidth N - Only extract counters at least N bits wide (default 2) - - -allow_arst yes|no - Allow counters to have async reset (default yes) - - -dir up|down|both - Look for up-counters, down-counters, or both (default down) - - -pout X,Y,... - Only allow parallel output from the counter to the listed cell types - (if not specified, parallel outputs are not restricted) -\end{lstlisting} - -\section{extract\_fa -- find and extract full/half adders} -\label{cmd:extract_fa} -\begin{lstlisting}[numbers=left,frame=single] - extract_fa [options] [selection] - -This pass extracts full/half adders from a gate-level design. - - -fa, -ha - Enable cell types (fa=full adder, ha=half adder) - All types are enabled if none of this options is used - - -d <int> - Set maximum depth for extracted logic cones (default=20) - - -b <int> - Set maximum breadth for extracted logic cones (default=6) - - -v - Verbose output -\end{lstlisting} - -\section{extract\_reduce -- converts gate chains into \$reduce\_* cells} -\label{cmd:extract_reduce} -\begin{lstlisting}[numbers=left,frame=single] - extract_reduce [options] [selection] - -converts gate chains into $reduce_* cells - -This command finds chains of $_AND_, $_OR_, and $_XOR_ cells and replaces them -with their corresponding $reduce_* cells. Because this command only operates on -these cell types, it is recommended to map the design to only these cell types -using the `abc -g` command. Note that, in some cases, it may be more effective -to map the design to only $_AND_ cells, run extract_reduce, map the remaining -parts of the design to AND/OR/XOR cells, and run extract_reduce a second time. - - -allow-off-chain - Allows matching of cells that have loads outside the chain. These cells - will be replicated and folded into the $reduce_* cell, but the original - cell will remain, driving its original loads. -\end{lstlisting} - -\section{extractinv -- extract explicit inverter cells for invertible cell pins} -\label{cmd:extractinv} -\begin{lstlisting}[numbers=left,frame=single] - extractinv [options] [selection] - -Searches the design for all cells with invertible pins controlled by a cell -parameter (eg. IS_CLK_INVERTED on many Xilinx cells) and removes the parameter. -If the parameter was set to 1, inserts an explicit inverter cell in front of -the pin instead. Normally used for output to ISE, which does not support the -inversion parameters. - -To mark a cell port as invertible, use (* invertible_pin = "param_name" *) -on the wire in the blackbox module. The parameter value should have -the same width as the port, and will be effectively XORed with it. - - -inv <celltype> <portname_out>:<portname_in> - Specifies the cell type to use for the inverters and its port names. - This option is required. -\end{lstlisting} - -\section{flatten -- flatten design} -\label{cmd:flatten} -\begin{lstlisting}[numbers=left,frame=single] - flatten [options] [selection] - -This pass flattens the design by replacing cells by their implementation. This -pass is very similar to the 'techmap' pass. The only difference is that this -pass is using the current design as mapping library. - -Cells and/or modules with the 'keep_hierarchy' attribute set will not be -flattened by this command. - - -wb - Ignore the 'whitebox' attribute on cell implementations. -\end{lstlisting} - -\section{flowmap -- pack LUTs with FlowMap} -\label{cmd:flowmap} -\begin{lstlisting}[numbers=left,frame=single] - flowmap [options] [selection] - -This pass uses the FlowMap technology mapping algorithm to pack logic gates -into k-LUTs with optimal depth. It allows mapping any circuit elements that can -be evaluated with the `eval` pass, including cells with multiple output ports -and multi-bit input and output ports. - - -maxlut k - perform technology mapping for a k-LUT architecture. if not specified, - defaults to 3. - - -minlut n - only produce n-input or larger LUTs. if not specified, defaults to 1. - - -cells <cell>[,<cell>,...] - map specified cells. if not specified, maps $_NOT_, $_AND_, $_OR_, - $_XOR_ and $_MUX_, which are the outputs of the `simplemap` pass. - - -relax - perform depth relaxation and area minimization. - - -r-alpha n, -r-beta n, -r-gamma n - parameters of depth relaxation heuristic potential function. - if not specified, alpha=8, beta=2, gamma=1. - - -optarea n - optimize for area by trading off at most n logic levels for fewer LUTs. - n may be zero, to optimize for area without increasing depth. - implies -relax. - - -debug - dump intermediate graphs. - - -debug-relax - explain decisions performed during depth relaxation. -\end{lstlisting} - -\section{fmcombine -- combine two instances of a cell into one} -\label{cmd:fmcombine} -\begin{lstlisting}[numbers=left,frame=single] - fmcombine [options] module_name gold_cell gate_cell - -This pass takes two cells, which are instances of the same module, and replaces -them with one instance of a special 'combined' module, that effectively -contains two copies of the original module, plus some formal properties. - -This is useful for formal test benches that check what differences in behavior -a slight difference in input causes in a module. - - -initeq - Insert assumptions that initially all FFs in both circuits have the - same initial values. - - -anyeq - Do not duplicate $anyseq/$anyconst cells. - - -fwd - Insert forward hint assumptions into the combined module. - - -bwd - Insert backward hint assumptions into the combined module. - (Backward hints are logically equivalend to fordward hits, but - some solvers are faster with bwd hints, or even both -bwd and -fwd.) - - -nop - Don't insert hint assumptions into the combined module. - (This should not provide any speedup over the original design, but - strangely sometimes it does.) - -If none of -fwd, -bwd, and -nop is given, then -fwd is used as default. -\end{lstlisting} - -\section{fminit -- set init values/sequences for formal} -\label{cmd:fminit} -\begin{lstlisting}[numbers=left,frame=single] - fminit [options] <selection> - -This pass creates init constraints (for example for reset sequences) in a formal -model. - - -seq <signal> <sequence> - Set sequence using comma-separated list of values, use 'z for - unconstrained bits. The last value is used for the remainder of the - trace. - - -set <signal> <value> - Add constant value constraint - - -posedge <signal> - -negedge <signal> - Set clock for init sequences -\end{lstlisting} - -\section{formalff -- prepare FFs for formal} -\label{cmd:formalff} -\begin{lstlisting}[numbers=left,frame=single] - formalff [options] [selection] - -This pass transforms clocked flip-flops to prepare a design for formal -verification. If a design contains latches and/or multiple different clocks run -the async2sync or clk2fflogic passes before using this pass. - - -clk2ff - Replace all clocked flip-flops with $ff cells that use the implicit - global clock. This assumes, without checking, that the design uses a - single global clock. If that is not the case, the clk2fflogic pass - should be used instead. - - -ff2anyinit - Replace uninitialized bits of $ff cells with $anyinit cells. An - $anyinit cell behaves exactly like an $ff cell with an undefined - initialization value. The difference is that $anyinit inhibits - don't-care optimizations and is used to track solver-provided values - in witness traces. - - If combined with -clk2ff this also affects newly created $ff cells. - - -anyinit2ff - Replaces $anyinit cells with uninitialized $ff cells. This performs the - reverse of -ff2anyinit and can be used, before running a backend pass - (or similar) that is not yet aware of $anyinit cells. - - Note that after running -anyinit2ff, in general, performing don't-care - optimizations is not sound in a formal verification setting. - - -fine - Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for - -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit. - - -setundef - Find FFs with undefined initialization values for which changing the - initialization does not change the observable behavior and initialize - them. For -ff2anyinit, this reduces the number of generated $anyinit - cells that drive wires with private names. -\end{lstlisting} - -\section{freduce -- perform functional reduction} -\label{cmd:freduce} -\begin{lstlisting}[numbers=left,frame=single] - freduce [options] [selection] - -This pass performs functional reduction in the circuit. I.e. if two nodes are -equivalent, they are merged to one node and one of the redundant drivers is -disconnected. A subsequent call to 'clean' will remove the redundant drivers. - - -v, -vv - enable verbose or very verbose output - - -inv - enable explicit handling of inverted signals - - -stop <n> - stop after <n> reduction operations. this is mostly used for - debugging the freduce command itself. - - -dump <prefix> - dump the design to <prefix>_<module>_<num>.il after each reduction - operation. this is mostly used for debugging the freduce command. - -This pass is undef-aware, i.e. it considers don't-care values for detecting -equivalent nodes. - -All selected wires are considered for rewiring. The selected cells cover the -circuit that is analyzed. -\end{lstlisting} - -\section{fsm -- extract and optimize finite state machines} -\label{cmd:fsm} -\begin{lstlisting}[numbers=left,frame=single] - fsm [options] [selection] - -This pass calls all the other fsm_* passes in a useful order. This performs -FSM extraction and optimization. It also calls opt_clean as needed: - - fsm_detect unless got option -nodetect - fsm_extract - - fsm_opt - opt_clean - fsm_opt - - fsm_expand if got option -expand - opt_clean if got option -expand - fsm_opt if got option -expand - - fsm_recode unless got option -norecode - - fsm_info - - fsm_export if got option -export - fsm_map unless got option -nomap - -Options: - - -expand, -norecode, -export, -nomap - enable or disable passes as indicated above - - -fullexpand - call expand with -full option - - -encoding type - -fm_set_fsm_file file - -encfile file - passed through to fsm_recode pass - -This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe' -before this pass to prepare the design. - -The Verific frontend may merge multiplexers in a way that interferes with FSM -detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before -reading the source, and 'bmuxmap' after 'proc' for best results. -\end{lstlisting} - -\section{fsm\_detect -- finding FSMs in design} -\label{cmd:fsm_detect} -\begin{lstlisting}[numbers=left,frame=single] - fsm_detect [selection] - -This pass detects finite state machines by identifying the state signal. -The state signal is then marked by setting the attribute 'fsm_encoding' -on the state signal to "auto". - -Existing 'fsm_encoding' attributes are not changed by this pass. - -Signals can be protected from being detected by this pass by setting the -'fsm_encoding' attribute to "none". - -This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe' -before this pass to prepare the design for fsm_detect. - -The Verific frontend may merge multiplexers in a way that interferes with FSM -detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before -reading the source, and 'bmuxmap' after 'proc' for best results. -\end{lstlisting} - -\section{fsm\_expand -- expand FSM cells by merging logic into it} -\label{cmd:fsm_expand} -\begin{lstlisting}[numbers=left,frame=single] - fsm_expand [-full] [selection] - -The fsm_extract pass is conservative about the cells that belong to a finite -state machine. This pass can be used to merge additional auxiliary gates into -the finite state machine. - -By default, fsm_expand is still a bit conservative regarding merging larger -word-wide cells. Call with -full to consider all cells for merging. -\end{lstlisting} - -\section{fsm\_export -- exporting FSMs to KISS2 files} -\label{cmd:fsm_export} -\begin{lstlisting}[numbers=left,frame=single] - fsm_export [-noauto] [-o filename] [-origenc] [selection] - -This pass creates a KISS2 file for every selected FSM. For FSMs with the -'fsm_export' attribute set, the attribute value is used as filename, otherwise -the module and cell name is used as filename. If the parameter '-o' is given, -the first exported FSM is written to the specified filename. This overwrites -the setting as specified with the 'fsm_export' attribute. All other FSMs are -exported to the default name as mentioned above. - - -noauto - only export FSMs that have the 'fsm_export' attribute set - - -o filename - filename of the first exported FSM - - -origenc - use binary state encoding as state names instead of s0, s1, ... -\end{lstlisting} - -\section{fsm\_extract -- extracting FSMs in design} -\label{cmd:fsm_extract} -\begin{lstlisting}[numbers=left,frame=single] - fsm_extract [selection] - -This pass operates on all signals marked as FSM state signals using the -'fsm_encoding' attribute. It consumes the logic that creates the state signal -and uses the state signal to generate control signal and replaces it with an -FSM cell. - -The generated FSM cell still generates the original state signal with its -original encoding. The 'fsm_opt' pass can be used in combination with the -'opt_clean' pass to eliminate this signal. -\end{lstlisting} - -\section{fsm\_info -- print information on finite state machines} -\label{cmd:fsm_info} -\begin{lstlisting}[numbers=left,frame=single] - fsm_info [selection] - -This pass dumps all internal information on FSM cells. It can be useful for -analyzing the synthesis process and is called automatically by the 'fsm' -pass so that this information is included in the synthesis log file. -\end{lstlisting} - -\section{fsm\_map -- mapping FSMs to basic logic} -\label{cmd:fsm_map} -\begin{lstlisting}[numbers=left,frame=single] - fsm_map [selection] - -This pass translates FSM cells to flip-flops and logic. -\end{lstlisting} - -\section{fsm\_opt -- optimize finite state machines} -\label{cmd:fsm_opt} -\begin{lstlisting}[numbers=left,frame=single] - fsm_opt [selection] - -This pass optimizes FSM cells. It detects which output signals are actually -not used and removes them from the FSM. This pass is usually used in -combination with the 'opt_clean' pass (see also 'help fsm'). -\end{lstlisting} - -\section{fsm\_recode -- recoding finite state machines} -\label{cmd:fsm_recode} -\begin{lstlisting}[numbers=left,frame=single] - fsm_recode [options] [selection] - -This pass reassign the state encodings for FSM cells. At the moment only -one-hot encoding and binary encoding is supported. - -encoding <type> - specify the encoding scheme used for FSMs without the - 'fsm_encoding' attribute or with the attribute set to `auto'. - - -fm_set_fsm_file <file> - generate a file containing the mapping from old to new FSM encoding - in form of Synopsys Formality set_fsm_* commands. - - -encfile <file> - write the mappings from old to new FSM encoding to a file in the - following format: - - .fsm <module_name> <state_signal> - .map <old_bitpattern> <new_bitpattern> -\end{lstlisting} - -\section{fst2tb -- generate testbench out of fst file} -\label{cmd:fst2tb} -\begin{lstlisting}[numbers=left,frame=single] - fst2tb [options] [top-level] - -This command generates testbench for the circuit using the given top-level -module and simulus signal from FST file - - -tb <name> - generated testbench name. - files <name>.v and <name>.txt are created as result. - - -r <filename> - read simulation FST file - - -clock <portname> - name of top-level clock input - - -clockn <portname> - name of top-level clock input (inverse polarity) - - -scope <name> - scope of simulation top model - - -start <time> - start co-simulation in arbitary time (default 0) - - -stop <time> - stop co-simulation in arbitary time (default END) - - -n <integer> - number of clock cycles to simulate (default: 20) -\end{lstlisting} - -\section{gatemate\_foldinv -- fold inverters into Gatemate LUT trees} -\label{cmd:gatemate_foldinv} -\begin{lstlisting}[numbers=left,frame=single] - gatemate_foldinv [selection] - - -This pass searches for $__CC_NOT cells and folds them into CC_LUT2, CC_L2T4 -and CC_L2T5 cells as created by LUT tree mapping. -\end{lstlisting} - -\section{glift -- create GLIFT models and optimization problems} -\label{cmd:glift} -\begin{lstlisting}[numbers=left,frame=single] - glift <command> [options] [selection] - -Augments the current or specified module with gate-level information flow -tracking (GLIFT) logic using the "constructive mapping" approach. Also can set -up QBF-SAT optimization problems in order to optimize GLIFT models or trade off -precision and complexity. - - -Commands: - - -create-precise-model - Replaces the current or specified module with one that has corresponding - "taint" inputs, outputs, and internal nets along with precise taint - tracking logic. For example, precise taint tracking logic for an AND gate - is: - - y_t = a & b_t | b & a_t | a_t & b_t - - - -create-imprecise-model - Replaces the current or specified module with one that has corresponding - "taint" inputs, outputs, and internal nets along with imprecise "All OR" - taint tracking logic: - - y_t = a_t | b_t - - - -create-instrumented-model - Replaces the current or specified module with one that has corresponding - "taint" inputs, outputs, and internal nets along with 4 varying-precision - versions of taint tracking logic. Which version of taint tracking logic is - used for a given gate is determined by a MUX selected by an $anyconst cell. - By default, unless the `-no-cost-model` option is provided, an additional - wire named `__glift_weight` with the `keep` and `minimize` attributes is - added to the module along with pmuxes and adders to calculate a rough - estimate of the number of logic gates in the GLIFT model given an assignment - for the $anyconst cells. The four versions of taint tracking logic for an - AND gate are: - y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`) - y_t = a_t | a & b_t - y_t = b_t | b & a_t - y_t = a_t | b_t (like `-create-imprecise-model`) - - -Options: - - -taint-constants - Constant values in the design are labeled as tainted. - (default: label constants as un-tainted) - - -keep-outputs - Do not remove module outputs. Taint tracking outputs will appear in the - module ports alongside the orignal outputs. - (default: original module outputs are removed) - - -simple-cost-model - Do not model logic area. Instead model the number of non-zero assignments to - $anyconsts. Taint tracking logic versions vary in their size, but all - reduced-precision versions are significantly smaller than the fully-precise - version. A non-zero $anyconst assignment means that reduced-precision taint - tracking logic was chosen for some gate. Only applicable in combination with - `-create-instrumented-model`. (default: use a complex model and give that - wire the "keep" and "minimize" attributes) - - -no-cost-model - Do not model taint tracking logic area and do not create a `__glift_weight` - wire. Only applicable in combination with `-create-instrumented-model`. - (default: model area and give that wire the "keep" and "minimize" - attributes) - - -instrument-more - Allow choice from more versions of (even simpler) taint tracking logic. A - total of 8 versions of taint tracking logic will be added per gate, - including the 4 versions from `-create-instrumented-model` and these - additional versions: - - y_t = a_t - y_t = b_t - y_t = 1 - y_t = 0 - - Only applicable in combination with `-create-instrumented-model`. - (default: do not add more versions of taint tracking logic. -\end{lstlisting} - -\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches} -\label{cmd:greenpak4_dffinv} -\begin{lstlisting}[numbers=left,frame=single] - greenpak4_dffinv [options] [selection] - -Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells. -\end{lstlisting} - -\section{help -- display help messages} -\label{cmd:help} -\begin{lstlisting}[numbers=left,frame=single] - help ................ list all commands - help <command> ...... print help message for given command - help -all ........... print complete command reference - - help -cells .......... list all cell types - help <celltype> ..... print help message for given cell type - help <celltype>+ .... print verilog code for given cell type -\end{lstlisting} - -\section{hierarchy -- check, expand and clean up design hierarchy} -\label{cmd:hierarchy} -\begin{lstlisting}[numbers=left,frame=single] - hierarchy [-check] [-top <module>] - hierarchy -generate <cell-types> <port-decls> - -In parametric designs, a module might exists in several variations with -different parameter values. This pass looks at all modules in the current -design and re-runs the language frontends for the parametric modules as -needed. It also resolves assignments to wired logic data types (wand/wor), -resolves positional module parameters, unrolls array instances, and more. - - -check - also check the design hierarchy. this generates an error when - an unknown module is used as cell type. - - -simcheck - like -check, but also throw an error if blackbox modules are - instantiated, and throw an error if the design has no top module. - - -smtcheck - like -simcheck, but allow smtlib2_module modules. - - -purge_lib - by default the hierarchy command will not remove library (blackbox) - modules. use this option to also remove unused blackbox modules. - - -libdir <directory> - search for files named <module_name>.v in the specified directory - for unknown modules and automatically run read_verilog for each - unknown module. - - -keep_positionals - per default this pass also converts positional arguments in cells - to arguments using port names. This option disables this behavior. - - -keep_portwidths - per default this pass adjusts the port width on cells that are - module instances when the width does not match the module port. This - option disables this behavior. - - -nodefaults - do not resolve input port default values - - -nokeep_asserts - per default this pass sets the "keep" attribute on all modules - that directly or indirectly contain one or more formal properties. - This option disables this behavior. - - -top <module> - use the specified top module to build the design hierarchy. Modules - outside this tree (unused modules) are removed. - - when the -top option is used, the 'top' attribute will be set on the - specified top module. otherwise a module with the 'top' attribute set - will implicitly be used as top module, if such a module exists. - - -auto-top - automatically determine the top of the design hierarchy and mark it. - - -chparam name value - elaborate the top module using this parameter value. Modules on which - this parameter does not exist may cause a warning message to be output. - This option can be specified multiple times to override multiple - parameters. String values must be passed in double quotes ("). - -In -generate mode this pass generates blackbox modules for the given cell -types (wildcards supported). For this the design is searched for cells that -match the given types and then the given port declarations are used to -determine the direction of the ports. The syntax for a port declaration is: - - {i|o|io}[@<num>]:<portname> - -Input ports are specified with the 'i' prefix, output ports with the 'o' -prefix and inout ports with the 'io' prefix. The optional <num> specifies -the position of the port in the parameter list (needed when instantiated -using positional arguments). When <num> is not specified, the <portname> can -also contain wildcard characters. - -This pass ignores the current selection and always operates on all modules -in the current design. -\end{lstlisting} - -\section{hilomap -- technology mapping of constant hi- and/or lo-drivers} -\label{cmd:hilomap} -\begin{lstlisting}[numbers=left,frame=single] - hilomap [options] [selection] - -Map constants to 'tielo' and 'tiehi' driver cells. - - -hicell <celltype> <portname> - Replace constant hi bits with this cell. - - -locell <celltype> <portname> - Replace constant lo bits with this cell. - - -singleton - Create only one hi/lo cell and connect all constant bits - to that cell. Per default a separate cell is created for - each constant bit. -\end{lstlisting} - -\section{history -- show last interactive commands} -\label{cmd:history} -\begin{lstlisting}[numbers=left,frame=single] - history - -This command prints all commands in the shell history buffer. This are -all commands executed in an interactive session, but not the commands -from executed scripts. -\end{lstlisting} - -\section{ice40\_braminit -- iCE40: perform SB\_RAM40\_4K initialization from file} -\label{cmd:ice40_braminit} -\begin{lstlisting}[numbers=left,frame=single] - ice40_braminit - -This command processes all SB_RAM40_4K blocks with a non-empty INIT_FILE -parameter and converts it into the required INIT_x attributes -\end{lstlisting} - -\section{ice40\_dsp -- iCE40: map multipliers} -\label{cmd:ice40_dsp} -\begin{lstlisting}[numbers=left,frame=single] - ice40_dsp [options] [selection] - -Map multipliers ($mul/SB_MAC16) and multiply-accumulate ($mul/SB_MAC16 + $add) -cells into iCE40 DSP resources. -Currently, only the 16x16 multiply mode is supported and not the 2 x 8x8 mode. - -Pack input registers (A, B, {C,D}; with optional hold), pipeline registers -({F,J,K,G}, H), output registers (O -- full 32-bits or lower 16-bits only; with -optional hold), and post-adder into into the SB_MAC16 resource. - -Multiply-accumulate operations using the post-adder with feedback on the {C,D} -input will be folded into the DSP. In this scenario only, resetting the -the accumulator to an arbitrary value can be inferred to use the {C,D} input. -\end{lstlisting} - -\section{ice40\_opt -- iCE40: perform simple optimizations} -\label{cmd:ice40_opt} -\begin{lstlisting}[numbers=left,frame=single] - ice40_opt [options] [selection] - -This command executes the following script: - - do - <ice40 specific optimizations> - opt_expr -mux_undef -undriven [-full] - opt_merge - opt_dff - opt_clean - while <changed design> -\end{lstlisting} - -\section{ice40\_wrapcarry -- iCE40: wrap carries} -\label{cmd:ice40_wrapcarry} -\begin{lstlisting}[numbers=left,frame=single] - ice40_wrapcarry [selection] - -Wrap manually instantiated SB_CARRY cells, along with their associated SB_LUT4s, -into an internal $__ICE40_CARRY_WRAPPER cell for preservation across technology -mapping. - -Attributes on both cells will have their names prefixed with 'SB_CARRY.' or -'SB_LUT4.' and attached to the wrapping cell. -A (* keep *) attribute on either cell will be logically OR-ed together. - - -unwrap - unwrap $__ICE40_CARRY_WRAPPER cells back into SB_CARRYs and SB_LUT4s, - including restoring their attributes. -\end{lstlisting} - -\section{insbuf -- insert buffer cells for connected wires} -\label{cmd:insbuf} -\begin{lstlisting}[numbers=left,frame=single] - insbuf [options] [selection] - -Insert buffer cells into the design for directly connected wires. - - -buf <celltype> <in-portname> <out-portname> - Use the given cell type instead of $_BUF_. (Notice that the next - call to "clean" will remove all $_BUF_ in the design.) -\end{lstlisting} - -\section{iopadmap -- technology mapping of i/o pads (or buffers)} -\label{cmd:iopadmap} -\begin{lstlisting}[numbers=left,frame=single] - iopadmap [options] [selection] - -Map module inputs/outputs to PAD cells from a library. This pass -can only map to very simple PAD cells. Use 'techmap' to further map -the resulting cells to more sophisticated PAD cells. - - -inpad <celltype> <in_port>[:<ext_port>] - Map module input ports to the given cell type with the - given output port name. if a 2nd portname is given, the - signal is passed through the pad cell, using the 2nd - portname as the port facing the module port. - - -outpad <celltype> <out_port>[:<ext_port>] - -inoutpad <celltype> <io_port>[:<ext_port>] - Similar to -inpad, but for output and inout ports. - - -toutpad <celltype> <oe_port>:<out_port>[:<ext_port>] - Merges $_TBUF_ cells into the output pad cell. This takes precedence - over the other -outpad cell. The first portname is the enable input - of the tristate driver, which can be prefixed with `~` for negative - polarity enable. - - -tinoutpad <celltype> <oe_port>:<in_port>:<out_port>[:<ext_port>] - Merges $_TBUF_ cells into the inout pad cell. This takes precedence - over the other -inoutpad cell. The first portname is the enable input - of the tristate driver and the 2nd portname is the internal output - buffering the external signal. Like with `-toutpad`, the enable can - be marked as negative polarity by prefixing the name with `~`. - - -ignore <celltype> <portname>[:<portname>]* - Skips mapping inputs/outputs that are already connected to given - ports of the given cell. Can be used multiple times. This is in - addition to the cells specified as mapping targets. - - -widthparam <param_name> - Use the specified parameter name to set the port width. - - -nameparam <param_name> - Use the specified parameter to set the port name. - - -bits - create individual bit-wide buffers even for ports that - are wider. (the default behavior is to create word-wide - buffers using -widthparam to set the word size on the cell.) - -Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode. -\end{lstlisting} - -\section{jny -- write design and metadata} -\label{cmd:jny} -\begin{lstlisting}[numbers=left,frame=single] - jny [options] [selection] - -Write JSON netlist metadata for the current design - - -o <filename> - write to the specified file. - - -no-connections - Don't include connection information in the netlist output. - - -no-attributes - Don't include attributed information in the netlist output. - - -no-properties - Don't include property information in the netlist output. - -See 'help write_jny' for a description of the JSON format used. -\end{lstlisting} - -\section{json -- write design in JSON format} -\label{cmd:json} -\begin{lstlisting}[numbers=left,frame=single] - json [options] [selection] - -Write a JSON netlist of all selected objects. - - -o <filename> - write to the specified file. - - -aig - also include AIG models for the different gate types - - -compat-int - emit 32-bit or smaller fully-defined parameter values directly - as JSON numbers (for compatibility with old parsers) - -See 'help write_json' for a description of the JSON format used. -\end{lstlisting} - -\section{log -- print text and log files} -\label{cmd:log} -\begin{lstlisting}[numbers=left,frame=single] - log string - -Print the given string to the screen and/or the log file. This is useful for TCL -scripts, because the TCL command "puts" only goes to stdout but not to -logfiles. - - -stdout - Print the output to stdout too. This is useful when all Yosys is - executed with a script and the -q (quiet operation) argument to notify - the user. - - -stderr - Print the output to stderr too. - - -nolog - Don't use the internal log() command. Use either -stdout or -stderr, - otherwise no output will be generated at all. - - -n - do not append a newline -\end{lstlisting} - -\section{logger -- set logger properties} -\label{cmd:logger} -\begin{lstlisting}[numbers=left,frame=single] - logger [options] - -This command sets global logger properties, also available using command line -options. - - -[no]time - enable/disable display of timestamp in log output. - - -[no]stderr - enable/disable logging errors to stderr. - - -warn regex - print a warning for all log messages matching the regex. - - -nowarn regex - if a warning message matches the regex, it is printed as regular - message instead. - - -werror regex - if a warning message matches the regex, it is printed as error - message instead and the tool terminates with a nonzero return code. - - -[no]debug - globally enable/disable debug log messages. - - -experimental <feature> - do not print warnings for the specified experimental feature - - -expect <type> <regex> <expected_count> - expect log, warning or error to appear. matched errors will terminate - with exit code 0. - - -expect-no-warnings - gives error in case there is at least one warning that is not expected. - - -check-expected - verifies that the patterns previously set up by -expect have actually - been met, then clears the expected log list. If this is not called - manually, the check will happen at yosys exist time instead. -\end{lstlisting} - -\section{ls -- list modules or objects in modules} -\label{cmd:ls} -\begin{lstlisting}[numbers=left,frame=single] - ls [selection] - -When no active module is selected, this prints a list of modules. - -When an active module is selected, this prints a list of objects in the module. -\end{lstlisting} - -\section{ltp -- print longest topological path} -\label{cmd:ltp} -\begin{lstlisting}[numbers=left,frame=single] - ltp [options] [selection] - -This command prints the longest topological path in the design. (Only considers -paths within a single module, so the design must be flattened.) - - -noff - automatically exclude FF cell types -\end{lstlisting} - -\section{lut2mux -- convert \$lut to \$\_MUX\_} -\label{cmd:lut2mux} -\begin{lstlisting}[numbers=left,frame=single] - lut2mux [options] [selection] - -This pass converts $lut cells to $_MUX_ gates. -\end{lstlisting} - -\section{maccmap -- mapping macc cells} -\label{cmd:maccmap} -\begin{lstlisting}[numbers=left,frame=single] - maccmap [-unmap] [selection] - -This pass maps $macc cells to yosys $fa and $alu cells. When the -unmap option -is used then the $macc cell is mapped to $add, $sub, etc. cells instead. -\end{lstlisting} - -\section{memory -- translate memories to basic cells} -\label{cmd:memory} -\begin{lstlisting}[numbers=left,frame=single] - memory [-norom] [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-no-rw-check] [-bram <bram_rules>] [selection] - -This pass calls all the other memory_* passes in a useful order: - - opt_mem - opt_mem_priority - opt_mem_feedback - memory_bmux2rom (skipped if called with -norom) - memory_dff [-no-rw-check] (skipped if called with -nordff or -memx) - opt_clean - memory_share [-nowiden] [-nosat] - opt_mem_widen - memory_memx (when called with -memx) - opt_clean - memory_collect - memory_bram -rules <bram_rules> (when called with -bram) - memory_map (skipped if called with -nomap) - -This converts memories to word-wide DFFs and address decoders -or multiport memory blocks if called with the -nomap option. -\end{lstlisting} - -\section{memory\_bmux2rom -- convert muxes to ROMs} -\label{cmd:memory_bmux2rom} -\begin{lstlisting}[numbers=left,frame=single] - memory_bmux2rom [options] [selection] - -This pass converts $bmux cells with constant A input to ROMs. -\end{lstlisting} - -\section{memory\_bram -- map memories to block rams} -\label{cmd:memory_bram} -\begin{lstlisting}[numbers=left,frame=single] - memory_bram -rules <rule_file> [selection] - -This pass converts the multi-port $mem memory cells into block ram instances. -The given rules file describes the available resources and how they should be -used. - -The rules file contains configuration options, a set of block ram description -and a sequence of match rules. - -The option 'attr_icase' configures how attribute values are matched. The value 0 -means case-sensitive, 1 means case-insensitive. - -A block ram description looks like this: - - bram RAMB1024X32 # name of BRAM cell - init 1 # set to '1' if BRAM can be initialized - abits 10 # number of address bits - dbits 32 # number of data bits - groups 2 # number of port groups - ports 1 1 # number of ports in each group - wrmode 1 0 # set to '1' if this groups is write ports - enable 4 1 # number of enable bits - transp 0 2 # transparent (for read ports) - clocks 1 2 # clock configuration - clkpol 2 2 # clock polarity configuration - endbram - -For the option 'transp' the value 0 means non-transparent, 1 means transparent -and a value greater than 1 means configurable. All groups with the same -value greater than 1 share the same configuration bit. - -For the option 'clocks' the value 0 means non-clocked, and a value greater -than 0 means clocked. All groups with the same value share the same clock -signal. - -For the option 'clkpol' the value 0 means negative edge, 1 means positive edge -and a value greater than 1 means configurable. All groups with the same value -greater than 1 share the same configuration bit. - -Using the same bram name in different bram blocks will create different variants -of the bram. Verilog configuration parameters for the bram are created as -needed. - -It is also possible to create variants by repeating statements in the bram block -and appending '@<label>' to the individual statements. - -A match rule looks like this: - - match RAMB1024X32 - max waste 16384 # only use this bram if <= 16k ram bits are unused - min efficiency 80 # only use this bram if efficiency is at least 80% - endmatch - -It is possible to match against the following values with min/max rules: - - words ........ number of words in memory in design - abits ........ number of address bits on memory in design - dbits ........ number of data bits on memory in design - wports ....... number of write ports on memory in design - rports ....... number of read ports on memory in design - ports ........ number of ports on memory in design - bits ......... number of bits in memory in design - dups .......... number of duplications for more read ports - - awaste ....... number of unused address slots for this match - dwaste ....... number of unused data bits for this match - bwaste ....... number of unused bram bits for this match - waste ........ total number of unused bram bits (bwaste*dups) - efficiency ... total percentage of used and non-duplicated bits - - acells ....... number of cells in 'address-direction' - dcells ....... number of cells in 'data-direction' - cells ........ total number of cells (acells*dcells*dups) - -A match containing the command 'attribute' followed by a list of space -separated 'name[=string_value]' values requires that the memory contains any -one of the given attribute name and string values (where specified), or name -and integer 1 value (if no string_value given, since Verilog will interpret -'(* attr *)' as '(* attr=1 *)'). -A name prefixed with '!' indicates that the attribute must not exist. - -The interface for the created bram instances is derived from the bram -description. Use 'techmap' to convert the created bram instances into -instances of the actual bram cells of your target architecture. - -A match containing the command 'or_next_if_better' is only used if it -has a higher efficiency than the next match (and the one after that if -the next also has 'or_next_if_better' set, and so forth). - -A match containing the command 'make_transp' will add external circuitry -to simulate 'transparent read', if necessary. - -A match containing the command 'make_outreg' will add external flip-flops -to implement synchronous read ports, if necessary. - -A match containing the command 'shuffle_enable A' will re-organize -the data bits to accommodate the enable pattern of port A. -\end{lstlisting} - -\section{memory\_collect -- creating multi-port memory cells} -\label{cmd:memory_collect} -\begin{lstlisting}[numbers=left,frame=single] - memory_collect [selection] - -This pass collects memories and memory ports and creates generic multiport -memory cells. -\end{lstlisting} - -\section{memory\_dff -- merge input/output DFFs into memory read ports} -\label{cmd:memory_dff} -\begin{lstlisting}[numbers=left,frame=single] - memory_dff [-no-rw-check] [selection] - -This pass detects DFFs at memory read ports and merges them into the memory -port. I.e. it consumes an asynchronous memory port and the flip-flops at its -interface and yields a synchronous memory port. - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). -\end{lstlisting} - -\section{memory\_libmap -- map memories to cells} -\label{cmd:memory_libmap} -\begin{lstlisting}[numbers=left,frame=single] - memory_libmap -lib <library_file> [-D <condition>] [selection] - -This pass takes a description of available RAM cell types and maps -all selected memories to one of them, or leaves them to be mapped to FFs. - - -lib <library_file> - Selects a library file containing RAM cell definitions. This option - can be passed more than once to select multiple libraries. - See passes/memory/memlib.md for description of the library format. - - -D <condition> - Enables a condition that can be checked within the library file - to eg. select between slightly different hardware variants. - This option can be passed any number of times. - - -logic-cost-rom <num> - -logic-cost-ram <num> - Sets the cost of a single bit for memory lowered to soft logic. - - -no-auto-distributed - -no-auto-block - -no-auto-huge - Disables automatic mapping of given kind of RAMs. Manual mapping - (using ram_style or other attributes) is still supported. -\end{lstlisting} - -\section{memory\_map -- translate multiport memories to basic cells} -\label{cmd:memory_map} -\begin{lstlisting}[numbers=left,frame=single] - memory_map [options] [selection] - -This pass converts multiport memory cells as generated by the memory_collect -pass to word-wide DFFs and address decoders. - - -attr !<name> - do not map memories that have attribute <name> set. - - -attr <name>[=<value>] - for memories that have attribute <name> set, only map them if its value - is a string <value> (if specified), or an integer 1 (otherwise). if this - option is specified multiple times, map the memory if the attribute is - to any of the values. - - -iattr - for -attr, ignore case of <value>. - - -rom-only - only perform conversion for ROMs (memories with no write ports). - - -keepdc - when mapping ROMs, keep x-bits shared across read ports. - - -formal - map memories for a global clock based formal verification flow. - This implies -keepdc, uses $ff cells for ROMs and sets hdlname - attributes. It also has limited support for async write ports - as generated by clk2fflogic. -\end{lstlisting} - -\section{memory\_memx -- emulate vlog sim behavior for mem ports} -\label{cmd:memory_memx} -\begin{lstlisting}[numbers=left,frame=single] - memory_memx [selection] - -This pass adds additional circuitry that emulates the Verilog simulation -behavior for out-of-bounds memory reads and writes. -\end{lstlisting} - -\section{memory\_narrow -- split up wide memory ports} -\label{cmd:memory_narrow} -\begin{lstlisting}[numbers=left,frame=single] - memory_narrow [options] [selection] - -This pass splits up wide memory ports into several narrow ports. -\end{lstlisting} - -\section{memory\_nordff -- extract read port FFs from memories} -\label{cmd:memory_nordff} -\begin{lstlisting}[numbers=left,frame=single] - memory_nordff [options] [selection] - -This pass extracts FFs from memory read ports. This results in a netlist -similar to what one would get from not calling memory_dff. -\end{lstlisting} - -\section{memory\_share -- consolidate memory ports} -\label{cmd:memory_share} -\begin{lstlisting}[numbers=left,frame=single] - memory_share [-nosat] [-nowiden] [selection] - -This pass merges share-able memory ports into single memory ports. - -The following methods are used to consolidate the number of memory ports: - - - When multiple write ports access the same address then this is converted - to a single write port with a more complex data and/or enable logic path. - - - When multiple read or write ports access adjacent aligned addresses, they - are merged to a single wide read or write port. This transformation can be - disabled with the "-nowiden" option. - - - When multiple write ports are never accessed at the same time (a SAT - solver is used to determine this), then the ports are merged into a single - write port. This transformation can be disabled with the "-nosat" option. - -Note that in addition to the algorithms implemented in this pass, the $memrd -and $memwr cells are also subject to generic resource sharing passes (and other -optimizations) such as "share" and "opt_merge". -\end{lstlisting} - -\section{memory\_unpack -- unpack multi-port memory cells} -\label{cmd:memory_unpack} -\begin{lstlisting}[numbers=left,frame=single] - memory_unpack [selection] - -This pass converts the multi-port $mem memory cells into individual $memrd and -$memwr cells. It is the counterpart to the memory_collect pass. -\end{lstlisting} - -\section{miter -- automatically create a miter circuit} -\label{cmd:miter} -\begin{lstlisting}[numbers=left,frame=single] - miter -equiv [options] gold_name gate_name miter_name - -Creates a miter circuit for equivalence checking. The gold- and gate- modules -must have the same interfaces. The miter circuit will have all inputs of the -two source modules, prefixed with 'in_'. The miter circuit has a 'trigger' -output that goes high if an output mismatch between the two source modules is -detected. - - -ignore_gold_x - a undef (x) bit in the gold module output will match any value in - the gate module output. - - -make_outputs - also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs - on the miter circuit. - - -make_outcmp - also create a cmp_* output for each gold/gate output pair. - - -make_assert - also create an 'assert' cell that checks if trigger is always low. - - -flatten - call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit. - - - -cross - allow output ports on the gold module to match input ports on the - gate module. This is useful when the gold module contains additional - logic to drive some of the gate module inputs. - - - miter -assert [options] module [miter_name] - -Creates a miter circuit for property checking. All input ports are kept, -output ports are discarded. An additional output 'trigger' is created that -goes high when an assert is violated. Without a miter_name, the existing -module is modified. - - -make_outputs - keep module output ports. - - -flatten - call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit. -\end{lstlisting} - -\section{mutate -- generate or apply design mutations} -\label{cmd:mutate} -\begin{lstlisting}[numbers=left,frame=single] - mutate -list N [options] [selection] - -Create a list of N mutations using an even sampling. - - -o filename - Write list to this file instead of console output - - -s filename - Write a list of all src tags found in the design to the specified file - - -seed N - RNG seed for selecting mutations - - -none - Include a "none" mutation in the output - - -ctrl name width value - Add -ctrl options to the output. Use 'value' for first mutation, then - simply count up from there. - - -mode name - -module name - -cell name - -port name - -portbit int - -ctrlbit int - -wire name - -wirebit int - -src string - Filter list of mutation candidates to those matching - the given parameters. - - -cfg option int - Set a configuration option. Options available: - weight_pq_w weight_pq_b weight_pq_c weight_pq_s - weight_pq_mw weight_pq_mb weight_pq_mc weight_pq_ms - weight_cover pick_cover_prcnt - - - mutate -mode MODE [options] - -Apply the given mutation. - - -ctrl name width value - Add a control signal with the given name and width. The mutation is - activated if the control signal equals the given value. - - -module name - -cell name - -port name - -portbit int - -ctrlbit int - Mutation parameters, as generated by 'mutate -list N'. - - -wire name - -wirebit int - -src string - Ignored. (They are generated by -list for documentation purposes.) -\end{lstlisting} - -\section{muxcover -- cover trees of MUX cells with wider MUXes} -\label{cmd:muxcover} -\begin{lstlisting}[numbers=left,frame=single] - muxcover [options] [selection] - -Cover trees of $_MUX_ cells with $_MUX{4,8,16}_ cells - - -mux4[=cost], -mux8[=cost], -mux16[=cost] - Cover $_MUX_ trees using the specified types of MUXes (with optional - integer costs). If none of these options are given, the effect is the - same as if all of them are. - Default costs: $_MUX4_ = 220, $_MUX8_ = 460, - $_MUX16_ = 940 - - -mux2=cost - Use the specified cost for $_MUX_ cells when making covering decisions. - Default cost: $_MUX_ = 100 - - -dmux=cost - Use the specified cost for $_MUX_ cells used in decoders. - Default cost: 90 - - -nodecode - Do not insert decoder logic. This reduces the number of possible - substitutions, but guarantees that the resulting circuit is not - less efficient than the original circuit. - - -nopartial - Do not consider mappings that use $_MUX<N>_ to select from less - than <N> different signals. -\end{lstlisting} - -\section{muxpack -- \$mux/\$pmux cascades to \$pmux} -\label{cmd:muxpack} -\begin{lstlisting}[numbers=left,frame=single] - muxpack [selection] - -This pass converts cascaded chains of $pmux cells (e.g. those create from case -constructs) and $mux cells (e.g. those created by if-else constructs) into -$pmux cells. - -This optimisation is conservative --- it will only pack $mux or $pmux cells -whose select lines are driven by '$eq' cells with other such cells if it can be -certain that their select inputs are mutually exclusive. -\end{lstlisting} - -\section{nlutmap -- map to LUTs of different sizes} -\label{cmd:nlutmap} -\begin{lstlisting}[numbers=left,frame=single] - nlutmap [options] [selection] - -This pass uses successive calls to 'abc' to map to an architecture. That -provides a small number of differently sized LUTs. - - -luts N_1,N_2,N_3,... - The number of LUTs with 1, 2, 3, ... inputs that are - available in the target architecture. - - -assert - Create an error if not all logic can be mapped - -Excess logic that does not fit into the specified LUTs is mapped back -to generic logic gates ($_AND_, etc.). -\end{lstlisting} - -\section{onehot -- optimize \$eq cells for onehot signals} -\label{cmd:onehot} -\begin{lstlisting}[numbers=left,frame=single] - onehot [options] [selection] - -This pass optimizes $eq cells that compare one-hot signals against constants - - -v, -vv - verbose output -\end{lstlisting} - -\section{opt -- perform simple optimizations} -\label{cmd:opt} -\begin{lstlisting}[numbers=left,frame=single] - opt [options] [selection] - -This pass calls all the other opt_* passes in a useful order. This performs -a series of trivial optimizations and cleanups. This pass executes the other -passes in the following order: - - opt_expr [-mux_undef] [-mux_bool] [-undriven] [-noclkinv] [-fine] [-full] [-keepdc] - opt_merge [-share_all] -nomux - - do - opt_muxtree - opt_reduce [-fine] [-full] - opt_merge [-share_all] - opt_share (-full only) - opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] (except when called with -noff) - opt_clean [-purge] - opt_expr [-mux_undef] [-mux_bool] [-undriven] [-noclkinv] [-fine] [-full] [-keepdc] - while <changed design> - -When called with -fast the following script is used instead: - - do - opt_expr [-mux_undef] [-mux_bool] [-undriven] [-noclkinv] [-fine] [-full] [-keepdc] - opt_merge [-share_all] - opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] (except when called with -noff) - opt_clean [-purge] - while <changed design in opt_dff> - -Note: Options in square brackets (such as [-keepdc]) are passed through to -the opt_* commands when given to 'opt'. -\end{lstlisting} - -\section{opt\_clean -- remove unused cells and wires} -\label{cmd:opt_clean} -\begin{lstlisting}[numbers=left,frame=single] - opt_clean [options] [selection] - -This pass identifies wires and cells that are unused and removes them. Other -passes often remove cells but leave the wires in the design or reconnect the -wires but leave the old cells in the design. This pass can be used to clean up -after the passes that do the actual work. - -This pass only operates on completely selected modules without processes. - - -purge - also remove internal nets if they have a public name -\end{lstlisting} - -\section{opt\_demorgan -- Optimize reductions with DeMorgan equivalents} -\label{cmd:opt_demorgan} -\begin{lstlisting}[numbers=left,frame=single] - opt_demorgan [selection] - -This pass pushes inverters through $reduce_* cells if this will reduce the -overall gate count of the circuit -\end{lstlisting} - -\section{opt\_dff -- perform DFF optimizations} -\label{cmd:opt_dff} -\begin{lstlisting}[numbers=left,frame=single] - opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] [selection] - -This pass converts flip-flops to a more suitable type by merging clock enables -and synchronous reset multiplexers, removing unused control inputs, or -potentially removes the flip-flop altogether, converting it to a constant -driver. - - -nodffe - disables dff -> dffe conversion, and other transforms recognizing clock - enable - - -nosdff - disables dff -> sdff conversion, and other transforms recognizing sync - resets - - -simple-dffe - only enables clock enable recognition transform for obvious cases - - -sat - additionally invoke SAT solver to detect and remove flip-flops (with - non-constant inputs) that can also be replaced with a constant driver - - -keepdc - some optimizations change the behavior of the circuit with respect to - don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause - all result bits to be set to x. this behavior changes when 'a+0' is - replaced by 'a'. the -keepdc option disables all such optimizations. -\end{lstlisting} - -\section{opt\_expr -- perform const folding and simple expression rewriting} -\label{cmd:opt_expr} -\begin{lstlisting}[numbers=left,frame=single] - opt_expr [options] [selection] - -This pass performs const folding on internal cell types with constant inputs. -It also performs some simple expression rewriting. - - -mux_undef - remove 'undef' inputs from $mux, $pmux and $_MUX_ cells - - -mux_bool - replace $mux cells with inverters or buffers when possible - - -undriven - replace undriven nets with undef (x) constants - - -noclkinv - do not optimize clock inverters by changing FF types - - -fine - perform fine-grain optimizations - - -full - alias for -mux_undef -mux_bool -undriven -fine - - -keepdc - some optimizations change the behavior of the circuit with respect to - don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause - all result bits to be set to x. this behavior changes when 'a+0' is - replaced by 'a'. the -keepdc option disables all such optimizations. -\end{lstlisting} - -\section{opt\_ffinv -- push inverters through FFs} -\label{cmd:opt_ffinv} -\begin{lstlisting}[numbers=left,frame=single] - opt_ffinv [selection] - -This pass pushes inverters to the other side of a FF when they can be merged -into LUTs on the other side. -\end{lstlisting} - -\section{opt\_lut -- optimize LUT cells} -\label{cmd:opt_lut} -\begin{lstlisting}[numbers=left,frame=single] - opt_lut [options] [selection] - -This pass combines cascaded $lut cells with unused inputs. - - -dlogic <type>:<cell-port>=<LUT-input>[:<cell-port>=<LUT-input>...] - preserve connections to dedicated logic cell <type> that has ports - <cell-port> connected to LUT inputs <LUT-input>. this includes - the case where both LUT and dedicated logic input are connected to - the same constant. - - -limit N - only perform the first N combines, then stop. useful for debugging. -\end{lstlisting} - -\section{opt\_lut\_ins -- discard unused LUT inputs} -\label{cmd:opt_lut_ins} -\begin{lstlisting}[numbers=left,frame=single] - opt_lut_ins [options] [selection] - -This pass removes unused inputs from LUT cells (that is, inputs that can not -influence the output signal given this LUT's value). While such LUTs cannot -be directly emitted by ABC, they can be a result of various post-ABC -transformations, such as mapping wide LUTs (not all sub-LUTs will use the -full set of inputs) or optimizations such as xilinx_dffopt. - - -tech <technology> - Instead of generic $lut cells, operate on LUT cells specific - to the given technology. Valid values are: xilinx, ecp5, gowin. -\end{lstlisting} - -\section{opt\_mem -- optimize memories} -\label{cmd:opt_mem} -\begin{lstlisting}[numbers=left,frame=single] - opt_mem [options] [selection] - -This pass performs various optimizations on memories in the design. -\end{lstlisting} - -\section{opt\_mem\_feedback -- convert memory read-to-write port feedback paths to write enables} -\label{cmd:opt_mem_feedback} -\begin{lstlisting}[numbers=left,frame=single] - opt_mem_feedback [selection] - -This pass detects cases where an asynchronous read port is only connected via -a mux tree to a write port with the same address. When such a connection is -found, it is replaced with a new condition on an enable signal, allowing -for removal of the read port. -\end{lstlisting} - -\section{opt\_mem\_priority -- remove priority relations between write ports that can never collide} -\label{cmd:opt_mem_priority} -\begin{lstlisting}[numbers=left,frame=single] - opt_mem_priority [selection] - -This pass detects cases where one memory write port has priority over another -even though they can never collide with each other -- ie. there can never be -a situation where a given memory bit is written by both ports at the same -time, for example because of always-different addresses, or mutually exclusive -enable signals. In such cases, the priority relation is removed. -\end{lstlisting} - -\section{opt\_mem\_widen -- optimize memories where all ports are wide} -\label{cmd:opt_mem_widen} -\begin{lstlisting}[numbers=left,frame=single] - opt_mem_widen [options] [selection] - -This pass looks for memories where all ports are wide and adjusts the base -memory width up until that stops being the case. -\end{lstlisting} - -\section{opt\_merge -- consolidate identical cells} -\label{cmd:opt_merge} -\begin{lstlisting}[numbers=left,frame=single] - opt_merge [options] [selection] - -This pass identifies cells with identical type and input signals. Such cells -are then merged to one cell. - - -nomux - Do not merge MUX cells. - - -share_all - Operate on all cell types, not just built-in types. - - -keepdc - Do not merge flipflops with don't-care bits in their initial value. -\end{lstlisting} - -\section{opt\_muxtree -- eliminate dead trees in multiplexer trees} -\label{cmd:opt_muxtree} -\begin{lstlisting}[numbers=left,frame=single] - opt_muxtree [selection] - -This pass analyzes the control signals for the multiplexer trees in the design -and identifies inputs that can never be active. It then removes this dead -branches from the multiplexer trees. - -This pass only operates on completely selected modules without processes. -\end{lstlisting} - -\section{opt\_reduce -- simplify large MUXes and AND/OR gates} -\label{cmd:opt_reduce} -\begin{lstlisting}[numbers=left,frame=single] - opt_reduce [options] [selection] - -This pass performs two interlinked optimizations: - -1. it consolidates trees of large AND gates or OR gates and eliminates -duplicated inputs. - -2. it identifies duplicated inputs to MUXes and replaces them with a single -input with the original control signals OR'ed together. - - -fine - perform fine-grain optimizations - - -full - alias for -fine -\end{lstlisting} - -\section{opt\_share -- merge mutually exclusive cells of the same type that share an input signal} -\label{cmd:opt_share} -\begin{lstlisting}[numbers=left,frame=single] - opt_share [selection] - -This pass identifies mutually exclusive cells of the same type that: - (a) share an input signal, - (b) drive the same $mux, $_MUX_, or $pmux multiplexing cell, - -allowing the cell to be merged and the multiplexer to be moved from -multiplexing its output to multiplexing the non-shared input signals. -\end{lstlisting} - -\section{paramap -- renaming cell parameters} -\label{cmd:paramap} -\begin{lstlisting}[numbers=left,frame=single] - paramap [options] [selection] - -This command renames cell parameters and/or maps key/value pairs to -other key/value pairs. - - -tocase <name> - Match attribute names case-insensitively and set it to the specified - name. - - -rename <old_name> <new_name> - Rename attributes as specified - - -map <old_name>=<old_value> <new_name>=<new_value> - Map key/value pairs as indicated. - - -imap <old_name>=<old_value> <new_name>=<new_value> - Like -map, but use case-insensitive match for <old_value> when - it is a string value. - - -remove <name>=<value> - Remove attributes matching this pattern. - -For example, mapping Diamond-style ECP5 "init" attributes to Yosys-style: - - paramap -tocase INIT t:LUT4 -\end{lstlisting} - -\section{peepopt -- collection of peephole optimizers} -\label{cmd:peepopt} -\begin{lstlisting}[numbers=left,frame=single] - peepopt [options] [selection] - -This pass applies a collection of peephole optimizers to the current design. -\end{lstlisting} - -\section{plugin -- load and list loaded plugins} -\label{cmd:plugin} -\begin{lstlisting}[numbers=left,frame=single] - plugin [options] - -Load and list loaded plugins. - - -i <plugin_filename> - Load (install) the specified plugin. - - -a <alias_name> - Register the specified alias name for the loaded plugin - - -l - List loaded plugins -\end{lstlisting} - -\section{pmux2shiftx -- transform \$pmux cells to \$shiftx cells} -\label{cmd:pmux2shiftx} -\begin{lstlisting}[numbers=left,frame=single] - pmux2shiftx [options] [selection] - -This pass transforms $pmux cells to $shiftx cells. - - -v, -vv - verbose output - - -min_density <percentage> - specifies the minimum density for the shifter - default: 50 - - -min_choices <int> - specified the minimum number of choices for a control signal - default: 3 - - -onehot ignore|pmux|shiftx - select strategy for one-hot encoded control signals - default: pmux - - -norange - disable $sub inference for "range decoders" -\end{lstlisting} - -\section{pmuxtree -- transform \$pmux cells to trees of \$mux cells} -\label{cmd:pmuxtree} -\begin{lstlisting}[numbers=left,frame=single] - pmuxtree [selection] - -This pass transforms $pmux cells to trees of $mux cells. -\end{lstlisting} - -\section{portlist -- list (top-level) ports} -\label{cmd:portlist} -\begin{lstlisting}[numbers=left,frame=single] - portlist [options] [selection] - -This command lists all module ports found in the selected modules. - -If no selection is provided then it lists the ports on the top module. - - -m - print verilog blackbox module definitions instead of port lists -\end{lstlisting} - -\section{prep -- generic synthesis script} -\label{cmd:prep} -\begin{lstlisting}[numbers=left,frame=single] - prep [options] - -This command runs a conservative RTL synthesis. A typical application for this -is the preparation stage of a verification flow. This command does not operate -on partly selected designs. - - -top <module> - use the specified module as top module (default='top') - - -auto-top - automatically determine the top of the design hierarchy - - -flatten - flatten the design before synthesis. this will pass '-auto-top' to - 'hierarchy' if no top module is specified. - - -ifx - passed to 'proc'. uses verilog simulation behavior for verilog if/case - undef handling. this also prevents 'wreduce' from being run. - - -memx - simulate verilog simulation behavior for out-of-bounds memory accesses - using the 'memory_memx' pass. - - -nomem - do not run any of the memory_* passes - - -rdff - call 'memory_dff'. This enables merging of FFs into - memory read ports. - - -nokeepdc - do not call opt_* with -keepdc - - -run <from_label>[:<to_label>] - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -The following commands are executed by this synthesis command: - - begin: - hierarchy -check [-top <top> | -auto-top] - - coarse: - proc [-ifx] - flatten (if -flatten) - opt_expr -keepdc - opt_clean - check - opt -noff -keepdc - wreduce -keepdc [-memx] - memory_dff (if -rdff) - memory_memx (if -memx) - opt_clean - memory_collect - opt -noff -keepdc -fast - - check: - stat - check -\end{lstlisting} - -\section{printattrs -- print attributes of selected objects} -\label{cmd:printattrs} -\begin{lstlisting}[numbers=left,frame=single] - printattrs [selection] - -Print all attributes of the selected objects. -\end{lstlisting} - -\section{proc -- translate processes to netlists} -\label{cmd:proc} -\begin{lstlisting}[numbers=left,frame=single] - proc [options] [selection] - -This pass calls all the other proc_* passes in the most common order. - - proc_clean - proc_rmdead - proc_prune - proc_init - proc_arst - proc_rom - proc_mux - proc_dlatch - proc_dff - proc_memwr - proc_clean - opt_expr -keepdc - -This replaces the processes in the design with multiplexers, -flip-flops and latches. - -The following options are supported: - - -nomux - Will omit the proc_mux pass. - - -norom - Will omit the proc_rom pass. - - -global_arst [!]<netname> - This option is passed through to proc_arst. - - -ifx - This option is passed through to proc_mux. proc_rmdead is not - executed in -ifx mode. - - -noopt - Will omit the opt_expr pass. -\end{lstlisting} - -\section{proc\_arst -- detect asynchronous resets} -\label{cmd:proc_arst} -\begin{lstlisting}[numbers=left,frame=single] - proc_arst [-global_arst [!]<netname>] [selection] - -This pass identifies asynchronous resets in the processes and converts them -to a different internal representation that is suitable for generating -flip-flop cells with asynchronous resets. - - -global_arst [!]<netname> - In modules that have a net with the given name, use this net as async - reset for registers that have been assign initial values in their - declaration ('reg foobar = constant_value;'). Use the '!' modifier for - active low reset signals. Note: the frontend stores the default value - in the 'init' attribute on the net. -\end{lstlisting} - -\section{proc\_clean -- remove empty parts of processes} -\label{cmd:proc_clean} -\begin{lstlisting}[numbers=left,frame=single] - proc_clean [options] [selection] - - -quiet - do not print any messages. - -This pass removes empty parts of processes and ultimately removes a process -if it contains only empty structures. -\end{lstlisting} - -\section{proc\_dff -- extract flip-flops from processes} -\label{cmd:proc_dff} -\begin{lstlisting}[numbers=left,frame=single] - proc_dff [selection] - -This pass identifies flip-flops in the processes and converts them to -d-type flip-flop cells. -\end{lstlisting} - -\section{proc\_dlatch -- extract latches from processes} -\label{cmd:proc_dlatch} -\begin{lstlisting}[numbers=left,frame=single] - proc_dlatch [selection] - -This pass identifies latches in the processes and converts them to -d-type latches. -\end{lstlisting} - -\section{proc\_init -- convert initial block to init attributes} -\label{cmd:proc_init} -\begin{lstlisting}[numbers=left,frame=single] - proc_init [selection] - -This pass extracts the 'init' actions from processes (generated from Verilog -'initial' blocks) and sets the initial value to the 'init' attribute on the -respective wire. -\end{lstlisting} - -\section{proc\_memwr -- extract memory writes from processes} -\label{cmd:proc_memwr} -\begin{lstlisting}[numbers=left,frame=single] - proc_memwr [selection] - -This pass converts memory writes in processes into $memwr cells. -\end{lstlisting} - -\section{proc\_mux -- convert decision trees to multiplexers} -\label{cmd:proc_mux} -\begin{lstlisting}[numbers=left,frame=single] - proc_mux [options] [selection] - -This pass converts the decision trees in processes (originating from if-else -and case statements) to trees of multiplexer cells. - - -ifx - Use Verilog simulation behavior with respect to undef values in - 'case' expressions and 'if' conditions. -\end{lstlisting} - -\section{proc\_prune -- remove redundant assignments} -\label{cmd:proc_prune} -\begin{lstlisting}[numbers=left,frame=single] - proc_prune [selection] - -This pass identifies assignments in processes that are always overwritten by -a later assignment to the same signal and removes them. -\end{lstlisting} - -\section{proc\_rmdead -- eliminate dead trees in decision trees} -\label{cmd:proc_rmdead} -\begin{lstlisting}[numbers=left,frame=single] - proc_rmdead [selection] - -This pass identifies unreachable branches in decision trees and removes them. -\end{lstlisting} - -\section{proc\_rom -- convert switches to ROMs} -\label{cmd:proc_rom} -\begin{lstlisting}[numbers=left,frame=single] - proc_rom [selection] - -This pass converts switches into read-only memories when appropriate. -\end{lstlisting} - -\section{qbfsat -- solve a 2QBF-SAT problem in the circuit} -\label{cmd:qbfsat} -\begin{lstlisting}[numbers=left,frame=single] - qbfsat [options] [selection] - -This command solves an "exists-forall" 2QBF-SAT problem defined over the -currently selected module. Existentially-quantified variables are declared by -assigning a wire "$anyconst". Universally-quantified variables may be -explicitly declared by assigning a wire "$allconst", but module inputs will be -treated as universally-quantified variables by default. - - -nocleanup - Do not delete temporary files and directories. Useful for debugging. - - -dump-final-smt2 <file> - Pass the --dump-smt2 option to yosys-smtbmc. - - -assume-outputs - Add an "$assume" cell for the conjunction of all one-bit module output - wires. - - -assume-negative-polarity - When adding $assume cells for one-bit module output wires, assume they - are negative polarity signals and should always be low, for example like - the miters created with the `miter` command. - - -nooptimize - Ignore "\minimize" and "\maximize" attributes, do not emit - "(maximize)" or "(minimize)" in the SMT-LIBv2, and generally make no - attempt to optimize anything. - - -nobisection - If a wire is marked with the "\minimize" or "\maximize" attribute, - do not attempt to optimize that value with the default iterated solving - and threshold bisection approach. Instead, have yosys-smtbmc emit a - "(minimize)" or "(maximize)" command in the SMT-LIBv2 output and - hope that the solver supports optimizing quantified bitvector problems. - - -solver <solver> - Use a particular solver. Choose one of: "z3", "yices", and "cvc4". - (default: yices) - - -solver-option <name> <value> - Set the specified solver option in the SMT-LIBv2 problem file. - - -timeout <value> - Set the per-iteration timeout in seconds. - (default: no timeout) - - -O0, -O1, -O2 - Control the use of ABC to simplify the QBF-SAT problem before solving. - - -sat - Generate an error if the solver does not return "sat". - - -unsat - Generate an error if the solver does not return "unsat". - - -show-smtbmc - Print the output from yosys-smtbmc. - - -specialize - If the problem is satisfiable, replace each "$anyconst" cell with its - corresponding constant value from the model produced by the solver. - - -specialize-from-file <solution file> - Do not run the solver, but instead only attempt to replace each - "$anyconst" cell in the current module with a constant value provided - by the specified file. - - -write-solution <solution file> - If the problem is satisfiable, write the corresponding constant value - for each "$anyconst" cell from the model produced by the solver to the - specified file. -\end{lstlisting} - -\section{qwp -- quadratic wirelength placer} -\label{cmd:qwp} -\begin{lstlisting}[numbers=left,frame=single] - qwp [options] [selection] - -This command runs quadratic wirelength placement on the selected modules and -annotates the cells in the design with 'qwp_position' attributes. - - -ltr - Add left-to-right constraints: constrain all inputs on the left border - outputs to the right border. - - -alpha - Add constraints for inputs/outputs to be placed in alphanumerical - order along the y-axis (top-to-bottom). - - -grid N - Number of grid divisions in x- and y-direction. (default=16) - - -dump <html_file_name> - Dump a protocol of the placement algorithm to the html file. - - -v - Verbose solver output for profiling or debugging - -Note: This implementation of a quadratic wirelength placer uses exact -dense matrix operations. It is only a toy-placer for small circuits. -\end{lstlisting} - -\section{read -- load HDL designs} -\label{cmd:read} -\begin{lstlisting}[numbers=left,frame=single] - read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>.. - -Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support -is only available via Verific.) - -Additional -D<macro>[=<value>] options may be added after the option indicating -the language version (and before file names) to set additional verilog defines. - - - read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>.. - -Load the specified VHDL files. (Requires Verific.) - - - read {-edif} <edif-file>.. - -Load the specified EDIF files. (Requires Verific.) - - - read {-liberty} <liberty-file>.. - -Load the specified Liberty files. - - -lib - only create empty blackbox modules - - - read {-f|-F} <command-file> - -Load and execute the specified command file. (Requires Verific.) -Check verific command for more information about supported commands in file. - - - read -define <macro>[=<value>].. - -Set global Verilog/SystemVerilog defines. - - - read -undef <macro>.. - -Unset global Verilog/SystemVerilog defines. - - - read -incdir <directory> - -Add directory to global Verilog/SystemVerilog include directories. - - - read -verific - read -noverific - -Subsequent calls to 'read' will either use or not use Verific. Calling 'read' -with -verific will result in an error on Yosys binaries that are built without -Verific support. The default is to use Verific if it is available. -\end{lstlisting} - -\section{read\_aiger -- read AIGER file} -\label{cmd:read_aiger} -\begin{lstlisting}[numbers=left,frame=single] - read_aiger [options] [filename] - -Load module from an AIGER file into the current design. - - -module_name <module_name> - name of module to be created (default: <filename>) - - -clk_name <wire_name> - if specified, AIGER latches to be transformed into $_DFF_P_ cells - clocked by wire of this name. otherwise, $_FF_ cells will be used - - -map <filename> - read file with port and latch symbols - - -wideports - merge ports that match the pattern 'name[int]' into a single - multi-bit port 'name' - - -xaiger - read XAIGER extensions -\end{lstlisting} - -\section{read\_blif -- read BLIF file} -\label{cmd:read_blif} -\begin{lstlisting}[numbers=left,frame=single] - read_blif [options] [filename] - -Load modules from a BLIF file into the current design. - - -sop - Create $sop cells instead of $lut cells - - -wideports - Merge ports that match the pattern 'name[int]' into a single - multi-bit port 'name'. -\end{lstlisting} - -\section{read\_ilang -- (deprecated) alias of read\_rtlil} -\label{cmd:read_ilang} -\begin{lstlisting}[numbers=left,frame=single] -See `help read_rtlil`. -\end{lstlisting} - -\section{read\_json -- read JSON file} -\label{cmd:read_json} -\begin{lstlisting}[numbers=left,frame=single] - read_json [filename] - -Load modules from a JSON file into the current design See "help write_json" -for a description of the file format. -\end{lstlisting} - -\section{read\_liberty -- read cells from liberty file} -\label{cmd:read_liberty} -\begin{lstlisting}[numbers=left,frame=single] - read_liberty [filename] - -Read cells from liberty file as modules into current design. - - -lib - only create empty blackbox modules - - -wb - mark imported cells as whiteboxes - - -nooverwrite - ignore re-definitions of modules. (the default behavior is to - create an error message if the existing module is not a blackbox - module, and overwrite the existing module if it is a blackbox module.) - - -overwrite - overwrite existing modules with the same name - - -ignore_miss_func - ignore cells with missing function specification of outputs - - -ignore_miss_dir - ignore cells with a missing or invalid direction - specification on a pin - - -ignore_miss_data_latch - ignore latches with missing data and/or enable pins - - -setattr <attribute_name> - set the specified attribute (to the value 1) on all loaded modules -\end{lstlisting} - -\section{read\_rtlil -- read modules from RTLIL file} -\label{cmd:read_rtlil} -\begin{lstlisting}[numbers=left,frame=single] - read_rtlil [filename] - -Load modules from an RTLIL file to the current design. (RTLIL is a text -representation of a design in yosys's internal format.) - - -nooverwrite - ignore re-definitions of modules. (the default behavior is to - create an error message if the existing module is not a blackbox - module, and overwrite the existing module if it is a blackbox module.) - - -overwrite - overwrite existing modules with the same name - - -lib - only create empty blackbox modules -\end{lstlisting} - -\section{read\_verilog -- read modules from Verilog file} -\label{cmd:read_verilog} -\begin{lstlisting}[numbers=left,frame=single] - read_verilog [options] [filename] - -Load modules from a Verilog file to the current design. A large subset of -Verilog-2005 is supported. - - -sv - enable support for SystemVerilog features. (only a small subset - of SystemVerilog is supported) - - -formal - enable support for SystemVerilog assertions and some Yosys extensions - replace the implicit -D SYNTHESIS with -D FORMAL - - -nosynthesis - don't add implicit -D SYNTHESIS - - -noassert - ignore assert() statements - - -noassume - ignore assume() statements - - -norestrict - ignore restrict() statements - - -assume-asserts - treat all assert() statements like assume() statements - - -assert-assumes - treat all assume() statements like assert() statements - - -debug - alias for -dump_ast1 -dump_ast2 -dump_vlog1 -dump_vlog2 -yydebug - - -dump_ast1 - dump abstract syntax tree (before simplification) - - -dump_ast2 - dump abstract syntax tree (after simplification) - - -no_dump_ptr - do not include hex memory addresses in dump (easier to diff dumps) - - -dump_vlog1 - dump ast as Verilog code (before simplification) - - -dump_vlog2 - dump ast as Verilog code (after simplification) - - -dump_rtlil - dump generated RTLIL netlist - - -yydebug - enable parser debug output - - -nolatches - usually latches are synthesized into logic loops - this option prohibits this and sets the output to 'x' - in what would be the latches hold condition - - this behavior can also be achieved by setting the - 'nolatches' attribute on the respective module or - always block. - - -nomem2reg - under certain conditions memories are converted to registers - early during simplification to ensure correct handling of - complex corner cases. this option disables this behavior. - - this can also be achieved by setting the 'nomem2reg' - attribute on the respective module or register. - - This is potentially dangerous. Usually the front-end has good - reasons for converting an array to a list of registers. - Prohibiting this step will likely result in incorrect synthesis - results. - - -mem2reg - always convert memories to registers. this can also be - achieved by setting the 'mem2reg' attribute on the respective - module or register. - - -nomeminit - do not infer $meminit cells and instead convert initialized - memories to registers directly in the front-end. - - -ppdump - dump Verilog code after pre-processor - - -nopp - do not run the pre-processor - - -nodpi - disable DPI-C support - - -noblackbox - do not automatically add a (* blackbox *) attribute to an - empty module. - - -lib - only create empty blackbox modules. This implies -DBLACKBOX. - modules with the (* whitebox *) attribute will be preserved. - (* lib_whitebox *) will be treated like (* whitebox *). - - -nowb - delete (* whitebox *) and (* lib_whitebox *) attributes from - all modules. - - -specify - parse and import specify blocks - - -noopt - don't perform basic optimizations (such as const folding) in the - high-level front-end. - - -icells - interpret cell types starting with '$' as internal cell types - - -pwires - add a wire for each module parameter - - -nooverwrite - ignore re-definitions of modules. (the default behavior is to - create an error message if the existing module is not a black box - module, and overwrite the existing module otherwise.) - - -overwrite - overwrite existing modules with the same name - - -defer - only read the abstract syntax tree and defer actual compilation - to a later 'hierarchy' command. Useful in cases where the default - parameters of modules yield invalid or not synthesizable code. - - -noautowire - make the default of `default_nettype be "none" instead of "wire". - - -setattr <attribute_name> - set the specified attribute (to the value 1) on all loaded modules - - -Dname[=definition] - define the preprocessor symbol 'name' and set its optional value - 'definition' - - -Idir - add 'dir' to the directories which are used when searching include - files - -The command 'verilog_defaults' can be used to register default options for -subsequent calls to 'read_verilog'. - -Note that the Verilog frontend does a pretty good job of processing valid -verilog input, but has not very good error reporting. It generally is -recommended to use a simulator (for example Icarus Verilog) for checking -the syntax of the code, rather than to rely on read_verilog for that. - -Depending on if read_verilog is run in -formal mode, either the macro -SYNTHESIS or FORMAL is defined automatically, unless -nosynthesis is used. -In addition, read_verilog always defines the macro YOSYS. - -See the Yosys README file for a list of non-standard Verilog features -supported by the Yosys Verilog front-end. -\end{lstlisting} - -\section{rename -- rename object in the design} -\label{cmd:rename} -\begin{lstlisting}[numbers=left,frame=single] - rename old_name new_name - -Rename the specified object. Note that selection patterns are not supported -by this command. - - - - rename -output old_name new_name - -Like above, but also make the wire an output. This will fail if the object is -not a wire. - - - rename -src [selection] - -Assign names auto-generated from the src attribute to all selected wires and -cells with private names. - - - rename -wire [selection] [-suffix <suffix>] - -Assign auto-generated names based on the wires they drive to all selected -cells with private names. Ignores cells driving privatly named wires. -By default, the cell is named after the wire with the cell type as suffix. -The -suffix option can be used to set the suffix to the given string instead. - - - rename -enumerate [-pattern <pattern>] [selection] - -Assign short auto-generated names to all selected wires and cells with private -names. The -pattern option can be used to set the pattern for the new names. -The character % in the pattern is replaced with a integer number. The default -pattern is '_%_'. - - - rename -witness - -Assigns auto-generated names to all $any*/$all* output wires and containing -cells that do not have a public name. This ensures that, during formal -verification, a solver-found trace can be fully specified using a public -hierarchical names. - - - rename -hide [selection] - -Assign private names (the ones with $-prefix) to all selected wires and cells -with public names. This ignores all selected ports. - - - rename -top new_name - -Rename top module. - - - rename -scramble-name [-seed <seed>] [selection] - -Assign randomly-generated names to all selected wires and cells. The seed option -can be used to change the random number generator seed from the default, but it -must be non-zero. -\end{lstlisting} - -\section{rmports -- remove module ports with no connections} -\label{cmd:rmports} -\begin{lstlisting}[numbers=left,frame=single] - rmports [selection] - -This pass identifies ports in the selected modules which are not used or -driven and removes them. -\end{lstlisting} - -\section{sat -- solve a SAT problem in the circuit} -\label{cmd:sat} -\begin{lstlisting}[numbers=left,frame=single] - sat [options] [selection] - -This command solves a SAT problem defined over the currently selected circuit -and additional constraints passed as parameters. - - -all - show all solutions to the problem (this can grow exponentially, use - -max <N> instead to get <N> solutions) - - -max <N> - like -all, but limit number of solutions to <N> - - -enable_undef - enable modeling of undef value (aka 'x-bits') - this option is implied by -set-def, -set-undef et. cetera - - -max_undef - maximize the number of undef bits in solutions, giving a better - picture of which input bits are actually vital to the solution. - - -set <signal> <value> - set the specified signal to the specified value. - - -set-def <signal> - add a constraint that all bits of the given signal must be defined - - -set-any-undef <signal> - add a constraint that at least one bit of the given signal is undefined - - -set-all-undef <signal> - add a constraint that all bits of the given signal are undefined - - -set-def-inputs - add -set-def constraints for all module inputs - - -set-def-formal - add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells - - -show <signal> - show the model for the specified signal. if no -show option is - passed then a set of signals to be shown is automatically selected. - - -show-inputs, -show-outputs, -show-ports - add all module (input/output) ports to the list of shown signals - - -show-regs, -show-public, -show-all - show all registers, show signals with 'public' names, show all signals - - -ignore_div_by_zero - ignore all solutions that involve a division by zero - - -ignore_unknown_cells - ignore all cells that can not be matched to a SAT model - -The following options can be used to set up a sequential problem: - - -seq <N> - set up a sequential problem with <N> time steps. The steps will - be numbered from 1 to N. - - note: for large <N> it can be significantly faster to use - -tempinduct-baseonly -maxsteps <N> instead of -seq <N>. - - -set-at <N> <signal> <value> - -unset-at <N> <signal> - set or unset the specified signal to the specified value in the - given timestep. this has priority over a -set for the same signal. - - -set-assumes - set all assumptions provided via $assume cells - - -set-def-at <N> <signal> - -set-any-undef-at <N> <signal> - -set-all-undef-at <N> <signal> - add undef constraints in the given timestep. - - -set-init <signal> <value> - set the initial value for the register driving the signal to the value - - -set-init-undef - set all initial states (not set using -set-init) to undef - - -set-init-def - do not force a value for the initial state but do not allow undef - - -set-init-zero - set all initial states (not set using -set-init) to zero - - -dump_vcd <vcd-file-name> - dump SAT model (counter example in proof) to VCD file - - -dump_json <json-file-name> - dump SAT model (counter example in proof) to a WaveJSON file. - - -dump_cnf <cnf-file-name> - dump CNF of SAT problem (in DIMACS format). in temporal induction - proofs this is the CNF of the first induction step. - -The following additional options can be used to set up a proof. If also -seq -is passed, a temporal induction proof is performed. - - -tempinduct - Perform a temporal induction proof. In a temporal induction proof it is - proven that the condition holds forever after the number of time steps - specified using -seq. - - -tempinduct-def - Perform a temporal induction proof. Assume an initial state with all - registers set to defined values for the induction step. - - -tempinduct-baseonly - Run only the basecase half of temporal induction (requires -maxsteps) - - -tempinduct-inductonly - Run only the induction half of temporal induction - - -tempinduct-skip <N> - Skip the first <N> steps of the induction proof. - - note: this will assume that the base case holds for <N> steps. - this must be proven independently with "-tempinduct-baseonly - -maxsteps <N>". Use -initsteps if you just want to set a - minimal induction length. - - -prove <signal> <value> - Attempt to proof that <signal> is always <value>. - - -prove-x <signal> <value> - Like -prove, but an undef (x) bit in the lhs matches any value on - the right hand side. Useful for equivalence checking. - - -prove-asserts - Prove that all asserts in the design hold. - - -prove-skip <N> - Do not enforce the prove-condition for the first <N> time steps. - - -maxsteps <N> - Set a maximum length for the induction. - - -initsteps <N> - Set initial length for the induction. - This will speed up the search of the right induction length - for deep induction proofs. - - -stepsize <N> - Increase the size of the induction proof in steps of <N>. - This will speed up the search of the right induction length - for deep induction proofs. - - -timeout <N> - Maximum number of seconds a single SAT instance may take. - - -verify - Return an error and stop the synthesis script if the proof fails. - - -verify-no-timeout - Like -verify but do not return an error for timeouts. - - -falsify - Return an error and stop the synthesis script if the proof succeeds. - - -falsify-no-timeout - Like -falsify but do not return an error for timeouts. -\end{lstlisting} - -\section{scatter -- add additional intermediate nets} -\label{cmd:scatter} -\begin{lstlisting}[numbers=left,frame=single] - scatter [selection] - -This command adds additional intermediate nets on all cell ports. This is used -for testing the correct use of the SigMap helper in passes. If you don't know -what this means: don't worry -- you only need this pass when testing your own -extensions to Yosys. - -Use the opt_clean command to get rid of the additional nets. -\end{lstlisting} - -\section{scc -- detect strongly connected components (logic loops)} -\label{cmd:scc} -\begin{lstlisting}[numbers=left,frame=single] - scc [options] [selection] - -This command identifies strongly connected components (aka logic loops) in the -design. - - -expect <num> - expect to find exactly <num> SCCs. A different number of SCCs will - produce an error. - - -max_depth <num> - limit to loops not longer than the specified number of cells. This - can e.g. be useful in identifying small local loops in a module that - implements one large SCC. - - -nofeedback - do not count cells that have their output fed back into one of their - inputs as single-cell scc. - - -all_cell_types - Usually this command only considers internal non-memory cells. With - this option set, all cells are considered. For unknown cells all ports - are assumed to be bidirectional 'inout' ports. - - -set_attr <name> <value> - set the specified attribute on all cells that are part of a logic - loop. the special token {} in the value is replaced with a unique - identifier for the logic loop. - - -select - replace the current selection with a selection of all cells and wires - that are part of a found logic loop - - -specify - examine specify rules to detect logic loops in whitebox/blackbox cells -\end{lstlisting} - -\section{scratchpad -- get/set values in the scratchpad} -\label{cmd:scratchpad} -\begin{lstlisting}[numbers=left,frame=single] - scratchpad [options] - -This pass allows to read and modify values from the scratchpad of the current -design. Options: - - -get <identifier> - print the value saved in the scratchpad under the given identifier. - - -set <identifier> <value> - save the given value in the scratchpad under the given identifier. - - -unset <identifier> - remove the entry for the given identifier from the scratchpad. - - -copy <identifier_from> <identifier_to> - copy the value of the first identifier to the second identifier. - - -assert <identifier> <value> - assert that the entry for the given identifier is set to the given - value. - - -assert-set <identifier> - assert that the entry for the given identifier exists. - - -assert-unset <identifier> - assert that the entry for the given identifier does not exist. - -The identifier may not contain whitespace. By convention, it is usually prefixed -by the name of the pass that uses it, e.g. 'opt.did_something'. If the value -contains whitespace, it must be enclosed in double quotes. -\end{lstlisting} - -\section{script -- execute commands from file or wire} -\label{cmd:script} -\begin{lstlisting}[numbers=left,frame=single] - script <filename> [<from_label>:<to_label>] - script -scriptwire [selection] - -This command executes the yosys commands in the specified file (default -behaviour), or commands embedded in the constant text value connected to the -selected wires. - -In the default (file) case, the 2nd argument can be used to only execute the -section of the file between the specified labels. An empty from label is -synonymous with the beginning of the file and an empty to label is synonymous -with the end of the file. - -If only one label is specified (without ':') then only the block -marked with that label (until the next label) is executed. - -In "-scriptwire" mode, the commands on the selected wire(s) will be executed -in the scope of (and thus, relative to) the wires' owning module(s). This -'-module' mode can be exited by using the 'cd' command. -\end{lstlisting} - -\section{select -- modify and view the list of selected objects} -\label{cmd:select} -\begin{lstlisting}[numbers=left,frame=single] - select [ -add | -del | -set <name> ] {-read <filename> | <selection>} - select [ -unset <name> ] - select [ <assert_option> ] {-read <filename> | <selection>} - select [ -list | -write <filename> | -count | -clear ] - select -module <modname> - -Most commands use the list of currently selected objects to determine which part -of the design to operate on. This command can be used to modify and view this -list of selected objects. - -Note that many commands support an optional [selection] argument that can be -used to override the global selection for the command. The syntax of this -optional argument is identical to the syntax of the <selection> argument -described here. - - -add, -del - add or remove the given objects to the current selection. - without this options the current selection is replaced. - - -set <name> - do not modify the current selection. instead save the new selection - under the given name (see @<name> below). to save the current selection, - use "select -set <name> %" - - -unset <name> - do not modify the current selection. instead remove a previously saved - selection under the given name (see @<name> below). - - -assert-none - do not modify the current selection. instead assert that the given - selection is empty. i.e. produce an error if any object or module - matching the selection is found. - - -assert-any - do not modify the current selection. instead assert that the given - selection is non-empty. i.e. produce an error if no object or module - matching the selection is found. - - -assert-count N - do not modify the current selection. instead assert that the given - selection contains exactly N objects. - - -assert-max N - do not modify the current selection. instead assert that the given - selection contains less than or exactly N objects. - - -assert-min N - do not modify the current selection. instead assert that the given - selection contains at least N objects. - - -list - list all objects in the current selection - - -write <filename> - like -list but write the output to the specified file - - -read <filename> - read the specified file (written by -write) - - -count - count all objects in the current selection - - -clear - clear the current selection. this effectively selects the whole - design. it also resets the selected module (see -module). use the - command 'select *' to select everything but stay in the current module. - - -none - create an empty selection. the current module is unchanged. - - -module <modname> - limit the current scope to the specified module. - the difference between this and simply selecting the module - is that all object names are interpreted relative to this - module after this command until the selection is cleared again. - -When this command is called without an argument, the current selection -is displayed in a compact form (i.e. only the module name when a whole module -is selected). - -The <selection> argument itself is a series of commands for a simple stack -machine. Each element on the stack represents a set of selected objects. -After this commands have been executed, the union of all remaining sets -on the stack is computed and used as selection for the command. - -Pushing (selecting) object when not in -module mode: - - <mod_pattern> - select the specified module(s) - - <mod_pattern>/<obj_pattern> - select the specified object(s) from the module(s) - -Pushing (selecting) object when in -module mode: - - <obj_pattern> - select the specified object(s) from the current module - -By default, patterns will not match black/white-box modules or their -contents. To include such objects, prefix the pattern with '='. - -A <mod_pattern> can be a module name, wildcard expression (*, ?, [..]) -matching module names, or one of the following: - - A:<pattern>, A:<pattern>=<pattern> - all modules with an attribute matching the given pattern - in addition to = also <, <=, >=, and > are supported - - N:<pattern> - all modules with a name matching the given pattern - (i.e. 'N:' is optional as it is the default matching rule) - -An <obj_pattern> can be an object name, wildcard expression, or one of -the following: - - w:<pattern> - all wires with a name matching the given wildcard pattern - - i:<pattern>, o:<pattern>, x:<pattern> - all inputs (i:), outputs (o:) or any ports (x:) with matching names - - s:<size>, s:<min>:<max> - all wires with a matching width - - m:<pattern> - all memories with a name matching the given pattern - - c:<pattern> - all cells with a name matching the given pattern - - t:<pattern> - all cells with a type matching the given pattern - - p:<pattern> - all processes with a name matching the given pattern - - a:<pattern> - all objects with an attribute name matching the given pattern - - a:<pattern>=<pattern> - all objects with a matching attribute name-value-pair. - in addition to = also <, <=, >=, and > are supported - - r:<pattern>, r:<pattern>=<pattern> - cells with matching parameters. also with <, <=, >= and >. - - n:<pattern> - all objects with a name matching the given pattern - (i.e. 'n:' is optional as it is the default matching rule) - - @<name> - push the selection saved prior with 'select -set <name> ...' - -The following actions can be performed on the top sets on the stack: - - % - push a copy of the current selection to the stack - - %% - replace the stack with a union of all elements on it - - %n - replace top set with its invert - - %u - replace the two top sets on the stack with their union - - %i - replace the two top sets on the stack with their intersection - - %d - pop the top set from the stack and subtract it from the new top - - %D - like %d but swap the roles of two top sets on the stack - - %c - create a copy of the top set from the stack and push it - - %x[<num1>|*][.<num2>][:<rule>[:<rule>..]] - expand top set <num1> num times according to the specified rules. - (i.e. select all cells connected to selected wires and select all - wires connected to selected cells) The rules specify which cell - ports to use for this. the syntax for a rule is a '-' for exclusion - and a '+' for inclusion, followed by an optional comma separated - list of cell types followed by an optional comma separated list of - cell ports in square brackets. a rule can also be just a cell or wire - name that limits the expansion (is included but does not go beyond). - select at most <num2> objects. a warning message is printed when this - limit is reached. When '*' is used instead of <num1> then the process - is repeated until no further object are selected. - - %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]] - %co[<num1>|*][.<num2>][:<rule>[:<rule>..]] - similar to %x, but only select input (%ci) or output cones (%co) - - %xe[...] %cie[...] %coe - like %x, %ci, and %co but only consider combinatorial cells - - %a - expand top set by selecting all wires that are (at least in part) - aliases for selected wires. - - %s - expand top set by adding all modules that implement cells in selected - modules - - %m - expand top set by selecting all modules that contain selected objects - - %M - select modules that implement selected cells - - %C - select cells that implement selected modules - - %R[<num>] - select <num> random objects from top selection (default 1) - -Example: the following command selects all wires that are connected to a -'GATE' input of a 'SWITCH' cell: - - select */t:SWITCH %x:+[GATE] */t:SWITCH %d -\end{lstlisting} - -\section{setattr -- set/unset attributes on objects} -\label{cmd:setattr} -\begin{lstlisting}[numbers=left,frame=single] - setattr [ -mod ] [ -set name value | -unset name ]... [selection] - -Set/unset the given attributes on the selected objects. String values must be -passed in double quotes ("). - -When called with -mod, this command will set and unset attributes on modules -instead of objects within modules. -\end{lstlisting} - -\section{setparam -- set/unset parameters on objects} -\label{cmd:setparam} -\begin{lstlisting}[numbers=left,frame=single] - setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection] - -Set/unset the given parameters on the selected cells. String values must be -passed in double quotes ("). - -The -type option can be used to change the cell type of the selected cells. -\end{lstlisting} - -\section{setundef -- replace undef values with defined constants} -\label{cmd:setundef} -\begin{lstlisting}[numbers=left,frame=single] - setundef [options] [selection] - -This command replaces undef (x) constants with defined (0/1) constants. - - -undriven - also set undriven nets to constant values - - -expose - also expose undriven nets as inputs (use with -undriven) - - -zero - replace with bits cleared (0) - - -one - replace with bits set (1) - - -undef - replace with undef (x) bits, may be used with -undriven - - -anyseq - replace with $anyseq drivers (for formal) - - -anyconst - replace with $anyconst drivers (for formal) - - -random <seed> - replace with random bits using the specified integer as seed - value for the random number generator. - - -init - also create/update init values for flip-flops - - -params - replace undef in cell parameters -\end{lstlisting} - -\section{share -- perform sat-based resource sharing} -\label{cmd:share} -\begin{lstlisting}[numbers=left,frame=single] - share [options] [selection] - -This pass merges shareable resources into a single resource. A SAT solver -is used to determine if two resources are share-able. - - -force - Per default the selection of cells that is considered for sharing is - narrowed using a list of cell types. With this option all selected - cells are considered for resource sharing. - - IMPORTANT NOTE: If the -all option is used then no cells with internal - state must be selected! - - -aggressive - Per default some heuristics are used to reduce the number of cells - considered for resource sharing to only large resources. This options - turns this heuristics off, resulting in much more cells being considered - for resource sharing. - - -fast - Only consider the simple part of the control logic in SAT solving, resulting - in much easier SAT problems at the cost of maybe missing some opportunities - for resource sharing. - - -limit N - Only perform the first N merges, then stop. This is useful for debugging. -\end{lstlisting} - -\section{shell -- enter interactive command mode} -\label{cmd:shell} -\begin{lstlisting}[numbers=left,frame=single] - shell - -This command enters the interactive command mode. This can be useful -in a script to interrupt the script at a certain point and allow for -interactive inspection or manual synthesis of the design at this point. - -The command prompt of the interactive shell indicates the current -selection (see 'help select'): - - yosys> - the entire design is selected - - yosys*> - only part of the design is selected - - yosys [modname]> - the entire module 'modname' is selected using 'select -module modname' - - yosys [modname]*> - only part of current module 'modname' is selected - -When in interactive shell, some errors (e.g. invalid command arguments) -do not terminate yosys but return to the command prompt. - -This command is the default action if nothing else has been specified -on the command line. - -Press Ctrl-D or type 'exit' to leave the interactive shell. -\end{lstlisting} - -\section{show -- generate schematics using graphviz} -\label{cmd:show} -\begin{lstlisting}[numbers=left,frame=single] - show [options] [selection] - -Create a graphviz DOT file for the selected part of the design and compile it -to a graphics file (usually SVG or PostScript). - - -viewer <viewer> - Run the specified command with the graphics file as parameter. - On Windows, this pauses yosys until the viewer exits. - - -format <format> - Generate a graphics file in the specified format. Use 'dot' to just - generate a .dot file, or other <format> strings such as 'svg' or 'ps' - to generate files in other formats (this calls the 'dot' command). - - -lib <verilog_or_rtlil_file> - Use the specified library file for determining whether cell ports are - inputs or outputs. This option can be used multiple times to specify - more than one library. - - note: in most cases it is better to load the library before calling - show with 'read_verilog -lib <filename>'. it is also possible to - load liberty files with 'read_liberty -lib <filename>'. - - -prefix <prefix> - generate <prefix>.* instead of ~/.yosys_show.* - - -color <color> <object> - assign the specified color to the specified object. The object can be - a single selection wildcard expressions or a saved set of objects in - the @<name> syntax (see "help select" for details). - - -label <text> <object> - assign the specified label text to the specified object. The object can - be a single selection wildcard expressions or a saved set of objects in - the @<name> syntax (see "help select" for details). - - -colors <seed> - Randomly assign colors to the wires. The integer argument is the seed - for the random number generator. Change the seed value if the colored - graph still is ambiguous. A seed of zero deactivates the coloring. - - -colorattr <attribute_name> - Use the specified attribute to assign colors. A unique color is - assigned to each unique value of this attribute. - - -width - annotate buses with a label indicating the width of the bus. - - -signed - mark ports (A, B) that are declared as signed (using the [AB]_SIGNED - cell parameter) with an asterisk next to the port name. - - -stretch - stretch the graph so all inputs are on the left side and all outputs - (including inout ports) are on the right side. - - -pause - wait for the user to press enter to before returning - - -enum - enumerate objects with internal ($-prefixed) names - - -long - do not abbreviate objects with internal ($-prefixed) names - - -notitle - do not add the module name as graph title to the dot file - - -nobg - don't run viewer in the background, IE wait for the viewer tool to - exit before returning - -When no <format> is specified, 'dot' is used. When no <format> and <viewer> is -specified, 'xdot' is used to display the schematic (POSIX systems only). - -The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>', -unless another prefix is specified using -prefix <prefix>. - -Yosys on Windows and YosysJS use different defaults: The output is written -to 'show.dot' in the current directory and new viewer is launched each time -the 'show' command is executed. -\end{lstlisting} - -\section{shregmap -- map shift registers} -\label{cmd:shregmap} -\begin{lstlisting}[numbers=left,frame=single] - shregmap [options] [selection] - -This pass converts chains of $_DFF_[NP]_ gates to target specific shift register -primitives. The generated shift register will be of type $__SHREG_DFF_[NP]_ and -will use the same interface as the original $_DFF_*_ cells. The cell parameter -'DEPTH' will contain the depth of the shift register. Use a target-specific -'techmap' map file to convert those cells to the actual target cells. - - -minlen N - minimum length of shift register (default = 2) - (this is the length after -keep_before and -keep_after) - - -maxlen N - maximum length of shift register (default = no limit) - larger chains will be mapped to multiple shift register instances - - -keep_before N - number of DFFs to keep before the shift register (default = 0) - - -keep_after N - number of DFFs to keep after the shift register (default = 0) - - -clkpol pos|neg|any - limit match to only positive or negative edge clocks. (default = any) - - -enpol pos|neg|none|any_or_none|any - limit match to FFs with the specified enable polarity. (default = none) - - -match <cell_type>[:<d_port_name>:<q_port_name>] - match the specified cells instead of $_DFF_N_ and $_DFF_P_. If - ':<d_port_name>:<q_port_name>' is omitted then 'D' and 'Q' is used - by default. E.g. the option '-clkpol pos' is just an alias for - '-match $_DFF_P_', which is an alias for '-match $_DFF_P_:D:Q'. - - -params - instead of encoding the clock and enable polarity in the cell name by - deriving from the original cell name, simply name all generated cells - $__SHREG_ and use CLKPOL and ENPOL parameters. An ENPOL value of 2 is - used to denote cells without enable input. The ENPOL parameter is - omitted when '-enpol none' (or no -enpol option) is passed. - - -zinit - assume the shift register is automatically zero-initialized, so it - becomes legal to merge zero initialized FFs into the shift register. - - -init - map initialized registers to the shift reg, add an INIT parameter to - generated cells with the initialization value. (first bit to shift out - in LSB position) - - -tech greenpak4 - map to greenpak4 shift registers. -\end{lstlisting} - -\section{sim -- simulate the circuit} -\label{cmd:sim} -\begin{lstlisting}[numbers=left,frame=single] - sim [options] [top-level] - -This command simulates the circuit using the given top-level module. - - -vcd <filename> - write the simulation results to the given VCD file - - -fst <filename> - write the simulation results to the given FST file - - -aiw <filename> - write the simulation results to an AIGER witness file - (requires a *.aim file via -map) - - -hdlname - use the hdlname attribute when writing simulation results - (preserves hierarchy in a flattened design) - - -x - ignore constant x outputs in simulation file. - - -date - include date and full version info in output. - - -clock <portname> - name of top-level clock input - - -clockn <portname> - name of top-level clock input (inverse polarity) - - -multiclock - mark that witness file is multiclock. - - -reset <portname> - name of top-level reset input (active high) - - -resetn <portname> - name of top-level inverted reset input (active low) - - -rstlen <integer> - number of cycles reset should stay active (default: 1) - - -zinit - zero-initialize all uninitialized regs and memories - - -timescale <string> - include the specified timescale declaration in the vcd - - -n <integer> - number of clock cycles to simulate (default: 20) - - -a - use all nets in VCD/FST operations, not just those with public names - - -w - writeback mode: use final simulation state as new init state - - -r - read simulation results file - File formats supported: FST, VCD, AIW and WIT - VCD support requires vcd2fst external tool to be present - - -map <filename> - read file with port and latch symbols, needed for AIGER witness input - - -scope <name> - scope of simulation top model - - -at <time> - sets start and stop time - - -start <time> - start co-simulation in arbitary time (default 0) - - -stop <time> - stop co-simulation in arbitary time (default END) - - -sim - simulation with stimulus from FST (default) - - -sim-cmp - co-simulation expect exact match - - -sim-gold - co-simulation, x in simulation can match any value in FST - - -sim-gate - co-simulation, x in FST can match any value in simulation - - -q - disable per-cycle/sample log message - - -d - enable debug output -\end{lstlisting} - -\section{simplemap -- mapping simple coarse-grain cells} -\label{cmd:simplemap} -\begin{lstlisting}[numbers=left,frame=single] - simplemap [selection] - -This pass maps a small selection of simple coarse-grain cells to yosys gate -primitives. The following internal cell types are mapped by this pass: - - $not, $pos, $and, $or, $xor, $xnor - $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool - $logic_not, $logic_and, $logic_or, $mux, $tribuf - $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff, - $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr -\end{lstlisting} - -\section{splice -- create explicit splicing cells} -\label{cmd:splice} -\begin{lstlisting}[numbers=left,frame=single] - splice [options] [selection] - -This command adds $slice and $concat cells to the design to make the splicing -of multi-bit signals explicit. This for example is useful for coarse grain -synthesis, where dedicated hardware is needed to splice signals. - - -sel_by_cell - only select the cell ports to rewire by the cell. if the selection - contains a cell, than all cell inputs are rewired, if necessary. - - -sel_by_wire - only select the cell ports to rewire by the wire. if the selection - contains a wire, than all cell ports driven by this wire are wired, - if necessary. - - -sel_any_bit - it is sufficient if the driver of any bit of a cell port is selected. - by default all bits must be selected. - - -wires - also add $slice and $concat cells to drive otherwise unused wires. - - -no_outputs - do not rewire selected module outputs. - - -port <name> - only rewire cell ports with the specified name. can be used multiple - times. implies -no_output. - - -no_port <name> - do not rewire cell ports with the specified name. can be used multiple - times. can not be combined with -port <name>. - -By default selected output wires and all cell ports of selected cells driven -by selected wires are rewired. -\end{lstlisting} - -\section{splitnets -- split up multi-bit nets} -\label{cmd:splitnets} -\begin{lstlisting}[numbers=left,frame=single] - splitnets [options] [selection] - -This command splits multi-bit nets into single-bit nets. - - -format char1[char2[char3]] - the first char is inserted between the net name and the bit index, the - second char is appended to the netname. e.g. -format () creates net - names like 'mysignal(42)'. the 3rd character is the range separation - character when creating multi-bit wires. the default is '[]:'. - - -ports - also split module ports. per default only internal signals are split. - - -driver - don't blindly split nets in individual bits. instead look at the driver - and split nets so that no driver drives only part of a net. -\end{lstlisting} - -\section{sta -- perform static timing analysis} -\label{cmd:sta} -\begin{lstlisting}[numbers=left,frame=single] - sta [options] [selection] - -This command performs static timing analysis on the design. (Only considers -paths within a single module, so the design must be flattened.) -\end{lstlisting} - -\section{stat -- print some statistics} -\label{cmd:stat} -\begin{lstlisting}[numbers=left,frame=single] - stat [options] [selection] - -Print some statistics (number of objects) on the selected portion of the -design. - - -top <module> - print design hierarchy with this module as top. if the design is fully - selected and a module has the 'top' attribute set, this module is used - default value for this option. - - -liberty <liberty_file> - use cell area information from the provided liberty file - - -tech <technology> - print area estemate for the specified technology. Currently supported - values for <technology>: xilinx, cmos - - -width - annotate internal cell types with their word width. - e.g. $add_8 for an 8 bit wide $add cell. - - -json - output the statistics in a machine-readable JSON format. - this is output to the console; use "tee" to output to a file. -\end{lstlisting} - -\section{submod -- moving part of a module to a new submodule} -\label{cmd:submod} -\begin{lstlisting}[numbers=left,frame=single] - submod [options] [selection] - -This pass identifies all cells with the 'submod' attribute and moves them to -a newly created module. The value of the attribute is used as name for the -cell that replaces the group of cells with the same attribute value. - -This pass can be used to create a design hierarchy in flat design. This can -be useful for analyzing or reverse-engineering a design. - -This pass only operates on completely selected modules with no processes -or memories. - - -copy - by default the cells are 'moved' from the source module and the source - module will use an instance of the new module after this command is - finished. call with -copy to not modify the source module. - - -name <name> - don't use the 'submod' attribute but instead use the selection. only - objects from one module might be selected. the value of the -name option - is used as the value of the 'submod' attribute instead. - - -hidden - instead of creating submodule ports with public names, create ports with - private names so that a subsequent 'flatten; clean' call will restore - the original module with original public names. -\end{lstlisting} - -\section{supercover -- add hi/lo cover cells for each wire bit} -\label{cmd:supercover} -\begin{lstlisting}[numbers=left,frame=single] - supercover [options] [selection] - -This command adds two cover cells for each bit of each selected wire, one -checking for a hi signal level and one checking for lo level. -\end{lstlisting} - -\section{synth -- generic synthesis script} -\label{cmd:synth} -\begin{lstlisting}[numbers=left,frame=single] - synth [options] - -This command runs the default synthesis script. This command does not operate -on partly selected designs. - - -top <module> - use the specified module as top module (default='top') - - -auto-top - automatically determine the top of the design hierarchy - - -flatten - flatten the design before synthesis. this will pass '-auto-top' to - 'hierarchy' if no top module is specified. - - -encfile <file> - passed to 'fsm_recode' via 'fsm' - - -lut <k> - perform synthesis for a k-LUT architecture. - - -nofsm - do not run FSM optimization - - -noabc - do not run abc (as if yosys was compiled without ABC support) - - -noalumacc - do not run 'alumacc' pass. i.e. keep arithmetic operators in - their direct form ($add, $sub, etc.). - - -nordff - passed to 'memory'. prohibits merging of FFs into memory read ports - - -noshare - do not run SAT-based resource sharing - - -run <from_label>[:<to_label>] - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - - -flowmap - use FlowMap LUT techmapping instead of ABC - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). - - -The following commands are executed by this synthesis command: - - begin: - hierarchy -check [-top <top> | -auto-top] - - coarse: - proc - flatten (if -flatten) - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm (unless -nofsm) - opt - wreduce - peepopt - opt_clean - techmap -map +/cmp2lut.v -map +/cmp2lcu.v (if -lut) - alumacc (unless -noalumacc) - share (unless -noshare) - opt - memory -nomap - opt_clean - - fine: - opt -fast -full - memory_map - opt -full - techmap - techmap -map +/gate2lut.v (if -noabc and -lut) - clean; opt_lut (if -noabc and -lut) - flowmap -maxlut K (if -flowmap and -lut) - opt -fast - abc -fast (unless -noabc, unless -lut) - abc -fast -lut k (unless -noabc, if -lut) - opt -fast (unless -noabc) - - check: - hierarchy -check - stat - check -\end{lstlisting} - -\section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.} -\label{cmd:synth_achronix} -\begin{lstlisting}[numbers=left,frame=single] - synth_achronix [options] - -This command runs synthesis for Achronix Speedster eFPGAs. This work is still experimental. - - -top <module> - use the specified module as top module (default='top') - - -vout <file> - write the design to the specified Verilog netlist file. writing of an - output file is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -sv -lib +/achronix/speedster22i/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse - - fine: - opt -fast -mux_undef -undriven -fine -full - memory_map - opt -undriven -fine - opt -fine - techmap -map +/techmap.v - opt -full - clean -purge - setundef -undriven -zero - dfflegalize -cell $_DFF_P_ x - abc -markgroups -dff -D 1 (only if -retime) - - map_luts: - abc -lut 4 - clean - - map_cells: - iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I - techmap -map +/achronix/speedster22i/cells_map.v - clean -purge - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - vout: - write_verilog -nodec -attr2comment -defparam -renameprefix syn_ <file-name> -\end{lstlisting} - -\section{synth\_anlogic -- synthesis for Anlogic FPGAs} -\label{cmd:synth_anlogic} -\begin{lstlisting}[numbers=left,frame=single] - synth_anlogic [options] - -This command runs synthesis for Anlogic FPGAs. - - -top <module> - use the specified module as top module - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -nolutram - do not use EG_LOGIC_DRAM16X4 cells in output netlist - - -nobram - do not use EG_PHY_BRAM or EG_PHY_BRAM32K cells in output netlist - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib +/anlogic/cells_sim.v +/anlogic/eagle_bb.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse - - map_ram: - memory_libmap -lib +/anlogic/lutrams.txt -lib +/anlogic/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram) - techmap -map +/anlogic/lutrams_map.v -map +/anlogic/brams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/anlogic/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - - map_ffs: - dfflegalize -cell $_DFFE_P??P_ r -cell $_SDFFE_P??P_ r -cell $_DLATCH_N??_ r - techmap -D NO_LUT -map +/anlogic/cells_map.v - opt_expr -mux_undef - simplemap - - map_luts: - abc -lut 4:6 - clean - - map_cells: - techmap -map +/anlogic/cells_map.v - clean - - map_anlogic: - anlogic_fixcarry - anlogic_eqn - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - edif: - write_edif <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs} -\label{cmd:synth_coolrunner2} -\begin{lstlisting}[numbers=left,frame=single] - synth_coolrunner2 [options] - -This command runs synthesis for Coolrunner-II CPLDs. This work is experimental. -It is intended to be used with https://github.com/azonenberg/openfpga as the -place-and-route. - - -top <module> - use the specified module as top module (default='top') - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib +/coolrunner2/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - - coarse: - synth -run coarse - - fine: - extract_counter -dir up -allow_arst no - techmap -map +/coolrunner2/cells_counter_map.v - clean - opt -fast -full - techmap -map +/techmap.v -map +/coolrunner2/cells_latch.v - opt -fast - dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib - - map_tff: - abc -g AND,XOR - clean - extract -map +/coolrunner2/tff_extract.v - - map_pla: - abc -sop -I 40 -P 56 - clean - - map_cells: - dfflibmap -liberty +/coolrunner2/xc2_dff.lib - dffinit -ff FDCP Q INIT - dffinit -ff FDCP_N Q INIT - dffinit -ff FTCP Q INIT - dffinit -ff FTCP_N Q INIT - dffinit -ff LDCP Q INIT - dffinit -ff LDCP_N Q INIT - coolrunner2_sop - clean - iopadmap -bits -inpad IBUF O:I -outpad IOBUFE I:IO -inoutpad IOBUFE O:IO -toutpad IOBUFE E:I:IO -tinoutpad IOBUFE E:O:I:IO - attrmvcp -attr src -attr LOC t:IOBUFE n:* - attrmvcp -attr src -attr LOC -driven t:IBUF n:* - coolrunner2_fixup - splitnets - clean - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_easic -- synthesis for eASIC platform} -\label{cmd:synth_easic} -\begin{lstlisting}[numbers=left,frame=single] - synth_easic [options] - -This command runs synthesis for eASIC platform. - - -top <module> - use the specified module as top module - - -vlog <file> - write the design to the specified structural Verilog file. writing of - an output file is omitted if this parameter is not specified. - - -etools <path> - set path to the eTools installation. (default=/opt/eTools) - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -The following commands are executed by this synthesis command: - - begin: - read_liberty -lib <etools_phys_clk_lib> - read_liberty -lib <etools_logic_lut_lib> - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - - coarse: - synth -run coarse - - fine: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - techmap - opt -fast - abc -dff -D 1 (only if -retime) - opt_clean (only if -retime) - - map: - dfflibmap -liberty <etools_phys_clk_lib> - abc -liberty <etools_logic_lut_lib> - opt_clean - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - vlog: - write_verilog -noexpr -attr2comment <file-name> -\end{lstlisting} - -\section{synth\_ecp5 -- synthesis for ECP5 FPGAs} -\label{cmd:synth_ecp5} -\begin{lstlisting}[numbers=left,frame=single] - synth_ecp5 [options] - -This command runs synthesis for ECP5 FPGAs. - - -top <module> - use the specified module as top module - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -dff - run 'abc'/'abc9' with -dff option - - -retime - run 'abc' with '-dff -D 1' options - - -noccu2 - do not use CCU2 cells in output netlist - - -nodffe - do not use flipflops with CE in output netlist - - -nobram - do not use block RAM cells in output netlist - - -nolutram - do not use LUT RAM cells in output netlist - - -nowidelut - do not use PFU muxes to implement LUTs larger than LUT4s - - -asyncprld - use async PRLD mode to implement ALDFF (EXPERIMENTAL) - - -abc2 - run two passes of 'abc' for slightly improved logic density - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - - -vpr - generate an output netlist (and BLIF file) suitable for VPR - (this feature is experimental and incomplete) - - -nodsp - do not map multipliers to MULT18X18D - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -specify +/ecp5/cells_sim.v +/ecp5/cells_bb.v - hierarchy -check -top <top> - - coarse: - proc - flatten - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=4 - opt_expr - opt_clean - techmap -map +/mul2dsp.v -map +/ecp5/dsp_map.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_NAME=$__MUL18X18 (unless -nodsp) - chtype -set $mul t:$__soft_mul (unless -nodsp) - alumacc - opt - memory -nomap [-no-rw-check] - opt_clean - - map_ram: - memory_libmap -lib +/ecp5/lutrams.txt -lib +/ecp5/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram) - techmap -map +/ecp5/lutrams_map.v -map +/ecp5/brams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/ecp5/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - - map_ffs: - opt_clean - dfflegalize -cell $_DFF_?_ 01 -cell $_DFF_?P?_ r -cell $_SDFF_?P?_ r [-cell $_DFFE_??_ 01 -cell $_DFFE_?P??_ r -cell $_SDFFE_?P??_ r] [-cell $_ALDFF_?P_ x -cell $_ALDFFE_?P?_ x] [-cell $_DLATCH_?_ x] ($_ALDFF_*_ only if -asyncprld, $_DLATCH_* only if not -asyncprld, $_*DFFE_* only if not -nodffe) - zinit -all w:* t:$_DFF_?_ t:$_DFFE_??_ t:$_SDFF* (only if -abc9 and -dff) - techmap -D NO_LUT -map +/ecp5/cells_map.v - opt_expr -undriven -mux_undef - simplemap - ecp5_gsr - attrmvcp -copy -attr syn_useioff - opt_clean - - map_luts: - abc (only if -abc2) - techmap -map +/ecp5/latches_map.v (skip if -asyncprld) - abc -dress -lut 4:7 - clean - - map_cells: - techmap -map +/ecp5/cells_map.v (skip if -vpr) - opt_lut_ins -tech ecp5 - clean - - check: - autoname - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - blif: - opt_clean -purge (vpr mode) - write_blif -attr -cname -conn -param <file-name> (vpr mode) - write_blif -gates -attr -param <file-name> (non-vpr mode) - - edif: - write_edif <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_efinix -- synthesis for Efinix FPGAs} -\label{cmd:synth_efinix} -\begin{lstlisting}[numbers=left,frame=single] - synth_efinix [options] - -This command runs synthesis for Efinix FPGAs. - - -top <module> - use the specified module as top module - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -nobram - do not use EFX_RAM_5K cells in output netlist - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib +/efinix/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse - - map_ram: - memory_libmap -lib +/efinix/brams.txt - techmap -map +/efinix/brams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/efinix/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - - map_ffs: - dfflegalize -cell $_DFFE_????_ 0 -cell $_SDFFE_????_ 0 -cell $_SDFFCE_????_ 0 -cell $_DLATCH_?_ x - techmap -D NO_LUT -map +/efinix/cells_map.v - opt_expr -mux_undef - simplemap - - map_luts: - abc -lut 4 - clean - - map_cells: - techmap -map +/efinix/cells_map.v - clean - - map_gbuf: - clkbufmap -buf $__EFX_GBUF O:I - techmap -map +/efinix/gbuf_map.v - efinix_fixcarry - clean - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - edif: - write_edif <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_fabulous -- FABulous synthesis script} -\label{cmd:synth_fabulous} -\begin{lstlisting}[numbers=left,frame=single] - synth_fabulous [options] - -This command runs synthesis for FPGA fabrics generated with FABulous. This command does not operate -on partly selected designs. - - -top <module> - use the specified module as top module (default='top') - - -auto-top - automatically determine the top of the design hierarchy - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -lut <k> - perform synthesis for a k-LUT architecture (default 4). - - -vpr - perform synthesis for the FABulous VPR flow (using slightly different techmapping). - - -plib <primitive_library.v> - use the specified Verilog file as a primitive library. - - -extra-plib <primitive_library.v> - use the specified Verilog file for extra primitives (can be specified multiple - times). - - -extra-map <techamp.v> - use the specified Verilog file for extra techmap rules (can be specified multiple - times). - - -encfile <file> - passed to 'fsm_recode' via 'fsm' - - -nofsm - do not run FSM optimization - - -noalumacc - do not run 'alumacc' pass. i.e. keep arithmetic operators in - their direct form ($add, $sub, etc.). - - -noregfile - do not map register files - - -iopad - enable automatic insertion of IO buffers (otherwise a wrapper - with manually inserted and constrained IO should be used.) - - -complex-dff - enable support for FFs with enable and synchronous SR (must also be - supported by the target fabric.) - - -noflatten - do not flatten design after elaboration - - -nordff - passed to 'memory'. prohibits merging of FFs into memory read ports - - -noshare - do not run SAT-based resource sharing - - -run <from_label>[:<to_label>] - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). - - -The following commands are executed by this synthesis command: - read_verilog -lib +/fabulous/prims.v - read_verilog -lib <extra_plib.v> (for each -extra-plib) - - begin: - hierarchy -check - proc - - flatten: (unless -noflatten) - flatten - tribuf -logic - deminout - - coarse: - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm (unless -nofsm) - opt - wreduce - peepopt - opt_clean - techmap -map +/cmp2lut.v -map +/cmp2lcu.v (if -lut) - alumacc (unless -noalumacc) - share (unless -noshare) - opt - memory -nomap - opt_clean - - map_ram: - memory_libmap -lib +/fabulous/ram_regfile.txt - techmap -map +/fabulous/regfile_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - opt -full - techmap -map +/techmap.v - opt -fast - - map_iopad: (if -iopad) - - map_ffs: - dfflegalize -cell $_DFF_P_ 0 -cell $_DLATCH_?_ x without -complex-dff - techmap -map +/fabulous/latches_map.v - techmap -map +/fabulous/ff_map.v - techmap -map <extra_map.v>... (for each -extra-map) - clean - - map_luts: - abc -lut 4 -dress - clean - - map_cells: - techmap -D LUT_K=4 -map +/fabulous/cells_map.v - clean - - check: - hierarchy -check - stat - - blif: - opt_clean -purge - write_blif -attr -cname -conn -param <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_gatemate -- synthesis for Cologne Chip GateMate FPGAs} -\label{cmd:synth_gatemate} -\begin{lstlisting}[numbers=left,frame=single] - synth_gatemate [options] - -This command runs synthesis for Cologne Chip AG GateMate FPGAs. - - -top <module> - use the specified module as top module. - - -vlog <file> - write the design to the specified verilog file. Writing of an output - file is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. Writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). An empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis. - - -nobram - do not use CC_BRAM_20K or CC_BRAM_40K cells in output netlist. - - -noaddf - do not use CC_ADDF full adder cells in output netlist. - - -nomult - do not use CC_MULT multiplier cells in output netlist. - - -nomx8, -nomx4 - do not use CC_MX{8,4} multiplexer cells in output netlist. - - -luttree - use new LUT tree mapping approach (EXPERIMENTAL). - - -dff - run 'abc' with -dff option - - -retime - run 'abc' with '-dff -D 1' options - - -noiopad - disable I/O buffer insertion (useful for hierarchical or - out-of-context flows). - - -noclkbuf - disable automatic clock buffer insertion. - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -specify +/gatemate/cells_sim.v +/gatemate/cells_bb.v - hierarchy -check -top <top> - - prepare: - proc - flatten - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - muxpack - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=4 - opt_expr - opt_clean - - map_mult: (skip if '-nomult') - techmap -map +/gatemate/mul_map.v - - coarse: - alumacc - opt - memory -nomap - opt_clean - - map_bram: (skip if '-nobram') - memory_libmap -lib +/gatemate/brams.txt - techmap -map +/gatemate/brams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/gatemate/arith_map.v - opt -fast - - map_io: (skip if '-noiopad') - iopadmap -bits -inpad CC_IBUF Y:I -outpad CC_OBUF A:O -toutpad CC_TOBUF ~T:A:O -tinoutpad CC_IOBUF ~T:Y:A:IO - clean - - map_regs: - opt_clean - dfflegalize -cell $_DFFE_????_ x -cell $_DLATCH_???_ x - techmap -map +/gatemate/reg_map.v - opt_expr -mux_undef - simplemap - opt_clean - - map_muxs: - muxcover -mux4 -mux8 - opt -full - techmap -map +/gatemate/mux_map.v - - map_luts: - abc -genlib +/gatemate/lut_tree_cells.genlib (with -luttree) - techmap -map +/gatemate/lut_tree_map.v (with -luttree) - gatemate_foldinv (with -luttree) - techmap -map +/gatemate/inv_map.v (with -luttree) - abc -dress -lut 4 (without -luttree) - clean - - map_cells: - techmap -map +/gatemate/lut_map.v - clean - - map_bufg: (skip if '-noclkbuf') - clkbufmap -buf CC_BUFG O:I - clean - - check: - hierarchy -check - stat -width - check -noinit - blackbox =A:whitebox - - vlog: - opt_clean -purge - write_verilog -noattr <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_gowin -- synthesis for Gowin FPGAs} -\label{cmd:synth_gowin} -\begin{lstlisting}[numbers=left,frame=single] - synth_gowin [options] - -This command runs synthesis for Gowin FPGAs. This work is experimental. - - -top <module> - use the specified module as top module (default='top') - - -vout <file> - write the design to the specified Verilog netlist file. writing of an - output file is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON netlist file. writing of an - output file is omitted if this parameter is not specified. - This disables features not yet supported by nexpnr-gowin. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -nodffe - do not use flipflops with CE in output netlist - - -nobram - do not use BRAM cells in output netlist - - -nolutram - do not use distributed RAM cells in output netlist - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -nowidelut - do not use muxes to implement LUTs larger than LUT4s - - -noiopads - do not emit IOB at top level ports - - -noalu - do not use ALU cells - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -specify -lib +/gowin/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse [-no-rw-check] - - map_ram: - memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram) - techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/gowin/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - iopadmap -bits -inpad IBUF O:I -outpad OBUF I:O -toutpad TBUF ~OEN:I:O -tinoutpad IOBUF ~OEN:O:I:IO (unless -noiopads) - - map_ffs: - opt_clean - dfflegalize -cell $_DFF_?_ 0 -cell $_DFFE_?P_ 0 -cell $_SDFF_?P?_ r -cell $_SDFFE_?P?P_ r -cell $_DFF_?P?_ r -cell $_DFFE_?P?P_ r - techmap -map +/gowin/cells_map.v - opt_expr -mux_undef - simplemap - - map_luts: - abc -lut 4:8 - clean - - map_cells: - techmap -map +/gowin/cells_map.v - opt_lut_ins -tech gowin - setundef -undriven -params -zero - hilomap -singleton -hicell VCC V -locell GND G - splitnets -ports (only if -vout used) - clean - autoname - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - vout: - write_verilog -simple-lhs -decimal -attr2comment -defparam -renameprefix gen <file-name> - write_json <file-name> -\end{lstlisting} - -\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs} -\label{cmd:synth_greenpak4} -\begin{lstlisting}[numbers=left,frame=single] - synth_greenpak4 [options] - -This command runs synthesis for GreenPAK4 FPGAs. This work is experimental. -It is intended to be used with https://github.com/azonenberg/openfpga as the -place-and-route. - - -top <module> - use the specified module as top module (default='top') - - -part <part> - synthesize for the specified part. Valid values are SLG46140V, - SLG46620V, and SLG46621V (default). - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib +/greenpak4/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - - coarse: - synth -run coarse - - fine: - extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14 - clean - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - techmap -map +/techmap.v -map +/greenpak4/cells_latch.v - dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib - opt -fast -noclkinv -noff - abc -dff -D 1 (only if -retime) - - map_luts: - nlutmap -assert -luts 0,6,8,2 (for -part SLG46140V) - nlutmap -assert -luts 2,8,16,2 (for -part SLG46620V) - nlutmap -assert -luts 2,8,16,2 (for -part SLG46621V) - clean - - map_cells: - shregmap -tech greenpak4 - dfflibmap -liberty +/greenpak4/gp_dff.lib - dffinit -ff GP_DFF Q INIT - dffinit -ff GP_DFFR Q INIT - dffinit -ff GP_DFFS Q INIT - dffinit -ff GP_DFFSR Q INIT - iopadmap -bits -inpad GP_IBUF OUT:IN -outpad GP_OBUF IN:OUT -inoutpad GP_OBUF OUT:IN -toutpad GP_OBUFT OE:IN:OUT -tinoutpad GP_IOBUF OE:OUT:IN:IO - attrmvcp -attr src -attr LOC t:GP_OBUF t:GP_OBUFT t:GP_IOBUF n:* - attrmvcp -attr src -attr LOC -driven t:GP_IBUF n:* - techmap -map +/greenpak4/cells_map.v - greenpak4_dffinv - clean - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_ice40 -- synthesis for iCE40 FPGAs} -\label{cmd:synth_ice40} -\begin{lstlisting}[numbers=left,frame=single] - synth_ice40 [options] - -This command runs synthesis for iCE40 FPGAs. - - -device < hx | lp | u > - relevant only for '-abc9' flow, optimise timing for the specified - device. default: hx - - -top <module> - use the specified module as top module - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -dff - run 'abc'/'abc9' with -dff option - - -retime - run 'abc' with '-dff -D 1' options - - -nocarry - do not use SB_CARRY cells in output netlist - - -nodffe - do not use SB_DFFE* cells in output netlist - - -dffe_min_ce_use <min_ce_use> - do not use SB_DFFE* cells if the resulting CE line would go to less - than min_ce_use SB_DFFE* in output netlist - - -nobram - do not use SB_RAM40_4K* cells in output netlist - - -spram - enable automatic inference of SB_SPRAM256KA - - -dsp - use iCE40 UltraPlus DSP cells for large arithmetic - - -noabc - use built-in Yosys LUT techmapping instead of abc - - -abc2 - run two passes of 'abc' for slightly improved logic density - - -vpr - generate an output netlist (and BLIF file) suitable for VPR - (this feature is experimental and incomplete) - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - - -flowmap - use FlowMap LUT techmapping instead of abc (EXPERIMENTAL) - - -no-rw-check - marks all recognized read ports as "return don't-care value on - read/write collision" (same result as setting the no_rw_check - attribute on all memories). - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -D ICE40_HX -lib -specify +/ice40/cells_sim.v - hierarchy -check -top <top> - proc - - flatten: (unless -noflatten) - flatten - tribuf -logic - deminout - - coarse: - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=4 - opt_expr - opt_clean - memory_dff [-no-rw-check] - wreduce t:$mul - techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 -D DSP_NAME=$__MUL16X16 (if -dsp) - select a:mul2dsp (if -dsp) - setattr -unset mul2dsp (if -dsp) - opt_expr -fine (if -dsp) - wreduce (if -dsp) - select -clear (if -dsp) - ice40_dsp (if -dsp) - chtype -set $mul t:$__soft_mul (if -dsp) - alumacc - opt - memory -nomap [-no-rw-check] - opt_clean - - map_ram: - memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge [-no-auto-huge] [-no-auto-block] (-no-auto-huge unless -spram, -no-auto-block if -nobram) - techmap -map +/ice40/brams_map.v -map +/ice40/spram_map.v - ice40_braminit - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - ice40_wrapcarry - techmap -map +/techmap.v -map +/ice40/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - ice40_opt - - map_ffs: - dfflegalize -cell $_DFF_?_ 0 -cell $_DFFE_?P_ 0 -cell $_DFF_?P?_ 0 -cell $_DFFE_?P?P_ 0 -cell $_SDFF_?P?_ 0 -cell $_SDFFCE_?P?P_ 0 -cell $_DLATCH_?_ x -mince -1 - techmap -map +/ice40/ff_map.v - opt_expr -mux_undef - simplemap - ice40_opt -full - - map_luts: - abc (only if -abc2) - ice40_opt (only if -abc2) - techmap -map +/ice40/latches_map.v - simplemap (if -noabc or -flowmap) - techmap -map +/gate2lut.v -D LUT_WIDTH=4 (only if -noabc) - flowmap -maxlut 4 (only if -flowmap) - abc -dress -lut 4 (skip if -noabc) - ice40_wrapcarry -unwrap - techmap -map +/ice40/ff_map.v - clean - opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3 -dlogic SB_CARRY:CO=3 - - map_cells: - techmap -map +/ice40/cells_map.v (skip if -vpr) - clean - - check: - autoname - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - blif: - opt_clean -purge (vpr mode) - write_blif -attr -cname -conn -param <file-name> (vpr mode) - write_blif -gates -attr -param <file-name> (non-vpr mode) - - edif: - write_edif <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_intel -- synthesis for Intel (Altera) FPGAs.} -\label{cmd:synth_intel} -\begin{lstlisting}[numbers=left,frame=single] - synth_intel [options] - -This command runs synthesis for Intel FPGAs. - - -family <max10 | cyclone10lp | cycloneiv | cycloneive> - generate the synthesis netlist for the specified family. - MAX10 is the default target if no family argument specified. - For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use - cycloneive. For Cyclone V and Cyclone 10 GX, use the synth_intel_alm - backend instead. - - -top <module> - use the specified module as top module (default='top') - - -vqm <file> - write the design to the specified Verilog Quartus Mapping File. Writing - of an output file is omitted if this parameter is not specified. - Note that this backend has not been tested and is likely incompatible - with recent versions of Quartus. - - -vpr <file> - write BLIF files for VPR flow experiments. The synthesized BLIF output - file is not compatible with the Quartus flow. Writing of an - output file is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -iopads - use IO pad cells in output netlist - - -nobram - do not use block RAM cells in output netlist - - -noflatten - do not flatten design before synthesis - - -retime - run 'abc' with '-dff -D 1' options - -The following commands are executed by this synthesis command: - - begin: - - family: - read_verilog -sv -lib +/intel/max10/cells_sim.v - read_verilog -sv -lib +/intel/common/m9k_bb.v - read_verilog -sv -lib +/intel/common/altpll_bb.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse - - map_bram: (skip if -nobram) - memory_bram -rules +/intel/common/brams_m9k.txt (if applicable for family) - techmap -map +/intel/common/brams_map_m9k.v (if applicable for family) - - map_ffram: - opt -fast -mux_undef -undriven -fine -full - memory_map - opt -undriven -fine - techmap -map +/techmap.v - opt -full - clean -purge - setundef -undriven -zero - abc -markgroups -dff -D 1 (only if -retime) - - map_ffs: - dfflegalize -cell $_DFFE_PN0P_ 01 - techmap -map +/intel/common/ff_map.v - - map_luts: - abc -lut 4 - clean - - map_cells: - iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I (if -iopads) - techmap -map +/intel/max10/cells_map.v - clean -purge - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - vqm: - write_verilog -attr2comment -defparam -nohex -decimal -renameprefix syn_ <file-name> - - vpr: - opt_clean -purge - write_blif <file-name> - - -WARNING: THE 'synth_intel' COMMAND IS EXPERIMENTAL. -\end{lstlisting} - -\section{synth\_intel\_alm -- synthesis for ALM-based Intel (Altera) FPGAs.} -\label{cmd:synth_intel_alm} -\begin{lstlisting}[numbers=left,frame=single] - synth_intel_alm [options] - -This command runs synthesis for ALM-based Intel FPGAs. - - -top <module> - use the specified module as top module - - -family <family> - target one of: - "cyclonev" - Cyclone V (default) - "arriav" - Arria V (non-GZ) - "cyclone10gx" - Cyclone 10GX - - -vqm <file> - write the design to the specified Verilog Quartus Mapping File. Writing - of an output file is omitted if this parameter is not specified. Implies - -quartus. - - -noflatten - do not flatten design before synthesis; useful for per-module area - statistics - - -quartus - output a netlist using Quartus cells instead of MISTRAL_* cells - - -dff - pass DFFs to ABC to perform sequential logic optimisations - (EXPERIMENTAL) - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -nolutram - do not use LUT RAM cells in output netlist - - -nobram - do not use block RAM cells in output netlist - - -nodsp - do not map multipliers to MISTRAL_MUL cells - - -noiopad - do not instantiate IO buffers - - -noclkbuf - do not insert global clock buffers - -The following commands are executed by this synthesis command: - - begin: - read_verilog -specify -lib -D <family> +/intel_alm/common/alm_sim.v - read_verilog -specify -lib -D <family> +/intel_alm/common/dff_sim.v - read_verilog -specify -lib -D <family> +/intel_alm/common/dsp_sim.v - read_verilog -specify -lib -D <family> +/intel_alm/common/mem_sim.v - read_verilog -specify -lib -D <family> +/intel_alm/common/misc_sim.v - read_verilog -specify -lib -D <family> -icells +/intel_alm/common/abc9_model.v - read_verilog -lib +/intel/common/altpll_bb.v - read_verilog -lib +/intel_alm/common/megafunction_bb.v - hierarchy -check -top <top> - - coarse: - proc - flatten (skip if -noflatten) - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=6 - opt_expr - opt_clean - techmap -map +/mul2dsp.v [...] (unless -nodsp) - alumacc - iopadmap -bits -outpad MISTRAL_OB I:PAD -inpad MISTRAL_IB O:PAD -toutpad MISTRAL_IO OE:O:PAD -tinoutpad MISTRAL_IO OE:O:I:PAD A:top (unless -noiopad) - techmap -map +/intel_alm/common/arith_alm_map.v -map +/intel_alm/common/dsp_map.v - opt - memory -nomap - opt_clean - - map_bram: (skip if -nobram) - memory_bram -rules +/intel_alm/common/bram_<bram_type>.txt - techmap -map +/intel_alm/common/bram_<bram_type>_map.v - - map_lutram: (skip if -nolutram) - memory_bram -rules +/intel_alm/common/lutram_mlab.txt (for Cyclone V / Cyclone 10GX) - - map_ffram: - memory_map - opt -full - - map_ffs: - techmap - dfflegalize -cell $_DFFE_PN0P_ 0 -cell $_SDFFCE_PP0P_ 0 - techmap -map +/intel_alm/common/dff_map.v - opt -full -undriven -mux_undef - clean -purge - clkbufmap -buf MISTRAL_CLKBUF Q:A (unless -noclkbuf) - - map_luts: - techmap -map +/intel_alm/common/abc9_map.v - abc9 [-dff] -maxlut 6 -W 600 - techmap -map +/intel_alm/common/abc9_unmap.v - techmap -map +/intel_alm/common/alm_map.v - opt -fast - autoname - clean - - check: - hierarchy -check - stat - check - blackbox =A:whitebox - - quartus: - rename -hide w:*[* w:*]* - setundef -zero - hilomap -singleton -hicell __MISTRAL_VCC Q -locell __MISTRAL_GND Q - techmap -D <family> -map +/intel_alm/common/quartus_rename.v - - vqm: - write_verilog -attr2comment -defparam -nohex -decimal <file-name> -\end{lstlisting} - -\section{synth\_machxo2 -- synthesis for MachXO2 FPGAs. This work is experimental.} -\label{cmd:synth_machxo2} -\begin{lstlisting}[numbers=left,frame=single] - synth_machxo2 [options] - -This command runs synthesis for MachXO2 FPGAs. - - -top <module> - use the specified module as top module - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -nobram - do not use block RAM cells in output netlist - - -nolutram - do not use LUT RAM cells in output netlist - - -noflatten - do not flatten design before synthesis - - -noiopad - do not insert IO buffers - - -vpr - generate an output netlist (and BLIF file) suitable for VPR - (this feature is experimental and incomplete) - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -icells +/machxo2/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - synth -run coarse - - map_ram: - memory_libmap -lib +/machxo2/lutrams.txt -lib +/machxo2/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram) - techmap -map +/machxo2/lutrams_map.v -map +/machxo2/brams_map.v - - fine: - memory_map - opt -full - techmap -map +/techmap.v - opt -fast - - map_ios: (unless -noiopad) - iopadmap -bits -outpad $__FACADE_OUTPAD I:O -inpad $__FACADE_INPAD O:I -toutpad $__FACADE_TOUTPAD ~T:I:O -tinoutpad $__FACADE_TINOUTPAD ~T:O:I:B A:top - attrmvcp -attr src -attr LOC t:$__FACADE_OUTPAD %x:+[O] t:$__FACADE_TOUTPAD %x:+[O] t:$__FACADE_TINOUTPAD %x:+[B] - attrmvcp -attr src -attr LOC -driven t:$__FACADE_INPAD %x:+[I] - - map_ffs: - dfflegalize -cell $_DFF_P_ 0 - - map_luts: - abc -lut 4 -dress - clean - - map_cells: - techmap -map +/machxo2/cells_map.v - clean - - check: - hierarchy -check - stat - blackbox =A:whitebox - - blif: - opt_clean -purge (vpr mode) - write_blif -attr -cname -conn -param <file-name> (vpr mode) - write_blif -gates -attr -param <file-name> (non-vpr mode) - - edif: - write_edif <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_nexus -- synthesis for Lattice Nexus FPGAs} -\label{cmd:synth_nexus} -\begin{lstlisting}[numbers=left,frame=single] - synth_nexus [options] - -This command runs synthesis for Lattice Nexus FPGAs. - - -top <module> - use the specified module as top module - - -family <device> - run synthesis for the specified Nexus device - supported values: lifcl, lfd2nx - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -vm <file> - write the design to the specified structural Verilog file. writing of - an output file is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -dff - run 'abc'/'abc9' with -dff option - - -retime - run 'abc' with '-dff -D 1' options - - -noccu2 - do not use CCU2 cells in output netlist - - -nodffe - do not use flipflops with CE in output netlist - - -nolram - do not use large RAM cells in output netlist - note that large RAM must be explicitly requested with a (* lram *) - attribute on the memory. - - -nobram - do not use block RAM cells in output netlist - - -nolutram - do not use LUT RAM cells in output netlist - - -nowidelut - do not use PFU muxes to implement LUTs larger than LUT4s - - -noiopad - do not insert IO buffers - - -nodsp - do not infer DSP multipliers - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -specify +/nexus/cells_sim.v +/nexus/cells_xtra.v - hierarchy -check -top <top> - - coarse: - proc - flatten - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=4 - opt_expr - opt_clean - techmap -map +/mul2dsp.v [...] (unless -nodsp) - techmap -map +/nexus/dsp_map.v (unless -nodsp) - alumacc - opt - memory -nomap - opt_clean - - map_ram: - memory_libmap -lib +/nexus/lutrams.txt -lib +/nexus/brams.txt -lib +/nexus/lrams.txt -no-auto-huge [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram) - techmap -map +/nexus/lutrams_map.v -map +/nexus/brams_map.v -map +/nexus/lrams_map.v - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - - map_gates: - techmap -map +/techmap.v -map +/nexus/arith_map.v - iopadmap -bits -outpad OB I:O -inpad IB O:I -toutpad OBZ ~T:I:O -tinoutpad BB ~T:O:I:B A:top (skip if '-noiopad') - opt -fast - abc -dff -D 1 (only if -retime) - - map_ffs: - opt_clean - dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PP?_ r -cell $_SDFF_PP?_ r -cell $_DLATCH_?_ x [-cell $_DFFE_PP_ 01 -cell $_DFFE_PP?P_ r -cell $_SDFFE_PP?P_ r] ($_*DFFE_* only if not -nodffe) - zinit -all w:* t:$_DFF_?_ t:$_DFFE_??_ t:$_SDFF* (only if -abc9 and -dff - techmap -D NO_LUT -map +/nexus/cells_map.v - opt_expr -undriven -mux_undef - simplemap - attrmvcp -copy -attr syn_useioff - opt_clean - - map_luts: - techmap -map +/nexus/latches_map.v - abc -dress -lut 4:5 - clean - - map_cells: - techmap -map +/nexus/cells_map.v - setundef -zero - hilomap -singleton -hicell VHI Z -locell VLO Z - clean - - check: - autoname - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - json: - write_json <file-name> - - vm: - write_verilog <file-name> -\end{lstlisting} - -\section{synth\_quicklogic -- Synthesis for QuickLogic FPGAs} -\label{cmd:synth_quicklogic} -\begin{lstlisting}[numbers=left,frame=single] - synth_quicklogic [options] -This command runs synthesis for QuickLogic FPGAs - - -top <module> - use the specified module as top module - - -family <family> - run synthesis for the specified QuickLogic architecture - generate the synthesis netlist for the specified family. - supported values: - - pp3: PolarPro 3 - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -verilog <file> - write the design to the specified verilog file. writing of an output - file is omitted if this parameter is not specified. - - -abc - use old ABC flow, which has generally worse mapping results but is less - likely to have bugs. - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -specify +/quicklogic/cells_sim.v +/quicklogic/pp3_cells_sim.v - read_verilog -lib -specify +/quicklogic/lut_sim.v - hierarchy -check -top <top> - - coarse: - proc - flatten - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce - peepopt - opt_clean - share - techmap -map +/cmp2lut.v -D LUT_WIDTH=4 - opt_expr - opt_clean - alumacc - pmuxtree - opt - memory -nomap - opt_clean - - map_ffram: - opt -fast -mux_undef -undriven -fine - memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic - opt -undriven -fine - - map_gates: - techmap - opt -fast - muxcover -mux8 -mux4 - - map_ffs: - opt_expr - dfflegalize -cell $_DFFSRE_PPPP_ 0 -cell $_DLATCH_?_ x - techmap -map +/quicklogic/pp3_cells_map.v -map +/quicklogic/pp3_ffs_map.v - opt_expr -mux_undef - - map_luts: - techmap -map +/quicklogic/pp3_latches_map.v - read_verilog -lib -specify -icells +/quicklogic/abc9_model.v - techmap -map +/quicklogic/abc9_map.v - abc9 -maxlut 4 -dff - techmap -map +/quicklogic/abc9_unmap.v - clean - - map_cells: - techmap -map +/quicklogic/pp3_lut_map.v - clean - - check: - autoname - hierarchy -check - stat - check -noinit - - iomap: - clkbufmap -inpad ckpad Q:P - iopadmap -bits -outpad outpad A:P -inpad inpad Q:P -tinoutpad bipad EN:Q:A:P A:top - - finalize: - setundef -zero -params -undriven - hilomap -hicell logic_1 A -locell logic_0 A -singleton A:top - opt_clean -purge - check - blackbox =A:whitebox - - blif: - write_blif -attr -param -auto-top - - verilog: - write_verilog -noattr -nohex <file-name> -\end{lstlisting} - -\section{synth\_sf2 -- synthesis for SmartFusion2 and IGLOO2 FPGAs} -\label{cmd:synth_sf2} -\begin{lstlisting}[numbers=left,frame=single] - synth_sf2 [options] - -This command runs synthesis for SmartFusion2 and IGLOO2 FPGAs. - - -top <module> - use the specified module as top module - - -edif <file> - write the design to the specified EDIF file. writing of an output file - is omitted if this parameter is not specified. - - -vlog <file> - write the design to the specified Verilog file. writing of an output - file is omitted if this parameter is not specified. - - -json <file> - write the design to the specified JSON file. writing of an output file - is omitted if this parameter is not specified. - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -noflatten - do not flatten design before synthesis - - -noiobs - run synthesis in "block mode", i.e. do not insert IO buffers - - -clkbuf - insert direct PAD->global_net buffers - - -discard-ffinit - discard FF init value instead of emitting an error - - -retime - run 'abc' with '-dff -D 1' options - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib +/sf2/cells_sim.v - hierarchy -check -top <top> - - flatten: (unless -noflatten) - proc - flatten - tribuf -logic - deminout - - coarse: - attrmap -remove init (only if -discard-ffinit) - synth -run coarse - - fine: - opt -fast -mux_undef -undriven -fine - memory_map - opt -undriven -fine - techmap -map +/techmap.v -map +/sf2/arith_map.v - opt -fast - abc -dff -D 1 (only if -retime) - - map_ffs: - dfflegalize -cell $_DFFE_PN?P_ x -cell $_SDFFCE_PN?P_ x -cell $_DLATCH_PN?_ x - techmap -D NO_LUT -map +/sf2/cells_map.v - opt_expr -mux_undef - simplemap - - map_luts: - abc -lut 4 - clean - - map_cells: - techmap -map +/sf2/cells_map.v - clean - - map_iobs: - clkbufmap -buf CLKINT Y:A [-inpad CLKBUF Y:PAD] (unless -noiobs, -inpad only passed if -clkbuf) - iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD (unless -noiobs) - clean -purge - - check: - hierarchy -check - stat - check -noinit - blackbox =A:whitebox - - edif: - write_edif -gndvccy <file-name> - - vlog: - write_verilog <file-name> - - json: - write_json <file-name> -\end{lstlisting} - -\section{synth\_xilinx -- synthesis for Xilinx FPGAs} -\label{cmd:synth_xilinx} -\begin{lstlisting}[numbers=left,frame=single] - synth_xilinx [options] - -This command runs synthesis for Xilinx FPGAs. This command does not operate on -partly selected designs. At the moment this command creates netlists that are -compatible with 7-Series Xilinx devices. - - -top <module> - use the specified module as top module - - -family <family> - run synthesis for the specified Xilinx architecture - generate the synthesis netlist for the specified family. - supported values: - - xcup: Ultrascale Plus - - xcu: Ultrascale - - xc7: Series 7 (default) - - xc6s: Spartan 6 - - xc6v: Virtex 6 - - xc5v: Virtex 5 (EXPERIMENTAL) - - xc4v: Virtex 4 (EXPERIMENTAL) - - xc3sda: Spartan 3A DSP (EXPERIMENTAL) - - xc3sa: Spartan 3A (EXPERIMENTAL) - - xc3se: Spartan 3E (EXPERIMENTAL) - - xc3s: Spartan 3 (EXPERIMENTAL) - - xc2vp: Virtex 2 Pro (EXPERIMENTAL) - - xc2v: Virtex 2 (EXPERIMENTAL) - - xcve: Virtex E, Spartan 2E (EXPERIMENTAL) - - xcv: Virtex, Spartan 2 (EXPERIMENTAL) - - -edif <file> - write the design to the specified edif file. writing of an output file - is omitted if this parameter is not specified. - - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. - - -ise - generate an output netlist suitable for ISE - - -nobram - do not use block RAM cells in output netlist - - -nolutram - do not use distributed RAM cells in output netlist - - -nosrl - do not use distributed SRL cells in output netlist - - -nocarry - do not use XORCY/MUXCY/CARRY4 cells in output netlist - - -nowidelut - do not use MUXF[5-9] resources to implement LUTs larger than native for - the target - - -nodsp - do not use DSP48*s to implement multipliers and associated logic - - -noiopad - disable I/O buffer insertion (useful for hierarchical or - out-of-context flows) - - -noclkbuf - disable automatic clock buffer insertion - - -uram - infer URAM288s for large memories (xcup only) - - -widemux <int> - enable inference of hard multiplexer resources (MUXF[78]) for muxes at - or above this number of inputs (minimum value 2, recommended value >= 5) - default: 0 (no inference) - - -run <from_label>:<to_label> - only run the commands between the labels (see below). an empty - from label is synonymous to 'begin', and empty to label is - synonymous to the end of the command list. - - -flatten - flatten design before synthesis - - -dff - run 'abc'/'abc9' with -dff option - - -retime - run 'abc' with '-D 1' option to enable flip-flop retiming. - implies -dff. - - -abc9 - use new ABC9 flow (EXPERIMENTAL) - - -The following commands are executed by this synthesis command: - - begin: - read_verilog -lib -specify +/xilinx/cells_sim.v - read_verilog -lib +/xilinx/cells_xtra.v - hierarchy -check -auto-top - - prepare: - proc - flatten (with '-flatten') - tribuf -logic - deminout - opt_expr - opt_clean - check - opt -nodffe -nosdff - fsm - opt - wreduce [-keepdc] (option for '-widemux') - peepopt - opt_clean - muxpack ('-widemux' only) - pmux2shiftx (skip if '-nosrl' and '-widemux=0') - clean (skip if '-nosrl' and '-widemux=0') - - map_dsp: (skip if '-nodsp') - memory_dff - techmap -map +/mul2dsp.v -map +/xilinx/{family}_dsp_map.v {options} - select a:mul2dsp - setattr -unset mul2dsp - opt_expr -fine - wreduce - select -clear - xilinx_dsp -family <family> - chtype -set $mul t:$__soft_mul - - coarse: - techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=[46] - alumacc - share - opt - memory -nomap - opt_clean - - map_memory: - memory_libmap [...] - techmap -map +/xilinx/lutrams_<family>_map.v - techmap -map +/xilinx/brams_<family>_map.v - - map_ffram: - opt -fast -full - memory_map - - fine: - simplemap t:$mux ('-widemux' only) - muxcover <internal options> ('-widemux' only) - opt -full - xilinx_srl -variable -minlen 3 (skip if '-nosrl') - techmap -map +/techmap.v -D LUT_SIZE=[46] [-map +/xilinx/mux_map.v] -map +/xilinx/arith_map.v - opt -fast - - map_cells: - iopadmap -bits -outpad OBUF I:O -inpad IBUF O:I -toutpad OBUFT ~T:I:O -tinoutpad IOBUF ~T:O:I:IO A:top (skip if '-noiopad') - techmap -map +/techmap.v -map +/xilinx/cells_map.v - clean - - map_ffs: - dfflegalize -cell $_DFFE_?P?P_ 01 -cell $_SDFFE_?P?P_ 01 -cell $_DLATCH_?P?_ 01 (for xc6v, xc7, xcu, xcup) - zinit -all w:* t:$_SDFFE_* ('-dff' only) - techmap -map +/xilinx/ff_map.v ('-abc9' only) - - map_luts: - opt_expr -mux_undef -noclkinv - abc -luts 2:2,3,6:5[,10,20] [-dff] [-D 1] (option for '-nowidelut', '-dff', '-retime') - clean - techmap -map +/xilinx/ff_map.v (only if not '-abc9') - xilinx_srl -fixed -minlen 3 (skip if '-nosrl') - techmap -map +/xilinx/lut_map.v -map +/xilinx/cells_map.v -D LUT_WIDTH=[46] - xilinx_dffopt [-lut4] - opt_lut_ins -tech xilinx - - finalize: - clkbufmap -buf BUFG O:I (skip if '-noclkbuf') - extractinv -inv INV O:I (only if '-ise') - clean - - check: - hierarchy -check - stat -tech xilinx - check -noinit - blackbox =A:whitebox - - edif: - write_edif -pvector bra - - blif: - write_blif -\end{lstlisting} - -\section{tcl -- execute a TCL script file} -\label{cmd:tcl} -\begin{lstlisting}[numbers=left,frame=single] - tcl <filename> [args] - -This command executes the tcl commands in the specified file. -Use 'yosys cmd' to run the yosys command 'cmd' from tcl. - -The tcl command 'yosys -import' can be used to import all yosys -commands directly as tcl commands to the tcl shell. Yosys commands -'proc' and 'rename' are wrapped to tcl commands 'procs' and 'renames' -in order to avoid a name collision with the built in commands. - -If any arguments are specified, these arguments are provided to the script via -the standard $argc and $argv variables. - -Note, tcl will not recieve the output of any yosys command. If the output -of the tcl commands are needed, use the yosys command 'tee -s result.string' -to redirect yosys's output to the 'result.string' scratchpad value. -\end{lstlisting} - -\section{techmap -- generic technology mapper} -\label{cmd:techmap} -\begin{lstlisting}[numbers=left,frame=single] - techmap [-map filename] [selection] - -This pass implements a very simple technology mapper that replaces cells in -the design with implementations given in form of a Verilog or RTLIL source -file. - - -map filename - the library of cell implementations to be used. - without this parameter a builtin library is used that - transforms the internal RTL cells to the internal gate - library. - - -map %<design-name> - like -map above, but with an in-memory design instead of a file. - - -extern - load the cell implementations as separate modules into the design - instead of inlining them. - - -max_iter <number> - only run the specified number of iterations on each module. - default: unlimited - - -recursive - instead of the iterative breadth-first algorithm use a recursive - depth-first algorithm. both methods should yield equivalent results, - but may differ in performance. - - -autoproc - Automatically call "proc" on implementations that contain processes. - - -wb - Ignore the 'whitebox' attribute on cell implementations. - - -assert - this option will cause techmap to exit with an error if it can't map - a selected cell. only cell types that end on an underscore are accepted - as final cell types by this mode. - - -D <define>, -I <incdir> - this options are passed as-is to the Verilog frontend for loading the - map file. Note that the Verilog frontend is also called with the - '-nooverwrite' option set. - -When a module in the map file has the 'techmap_celltype' attribute set, it will -match cells with a type that match the text value of this attribute. Otherwise -the module name will be used to match the cell. Multiple space-separated cell -types can be listed, and wildcards using [] will be expanded (ie. -"$_DFF_[PN]_" is the same as "$_DFF_P_ $_DFF_N_"). - -When a module in the map file has the 'techmap_simplemap' attribute set, techmap -will use 'simplemap' (see 'help simplemap') to map cells matching the module. - -When a module in the map file has the 'techmap_maccmap' attribute set, techmap -will use 'maccmap' (see 'help maccmap') to map cells matching the module. - -When a module in the map file has the 'techmap_wrap' attribute set, techmap -will create a wrapper for the cell and then run the command string that the -attribute is set to on the wrapper module. - -When a port on a module in the map file has the 'techmap_autopurge' attribute -set, and that port is not connected in the instantiation that is mapped, then -then a cell port connected only to such wires will be omitted in the mapped -version of the circuit. - -All wires in the modules from the map file matching the pattern _TECHMAP_* -or *._TECHMAP_* are special wires that are used to pass instructions from -the mapping module to the techmap command. At the moment the following special -wires are supported: - - _TECHMAP_FAIL_ - When this wire is set to a non-zero constant value, techmap will not - use this module and instead try the next module with a matching - 'techmap_celltype' attribute. - - When such a wire exists but does not have a constant value after all - _TECHMAP_DO_* commands have been executed, an error is generated. - - _TECHMAP_DO_* - This wires are evaluated in alphabetical order. The constant text value - of this wire is a yosys command (or sequence of commands) that is run - by techmap on the module. A common use case is to run 'proc' on modules - that are written using always-statements. - - When such a wire has a non-constant value at the time it is to be - evaluated, an error is produced. That means it is possible for such a - wire to start out as non-constant and evaluate to a constant value - during processing of other _TECHMAP_DO_* commands. - - A _TECHMAP_DO_* command may start with the special token 'CONSTMAP; '. - in this case techmap will create a copy for each distinct configuration - of constant inputs and shorted inputs at this point and import the - constant and connected bits into the map module. All further commands - are executed in this copy. This is a very convenient way of creating - optimized specializations of techmap modules without using the special - parameters described below. - - A _TECHMAP_DO_* command may start with the special token 'RECURSION; '. - then techmap will recursively replace the cells in the module with their - implementation. This is not affected by the -max_iter option. - - It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '. - - _TECHMAP_REMOVEINIT_<port-name>_ - When this wire is set to a constant value, the init attribute of the - wire(s) connected to this port will be consumed. This wire must have - the same width as the given port, and for every bit that is set to 1 in - the value, the corresponding init attribute bit will be changed to 1'bx. - If all bits of an init attribute are left as x, it will be removed. - -In addition to this special wires, techmap also supports special parameters in -modules in the map file: - - _TECHMAP_CELLTYPE_ - When a parameter with this name exists, it will be set to the type name - of the cell that matches the module. - - _TECHMAP_CELLNAME_ - When a parameter with this name exists, it will be set to the name - of the cell that matches the module. - - _TECHMAP_CONSTMSK_<port-name>_ - _TECHMAP_CONSTVAL_<port-name>_ - When this pair of parameters is available in a module for a port, then - former has a 1-bit for each constant input bit and the latter has the - value for this bit. The unused bits of the latter are set to undef (x). - - _TECHMAP_WIREINIT_<port-name>_ - When a parameter with this name exists, it will be set to the initial - value of the wire(s) connected to the given port, as specified by the - init attribute. If the attribute doesn't exist, x will be filled for the - missing bits. To remove the init attribute bits used, use the - _TECHMAP_REMOVEINIT_*_ wires. - - _TECHMAP_BITS_CONNMAP_ - _TECHMAP_CONNMAP_<port-name>_ - For an N-bit port, the _TECHMAP_CONNMAP_<port-name>_ parameter, if it - exists, will be set to an N*_TECHMAP_BITS_CONNMAP_ bit vector containing - N words (of _TECHMAP_BITS_CONNMAP_ bits each) that assign each single - bit driver a unique id. The values 0-3 are reserved for 0, 1, x, and z. - This can be used to detect shorted inputs. - -When a module in the map file has a parameter where the according cell in the -design has a port, the module from the map file is only used if the port in -the design is connected to a constant value. The parameter is then set to the -constant value. - -A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name -and attributes of the cell that is being replaced. -A cell with a name of the form `_TECHMAP_REPLACE_.<suffix>` in the map file will -be named thus but with the `_TECHMAP_REPLACE_' prefix substituted with the name -of the cell being replaced. -Similarly, a wire named in the form `_TECHMAP_REPLACE_.<suffix>` will cause a -new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_' -prefix also substituted. - -See 'help extract' for a pass that does the opposite thing. - -See 'help flatten' for a pass that does flatten the design (which is -essentially techmap but using the design itself as map library). -\end{lstlisting} - -\section{tee -- redirect command output to file} -\label{cmd:tee} -\begin{lstlisting}[numbers=left,frame=single] - tee [-q] [-o logfile|-a logfile] cmd - -Execute the specified command, optionally writing the commands output to the -specified logfile(s). - - -q - Do not print output to the normal destination (console and/or log file). - - -o logfile - Write output to this file, truncate if exists. - - -a logfile - Write output to this file, append if exists. - - -s scratchpad - Write output to this scratchpad value, truncate if it exists. - - +INT, -INT - Add/subtract INT from the -v setting for this command. -\end{lstlisting} - -\section{test\_abcloop -- automatically test handling of loops in abc command} -\label{cmd:test_abcloop} -\begin{lstlisting}[numbers=left,frame=single] - test_abcloop [options] - -Test handling of logic loops in ABC. - - -n {integer} - create this number of circuits and test them (default = 100). - - -s {positive_integer} - use this value as rng seed value (default = unix time). -\end{lstlisting} - -\section{test\_autotb -- generate simple test benches} -\label{cmd:test_autotb} -\begin{lstlisting}[numbers=left,frame=single] - test_autotb [options] [filename] - -Automatically create primitive Verilog test benches for all modules in the -design. The generated testbenches toggle the input pins of the module in -a semi-random manner and dumps the resulting output signals. - -This can be used to check the synthesis results for simple circuits by -comparing the testbench output for the input files and the synthesis results. - -The backend automatically detects clock signals. Additionally a signal can -be forced to be interpreted as clock signal by setting the attribute -'gentb_clock' on the signal. - -The attribute 'gentb_constant' can be used to force a signal to a constant -value after initialization. This can e.g. be used to force a reset signal -low in order to explore more inner states in a state machine. - -The attribute 'gentb_skip' can be attached to modules to suppress testbench -generation. - - -n <int> - number of iterations the test bench should run (default = 1000) - - -seed <int> - seed used for pseudo-random number generation (default = 0). - a value of 0 will cause an arbitrary seed to be chosen, based on - the current system time. -\end{lstlisting} - -\section{test\_cell -- automatically test the implementation of a cell type} -\label{cmd:test_cell} -\begin{lstlisting}[numbers=left,frame=single] - test_cell [options] {cell-types} - -Tests the internal implementation of the given cell type (for example '$add') -by comparing SAT solver, EVAL and TECHMAP implementations of the cell types.. - -Run with 'all' instead of a cell type to run the test on all supported -cell types. Use for example 'all /$add' for all cell types except $add. - - -n {integer} - create this number of cell instances and test them (default = 100). - - -s {positive_integer} - use this value as rng seed value (default = unix time). - - -f {rtlil_file} - don't generate circuits. instead load the specified RTLIL file. - - -w {filename_prefix} - don't test anything. just generate the circuits and write them - to RTLIL files with the specified prefix - - -map {filename} - pass this option to techmap. - - -simlib - use "techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter 2 -autoproc" - - -aigmap - instead of calling "techmap", call "aigmap" - - -muxdiv - when creating test benches with dividers, create an additional mux - to mask out the division-by-zero case - - -script {script_file} - instead of calling "techmap", call "script {script_file}". - - -const - set some input bits to random constant values - - -nosat - do not check SAT model or run SAT equivalence checking - - -noeval - do not check const-eval models - - -edges - test cell edges db creator against sat-based implementation - - -v - print additional debug information to the console - - -vlog {filename} - create a Verilog test bench to test simlib and write_verilog -\end{lstlisting} - -\section{test\_pmgen -- test pass for pmgen} -\label{cmd:test_pmgen} -\begin{lstlisting}[numbers=left,frame=single] - test_pmgen -reduce_chain [options] [selection] - -Demo for recursive pmgen patterns. Map chains of AND/OR/XOR to $reduce_*. - - - test_pmgen -reduce_tree [options] [selection] - -Demo for recursive pmgen patterns. Map trees of AND/OR/XOR to $reduce_*. - - - test_pmgen -eqpmux [options] [selection] - -Demo for recursive pmgen patterns. Optimize EQ/NE/PMUX circuits. - - - test_pmgen -generate [options] <pattern_name> - -Create modules that match the specified pattern. -\end{lstlisting} - -\section{torder -- print cells in topological order} -\label{cmd:torder} -\begin{lstlisting}[numbers=left,frame=single] - torder [options] [selection] - -This command prints the selected cells in topological order. - - -stop <cell_type> <cell_port> - do not use the specified cell port in topological sorting - - -noautostop - by default Q outputs of internal FF cells and memory read port outputs - are not used in topological sorting. this option deactivates that. -\end{lstlisting} - -\section{trace -- redirect command output to file} -\label{cmd:trace} -\begin{lstlisting}[numbers=left,frame=single] - trace cmd - -Execute the specified command, logging all changes the command performs on -the design in real time. -\end{lstlisting} - -\section{tribuf -- infer tri-state buffers} -\label{cmd:tribuf} -\begin{lstlisting}[numbers=left,frame=single] - tribuf [options] [selection] - -This pass transforms $mux cells with 'z' inputs to tristate buffers. - - -merge - merge multiple tri-state buffers driving the same net - into a single buffer. - - -logic - convert tri-state buffers that do not drive output ports - to non-tristate logic. this option implies -merge. - - -formal - convert all tri-state buffers to non-tristate logic and - add a formal assertion that no two buffers are driving the - same net simultaneously. this option implies -merge. -\end{lstlisting} - -\section{uniquify -- create unique copies of modules} -\label{cmd:uniquify} -\begin{lstlisting}[numbers=left,frame=single] - uniquify [selection] - -By default, a module that is instantiated by several other modules is only -kept once in the design. This preserves the original modularity of the design -and reduces the overall size of the design in memory. But it prevents certain -optimizations and other operations on the design. This pass creates unique -modules for all selected cells. The created modules are marked with the -'unique' attribute. - -This commands only operates on modules that by themself have the 'unique' -attribute set (the 'top' module is unique implicitly). -\end{lstlisting} - -\section{verific -- load Verilog and VHDL designs using Verific} -\label{cmd:verific} -\begin{lstlisting}[numbers=left,frame=single] - verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>.. - -Load the specified Verilog/SystemVerilog files into Verific. - -All files specified in one call to this command are one compilation unit. -Files passed to different calls to this command are treated as belonging to -different compilation units. - -Additional -D<macro>[=<value>] options may be added after the option indicating -the language version (and before file names) to set additional verilog defines. -The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly. - - - verific -formal <verilog-file>.. - -Like -sv, but define FORMAL instead of SYNTHESIS. - - - verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>.. - -Load the specified VHDL files into Verific. - - - verific {-edif} <edif-file>.. - -Load the specified EDIF files into Verific. - - - verific {-liberty} <liberty-file>.. - -Load the specified Liberty files into Verific. -Default library when -work is not present is one specified in liberty file. -To use from SystemVerilog or VHDL use -L to specify liberty library. - -lib - only create empty blackbox modules - - - verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009| - -sv2012|-sv|-formal] <command-file> - -Load and execute the specified command file. -Override verilog parsing mode can be set. -The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly. - -Command file parser supports following commands in file: - +define+<MACRO>=<VALUE> - defines macro - -u - upper case all identifier (makes Verilog parser - case insensitive) - -v <filepath> - register library name (file) - -y <filepath> - register library name (directory) - +incdir+<filepath> - specify include dir - +libext+<filepath> - specify library extension - +liborder+<id> - add library in ordered list - +librescan - unresolved modules will be always searched - starting with the first library specified - by -y/-v options. - -f/-file <filepath> - nested -f option - -F <filepath> - nested -F option (relative path) - parse files: - <filepath> - +systemverilogext+<filepath> - +verilog1995ext+<filepath> - +verilog2001ext+<filepath> - - analysis mode: - -ams - +v2k - -sverilog - - - verific [-work <libname>] {-sv|-vhdl|...} <hdl-file> - -Load the specified Verilog/SystemVerilog/VHDL file into the specified library. -(default library when -work is not present: "work") - - - verific [-L <libname>] {-sv|-vhdl|...} <hdl-file> - -Look up external definitions in the specified library. -(-L may be used more than once) - - - verific -vlog-incdir <directory>.. - -Add Verilog include directories. - - - verific -vlog-libdir <directory>.. - -Add Verilog library directories. Verific will search in this directories to -find undefined modules. - - - verific -vlog-libext <extension>.. - -Add Verilog library extensions, used when searching in library directories. - - - verific -vlog-define <macro>[=<value>].. - -Add Verilog defines. - - - verific -vlog-undef <macro>.. - -Remove Verilog defines previously set with -vlog-define. - - - verific -set-error <msg_id>.. - verific -set-warning <msg_id>.. - verific -set-info <msg_id>.. - verific -set-ignore <msg_id>.. - -Set message severity. <msg_id> is the string in square brackets when a message -is printed, such as VERI-1209. -Also errors, warnings, infos and comments could be used to set new severity for -all messages of certain type. - - - verific -import [options] <top>.. - -Elaborate the design for the specified top modules or configurations, import to -Yosys and reset the internal state of Verific. - -Import options: - - -all - Elaborate all modules, not just the hierarchy below the given top - modules. With this option the list of modules to import is optional. - - -gates - Create a gate-level netlist. - - -flatten - Flatten the design in Verific before importing. - - -extnets - Resolve references to external nets by adding module ports as needed. - - -autocover - Generate automatic cover statements for all asserts - - -fullinit - Keep all register initializations, even those for non-FF registers. - - -cells - Import all cell definitions from Verific loaded libraries even if they are - unused in design. Useful with "-edif" and "-liberty" option. - - -chparam name value - Elaborate the specified top modules (all modules when -all given) using - this parameter value. Modules on which this parameter does not exist will - cause Verific to produce a VERI-1928 or VHDL-1676 message. This option - can be specified multiple times to override multiple parameters. - String values must be passed in double quotes ("). - - -v, -vv - Verbose log messages. (-vv is even more verbose than -v.) - - -pp <filename> - Pretty print design after elaboration to specified file. - -The following additional import options are useful for debugging the Verific -bindings (for Yosys and/or Verific developers): - - -k - Keep going after an unsupported verific primitive is found. The - unsupported primitive is added as blockbox module to the design. - This will also add all SVA related cells to the design parallel to - the checker logic inferred by it. - - -V - Import Verific netlist as-is without translating to Yosys cell types. - - -nosva - Ignore SVA properties, do not infer checker logic. - - -L <int> - Maximum number of ctrl bits for SVA checker FSMs (default=16). - - -n - Keep all Verific names on instances and nets. By default only - user-declared names are preserved. - - -d <dump_file> - Dump the Verific netlist as a verilog file. - - - verific [-work <libname>] -pp [options] <filename> [<module>].. - -Pretty print design (or just module) to the specified file from the -specified library. (default library when -work is not present: "work") - -Pretty print options: - - -verilog - Save output for Verilog/SystemVerilog design modules (default). - - -vhdl - Save output for VHDL design units. - - - verific -cfg [<name> [<value>]] - -Get/set Verific runtime flags. - - -Use YosysHQ Tabby CAD Suite if you need Yosys+Verific. -https://www.yosyshq.com/ - -Contact office@yosyshq.com for free evaluation -binaries of YosysHQ Tabby CAD Suite. -\end{lstlisting} - -\section{verilog\_defaults -- set default options for read\_verilog} -\label{cmd:verilog_defaults} -\begin{lstlisting}[numbers=left,frame=single] - verilog_defaults -add [options] - -Add the specified options to the list of default options to read_verilog. - - - verilog_defaults -clear - -Clear the list of Verilog default options. - - - verilog_defaults -push - verilog_defaults -pop - -Push or pop the list of default options to a stack. Note that -push does -not imply -clear. -\end{lstlisting} - -\section{verilog\_defines -- define and undefine verilog defines} -\label{cmd:verilog_defines} -\begin{lstlisting}[numbers=left,frame=single] - verilog_defines [options] - -Define and undefine verilog preprocessor macros. - - -Dname[=definition] - define the preprocessor symbol 'name' and set its optional value - 'definition' - - -Uname[=definition] - undefine the preprocessor symbol 'name' - - -reset - clear list of defined preprocessor symbols - - -list - list currently defined preprocessor symbols -\end{lstlisting} - -\section{wbflip -- flip the whitebox attribute} -\label{cmd:wbflip} -\begin{lstlisting}[numbers=left,frame=single] - wbflip [selection] - -Flip the whitebox attribute on selected cells. I.e. if it's set, unset it, and -vice-versa. Blackbox cells are not effected by this command. -\end{lstlisting} - -\section{wreduce -- reduce the word size of operations if possible} -\label{cmd:wreduce} -\begin{lstlisting}[numbers=left,frame=single] - wreduce [options] [selection] - -This command reduces the word size of operations. For example it will replace -the 32 bit adders in the following code with adders of more appropriate widths: - - module test(input [3:0] a, b, c, output [7:0] y); - assign y = a + b + c + 1; - endmodule - -Options: - - -memx - Do not change the width of memory address ports. Use this options in - flows that use the 'memory_memx' pass. - - -mux_undef - remove 'undef' inputs from $mux, $pmux and $_MUX_ cells - - -keepdc - Do not optimize explicit don't-care values. -\end{lstlisting} - -\section{write\_aiger -- write design to AIGER file} -\label{cmd:write_aiger} -\begin{lstlisting}[numbers=left,frame=single] - write_aiger [options] [filename] - -Write the current design to an AIGER file. The design must be flattened and -must not contain any cell types except $_AND_, $_NOT_, simple FF types, -$assert and $assume cells, and $initstate cells. - -$assert and $assume cells are converted to AIGER bad state properties and -invariant constraints. - - -ascii - write ASCII version of AIGER format - - -zinit - convert FFs to zero-initialized FFs, adding additional inputs for - uninitialized FFs. - - -miter - design outputs are AIGER bad state properties - - -symbols - include a symbol table in the generated AIGER file - - -map <filename> - write an extra file with port and latch symbols - - -vmap <filename> - like -map, but more verbose - - -no-startoffset - make indexes zero based, enable using map files with smt solvers. - - -ywmap <filename> - write a map file for conversion to and from yosys witness traces. - - -I, -O, -B, -L - If the design contains no input/output/assert/flip-flop then create one - dummy input/output/bad_state-pin or latch to make the tools reading the - AIGER file happy. -\end{lstlisting} - -\section{write\_blif -- write design to BLIF file} -\label{cmd:write_blif} -\begin{lstlisting}[numbers=left,frame=single] - write_blif [options] [filename] - -Write the current design to an BLIF file. - - -top top_module - set the specified module as design top module - - -buf <cell-type> <in-port> <out-port> - use cells of type <cell-type> with the specified port names for buffers - - -unbuf <cell-type> <in-port> <out-port> - replace buffer cells with the specified name and port names with - a .names statement that models a buffer - - -true <cell-type> <out-port> - -false <cell-type> <out-port> - -undef <cell-type> <out-port> - use the specified cell types to drive nets that are constant 1, 0, or - undefined. when '-' is used as <cell-type>, then <out-port> specifies - the wire name to be used for the constant signal and no cell driving - that wire is generated. when '+' is used as <cell-type>, then <out-port> - specifies the wire name to be used for the constant signal and a .names - statement is generated to drive the wire. - - -noalias - if a net name is aliasing another net name, then by default a net - without fanout is created that is driven by the other net. This option - suppresses the generation of this nets without fanout. - -The following options can be useful when the generated file is not going to be -read by a BLIF parser but a custom tool. It is recommended to not name the -output file *.blif when any of this options is used. - - -icells - do not translate Yosys's internal gates to generic BLIF logic - functions. Instead create .subckt or .gate lines for all cells. - - -gates - print .gate instead of .subckt lines for all cells that are not - instantiations of other modules from this design. - - -conn - do not generate buffers for connected wires. instead use the - non-standard .conn statement. - - -attr - use the non-standard .attr statement to write cell attributes - - -param - use the non-standard .param statement to write cell parameters - - -cname - use the non-standard .cname statement to write cell names - - -iname, -iattr - enable -cname and -attr functionality for .names statements - (the .cname and .attr statements will be included in the BLIF - output after the truth table for the .names statement) - - -blackbox - write blackbox cells with .blackbox statement. - - -impltf - do not write definitions for the $true, $false and $undef wires. -\end{lstlisting} - -\section{write\_btor -- write design to BTOR file} -\label{cmd:write_btor} -\begin{lstlisting}[numbers=left,frame=single] - write_btor [options] [filename] - -Write a BTOR description of the current design. - - -v - Add comments and indentation to BTOR output file - - -s - Output only a single bad property for all asserts - - -c - Output cover properties using 'bad' statements instead of asserts - - -i <filename> - Create additional info file with auxiliary information - - -x - Output symbols for internal netnames (starting with '$') -\end{lstlisting} - -\section{write\_cxxrtl -- convert design to C++ RTL simulation} -\label{cmd:write_cxxrtl} -\begin{lstlisting}[numbers=left,frame=single] - write_cxxrtl [options] [filename] - -Write C++ code that simulates the design. The generated code requires a driver -that instantiates the design, toggles its clock, and interacts with its ports. - -The following driver may be used as an example for a design with a single clock -driving rising edge triggered flip-flops: - - #include "top.cc" - - int main() { - cxxrtl_design::p_top top; - top.step(); - while (1) { - /* user logic */ - top.p_clk.set(false); - top.step(); - top.p_clk.set(true); - top.step(); - } - } - -Note that CXXRTL simulations, just like the hardware they are simulating, are -subject to race conditions. If, in the example above, the user logic would run -simultaneously with the rising edge of the clock, the design would malfunction. - -This backend supports replacing parts of the design with black boxes implemented -in C++. If a module marked as a CXXRTL black box, its implementation is ignored, -and the generated code consists only of an interface and a factory function. -The driver must implement the factory function that creates an implementation of -the black box, taking into account the parameters it is instantiated with. - -For example, the following Verilog code defines a CXXRTL black box interface for -a synchronous debug sink: - - (* cxxrtl_blackbox *) - module debug(...); - (* cxxrtl_edge = "p" *) input clk; - input en; - input [7:0] i_data; - (* cxxrtl_sync *) output [7:0] o_data; - endmodule - -For this HDL interface, this backend will generate the following C++ interface: - - struct bb_p_debug : public module { - value<1> p_clk; - bool posedge_p_clk() const { /* ... */ } - value<1> p_en; - value<8> p_i_data; - wire<8> p_o_data; - - bool eval() override; - bool commit() override; - - static std::unique_ptr<bb_p_debug> - create(std::string name, metadata_map parameters, metadata_map attributes); - }; - -The `create' function must be implemented by the driver. For example, it could -always provide an implementation logging the values to standard error stream: - - namespace cxxrtl_design { - - struct stderr_debug : public bb_p_debug { - bool eval() override { - if (posedge_p_clk() && p_en) - fprintf(stderr, "debug: %02x\n", p_i_data.data[0]); - p_o_data.next = p_i_data; - return bb_p_debug::eval(); - } - }; - - std::unique_ptr<bb_p_debug> - bb_p_debug::create(std::string name, cxxrtl::metadata_map parameters, - cxxrtl::metadata_map attributes) { - return std::make_unique<stderr_debug>(); - } - - } - -For complex applications of black boxes, it is possible to parameterize their -port widths. For example, the following Verilog code defines a CXXRTL black box -interface for a configurable width debug sink: - - (* cxxrtl_blackbox, cxxrtl_template = "WIDTH" *) - module debug(...); - parameter WIDTH = 8; - (* cxxrtl_edge = "p" *) input clk; - input en; - (* cxxrtl_width = "WIDTH" *) input [WIDTH - 1:0] i_data; - (* cxxrtl_width = "WIDTH" *) output [WIDTH - 1:0] o_data; - endmodule - -For this parametric HDL interface, this backend will generate the following C++ -interface (only the differences are shown): - - template<size_t WIDTH> - struct bb_p_debug : public module { - // ... - value<WIDTH> p_i_data; - wire<WIDTH> p_o_data; - // ... - static std::unique_ptr<bb_p_debug<WIDTH>> - create(std::string name, metadata_map parameters, metadata_map attributes); - }; - -The `create' function must be implemented by the driver, specialized for every -possible combination of template parameters. (Specialization is necessary to -enable separate compilation of generated code and black box implementations.) - - template<size_t SIZE> - struct stderr_debug : public bb_p_debug<SIZE> { - // ... - }; - - template<> - std::unique_ptr<bb_p_debug<8>> - bb_p_debug<8>::create(std::string name, cxxrtl::metadata_map parameters, - cxxrtl::metadata_map attributes) { - return std::make_unique<stderr_debug<8>>(); - } - -The following attributes are recognized by this backend: - - cxxrtl_blackbox - only valid on modules. if specified, the module contents are ignored, - and the generated code includes only the module interface and a factory - function, which will be called to instantiate the module. - - cxxrtl_edge - only valid on inputs of black boxes. must be one of "p", "n", "a". - if specified on signal `clk`, the generated code includes edge detectors - `posedge_p_clk()` (if "p"), `negedge_p_clk()` (if "n"), or both (if - "a"), simplifying implementation of clocked black boxes. - - cxxrtl_template - only valid on black boxes. must contain a space separated sequence of - identifiers that have a corresponding black box parameters. for each - of them, the generated code includes a `size_t` template parameter. - - cxxrtl_width - only valid on ports of black boxes. must be a constant expression, which - is directly inserted into generated code. - - cxxrtl_comb, cxxrtl_sync - only valid on outputs of black boxes. if specified, indicates that every - bit of the output port is driven, correspondingly, by combinatorial or - synchronous logic. this knowledge is used for scheduling optimizations. - if neither is specified, the output will be pessimistically treated as - driven by both combinatorial and synchronous logic. - -The following options are supported by this backend: - - -print-wire-types, -print-debug-wire-types - enable additional debug logging, for pass developers. - - -header - generate separate interface (.h) and implementation (.cc) files. - if specified, the backend must be called with a filename, and filename - of the interface is derived from filename of the implementation. - otherwise, interface and implementation are generated together. - - -namespace <ns-name> - place the generated code into namespace <ns-name>. if not specified, - "cxxrtl_design" is used. - - -nohierarchy - use design hierarchy as-is. in most designs, a top module should be - present as it is exposed through the C API and has unbuffered outputs - for improved performance; it will be determined automatically if absent. - - -noflatten - don't flatten the design. fully flattened designs can evaluate within - one delta cycle if they have no combinatorial feedback. - note that the debug interface and waveform dumps use full hierarchical - names for all wires even in flattened designs. - - -noproc - don't convert processes to netlists. in most designs, converting - processes significantly improves evaluation performance at the cost of - slight increase in compilation time. - - -O <level> - set the optimization level. the default is -O6. higher optimization - levels dramatically decrease compile and run time, and highest level - possible for a design should be used. - - -O0 - no optimization. - - -O1 - unbuffer internal wires if possible. - - -O2 - like -O1, and localize internal wires if possible. - - -O3 - like -O2, and inline internal wires if possible. - - -O4 - like -O3, and unbuffer public wires not marked (*keep*) if possible. - - -O5 - like -O4, and localize public wires not marked (*keep*) if possible. - - -O6 - like -O5, and inline public wires not marked (*keep*) if possible. - - -g <level> - set the debug level. the default is -g4. higher debug levels provide - more visibility and generate more code, but do not pessimize evaluation. - - -g0 - no debug information. the C API is disabled. - - -g1 - include bare minimum of debug information necessary to access all design - state. the C API is enabled. - - -g2 - like -g1, but include debug information for all public wires that are - directly accessible through the C++ interface. - - -g3 - like -g2, and include debug information for public wires that are tied - to a constant or another public wire. - - -g4 - like -g3, and compute debug information on demand for all public wires - that were optimized out. -\end{lstlisting} - -\section{write\_edif -- write design to EDIF netlist file} -\label{cmd:write_edif} -\begin{lstlisting}[numbers=left,frame=single] - write_edif [options] [filename] - -Write the current design to an EDIF netlist file. - - -top top_module - set the specified module as design top module - - -nogndvcc - do not create "GND" and "VCC" cells. (this will produce an error - if the design contains constant nets. use "hilomap" to map to custom - constant drivers first) - - -gndvccy - create "GND" and "VCC" cells with "Y" outputs. (the default is - "G" for "GND" and "P" for "VCC".) - - -attrprop - create EDIF properties for cell attributes - - -keep - create extra KEEP nets by allowing a cell to drive multiple nets. - - -pvector {par|bra|ang} - sets the delimiting character for module port rename clauses to - parentheses, square brackets, or angle brackets. - -Unfortunately there are different "flavors" of the EDIF file format. This -command generates EDIF files for the Xilinx place&route tools. It might be -necessary to make small modifications to this command when a different tool -is targeted. -\end{lstlisting} - -\section{write\_file -- write a text to a file} -\label{cmd:write_file} -\begin{lstlisting}[numbers=left,frame=single] - write_file [options] output_file [input_file] - -Write the text from the input file to the output file. - - -a - Append to output file (instead of overwriting) - - -Inside a script the input file can also can a here-document: - - write_file hello.txt <<EOT - Hello World! - EOT -\end{lstlisting} - -\section{write\_firrtl -- write design to a FIRRTL file} -\label{cmd:write_firrtl} -\begin{lstlisting}[numbers=left,frame=single] - write_firrtl [options] [filename] - -Write a FIRRTL netlist of the current design. -The following commands are executed by this command: - pmuxtree - bmuxmap - demuxmap -\end{lstlisting} - -\section{write\_ilang -- (deprecated) alias of write\_rtlil} -\label{cmd:write_ilang} -\begin{lstlisting}[numbers=left,frame=single] -See `help write_rtlil`. -\end{lstlisting} - -\section{write\_intersynth -- write design to InterSynth netlist file} -\label{cmd:write_intersynth} -\begin{lstlisting}[numbers=left,frame=single] - write_intersynth [options] [filename] - -Write the current design to an 'intersynth' netlist file. InterSynth is -a tool for Coarse-Grain Example-Driven Interconnect Synthesis. - - -notypes - do not generate celltypes and conntypes commands. i.e. just output - the netlists. this is used for postsilicon synthesis. - - -lib <verilog_or_rtlil_file> - Use the specified library file for determining whether cell ports are - inputs or outputs. This option can be used multiple times to specify - more than one library. - - -selected - only write selected modules. modules must be selected entirely or - not at all. - -http://bygone.clairexen.net/intersynth/ -\end{lstlisting} - -\section{write\_jny -- generate design metadata} -\label{cmd:write_jny} -\begin{lstlisting}[numbers=left,frame=single] - jny [options] [selection] - -Write JSON netlist metadata for the current design - - -no-connections - Don't include connection information in the netlist output. - - -no-attributes - Don't include attributed information in the netlist output. - - -no-properties - Don't include property information in the netlist output. - -The JSON schema for JNY output files is located in the "jny.schema.json" file -which is located at "https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json" -\end{lstlisting} - -\section{write\_json -- write design to a JSON file} -\label{cmd:write_json} -\begin{lstlisting}[numbers=left,frame=single] - write_json [options] [filename] - -Write a JSON netlist of the current design. - - -aig - include AIG models for the different gate types - - -compat-int - emit 32-bit or smaller fully-defined parameter values directly - as JSON numbers (for compatibility with old parsers) - - -The general syntax of the JSON output created by this command is as follows: - - { - "creator": "Yosys <version info>", - "modules": { - <module_name>: { - "attributes": { - <attribute_name>: <attribute_value>, - ... - }, - "parameter_default_values": { - <parameter_name>: <parameter_value>, - ... - }, - "ports": { - <port_name>: <port_details>, - ... - }, - "cells": { - <cell_name>: <cell_details>, - ... - }, - "memories": { - <memory_name>: <memory_details>, - ... - }, - "netnames": { - <net_name>: <net_details>, - ... - } - } - }, - "models": { - ... - }, - } - -Where <port_details> is: - - { - "direction": <"input" | "output" | "inout">, - "bits": <bit_vector> - "offset": <the lowest bit index in use, if non-0> - "upto": <1 if the port bit indexing is MSB-first> - "signed": <1 if the port is signed> - } - -The "offset" and "upto" fields are skipped if their value would be 0. -They don't affect connection semantics, and are only used to preserve original -HDL bit indexing.And <cell_details> is: - - { - "hide_name": <1 | 0>, - "type": <cell_type>, - "model": <AIG model name, if -aig option used>, - "parameters": { - <parameter_name>: <parameter_value>, - ... - }, - "attributes": { - <attribute_name>: <attribute_value>, - ... - }, - "port_directions": { - <port_name>: <"input" | "output" | "inout">, - ... - }, - "connections": { - <port_name>: <bit_vector>, - ... - }, - } - -And <memory_details> is: - - { - "hide_name": <1 | 0>, - "attributes": { - <attribute_name>: <attribute_value>, - ... - }, - "width": <memory width> - "start_offset": <the lowest valid memory address> - "size": <memory size> - } - -And <net_details> is: - - { - "hide_name": <1 | 0>, - "bits": <bit_vector> - "offset": <the lowest bit index in use, if non-0> - "upto": <1 if the port bit indexing is MSB-first> - "signed": <1 if the port is signed> - } - -The "hide_name" fields are set to 1 when the name of this cell or net is -automatically created and is likely not of interest for a regular user. - -The "port_directions" section is only included for cells for which the -interface is known. - -Module and cell ports and nets can be single bit wide or vectors of multiple -bits. Each individual signal bit is assigned a unique integer. The <bit_vector> -values referenced above are vectors of this integers. Signal bits that are -connected to a constant driver are denoted as string "0", "1", "x", or -"z" instead of a number. - -Bit vectors (including integers) are written as string holding the binary -representation of the value. Strings are written as strings, with an appended -blank in cases of strings of the form /[01xz]* */. - -For example the following Verilog code: - - module test(input x, y); - (* keep *) foo #(.P(42), .Q(1337)) - foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}})); - endmodule - -Translates to the following JSON output: - - { - "creator": "Yosys 0.9+2406 (git sha1 fb1168d8, clang 9.0.1 -fPIC -Os)", - "modules": { - "test": { - "attributes": { - "cells_not_processed": "00000000000000000000000000000001", - "src": "test.v:1.1-4.10" - }, - "ports": { - "x": { - "direction": "input", - "bits": [ 2 ] - }, - "y": { - "direction": "input", - "bits": [ 3 ] - } - }, - "cells": { - "foo_inst": { - "hide_name": 0, - "type": "foo", - "parameters": { - "P": "00000000000000000000000000101010", - "Q": "00000000000000000000010100111001" - }, - "attributes": { - "keep": "00000000000000000000000000000001", - "module_not_derived": "00000000000000000000000000000001", - "src": "test.v:3.1-3.55" - }, - "connections": { - "A": [ 3, 2 ], - "B": [ 2, 3 ], - "C": [ 2, 2, 2, 2, "0", "1", "0", "1" ] - } - } - }, - "netnames": { - "x": { - "hide_name": 0, - "bits": [ 2 ], - "attributes": { - "src": "test.v:1.19-1.20" - } - }, - "y": { - "hide_name": 0, - "bits": [ 3 ], - "attributes": { - "src": "test.v:1.22-1.23" - } - } - } - } - } - } - -The models are given as And-Inverter-Graphs (AIGs) in the following form: - - "models": { - <model_name>: [ - /* 0 */ [ <node-spec> ], - /* 1 */ [ <node-spec> ], - /* 2 */ [ <node-spec> ], - ... - ], - ... - }, - -The following node-types may be used: - - [ "port", <portname>, <bitindex>, <out-list> ] - - the value of the specified input port bit - - [ "nport", <portname>, <bitindex>, <out-list> ] - - the inverted value of the specified input port bit - - [ "and", <node-index>, <node-index>, <out-list> ] - - the ANDed value of the specified nodes - - [ "nand", <node-index>, <node-index>, <out-list> ] - - the inverted ANDed value of the specified nodes - - [ "true", <out-list> ] - - the constant value 1 - - [ "false", <out-list> ] - - the constant value 0 - -All nodes appear in topological order. I.e. only nodes with smaller indices -are referenced by "and" and "nand" nodes. - -The optional <out-list> at the end of a node specification is a list of -output portname and bitindex pairs, specifying the outputs driven by this node. - -For example, the following is the model for a 3-input 3-output $reduce_and cell -inferred by the following code: - - module test(input [2:0] in, output [2:0] out); - assign in = &out; - endmodule - - "$reduce_and:3U:3": [ - /* 0 */ [ "port", "A", 0 ], - /* 1 */ [ "port", "A", 1 ], - /* 2 */ [ "and", 0, 1 ], - /* 3 */ [ "port", "A", 2 ], - /* 4 */ [ "and", 2, 3, "Y", 0 ], - /* 5 */ [ "false", "Y", 1, "Y", 2 ] - ] - -Future version of Yosys might add support for additional fields in the JSON -format. A program processing this format must ignore all unknown fields. -\end{lstlisting} - -\section{write\_rtlil -- write design to RTLIL file} -\label{cmd:write_rtlil} -\begin{lstlisting}[numbers=left,frame=single] - write_rtlil [filename] - -Write the current design to an RTLIL file. (RTLIL is a text representation -of a design in yosys's internal format.) - - -selected - only write selected parts of the design. -\end{lstlisting} - -\section{write\_simplec -- convert design to simple C code} -\label{cmd:write_simplec} -\begin{lstlisting}[numbers=left,frame=single] - write_simplec [options] [filename] - -Write simple C code for simulating the design. The C code written can be used to -simulate the design in a C environment, but the purpose of this command is to -generate code that works well with C-based formal verification. - - -verbose - this will print the recursive walk used to export the modules. - - -i8, -i16, -i32, -i64 - set the maximum integer bit width to use in the generated code. - -THIS COMMAND IS UNDER CONSTRUCTION -\end{lstlisting} - -\section{write\_smt2 -- write design to SMT-LIBv2 file} -\label{cmd:write_smt2} -\begin{lstlisting}[numbers=left,frame=single] - write_smt2 [options] [filename] - -Write a SMT-LIBv2 [1] description of the current design. For a module with name -'<mod>' this will declare the sort '<mod>_s' (state of the module) and will -define and declare functions operating on that state. - -The following SMT2 functions are generated for a module with name '<mod>'. -Some declarations/definitions are printed with a special comment. A prover -using the SMT2 files can use those comments to collect all relevant metadata -about the design. - - ; yosys-smt2-module <mod> - (declare-sort |<mod>_s| 0) - The sort representing a state of module <mod>. - - (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...)) - This function must be asserted for each state to establish the - design hierarchy. - - ; yosys-smt2-input <wirename> <width> - ; yosys-smt2-output <wirename> <width> - ; yosys-smt2-register <wirename> <width> - ; yosys-smt2-wire <wirename> <width> - (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>)) - (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool) - For each port, register, and wire with the 'keep' attribute set an - accessor function is generated. Single-bit wires are returned as Bool, - multi-bit wires as BitVec. - - ; yosys-smt2-cell <submod> <instancename> - (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|) - There is a function like that for each hierarchical instance. It - returns the sort that represents the state of the sub-module that - implements the instance. - - (declare-fun |<mod>_is| (|<mod>_s|) Bool) - This function must be asserted 'true' for initial states, and 'false' - otherwise. - - (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...)) - This function must be asserted 'true' for initial states. For - non-initial states it must be left unconstrained. - - (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...)) - This function evaluates to 'true' if the states 'state' and - 'next_state' form a valid state transition. - - (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...)) - This function evaluates to 'true' if all assertions hold in the state. - - (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...)) - This function evaluates to 'true' if all assumptions hold in the state. - - ; yosys-smt2-assert <id> <filename:linenum> - (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...)) - Each $assert cell is converted into one of this functions. The function - evaluates to 'true' if the assert statement holds in the state. - - ; yosys-smt2-assume <id> <filename:linenum> - (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...)) - Each $assume cell is converted into one of this functions. The function - evaluates to 'true' if the assume statement holds in the state. - - ; yosys-smt2-cover <id> <filename:linenum> - (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...)) - Each $cover cell is converted into one of this functions. The function - evaluates to 'true' if the cover statement is activated in the state. - -Options: - - -verbose - this will print the recursive walk used to export the modules. - - -stbv - Use a BitVec sort to represent a state instead of an uninterpreted - sort. As a side-effect this will prevent use of arrays to model - memories. - - -stdt - Use SMT-LIB 2.6 style datatypes to represent a state instead of an - uninterpreted sort. - - -nobv - disable support for BitVec (FixedSizeBitVectors theory). without this - option multi-bit wires are represented using the BitVec sort and - support for coarse grain cells (incl. arithmetic) is enabled. - - -nomem - disable support for memories (via ArraysEx theory). this option is - implied by -nobv. only $mem cells without merged registers in - read ports are supported. call "memory" with -nordff to make sure - that no registers are merged into $mem read ports. '<mod>_m' functions - will be generated for accessing the arrays that are used to represent - memories. - - -wires - create '<mod>_n' functions for all public wires. by default only ports, - registers, and wires with the 'keep' attribute are exported. - - -tpl <template_file> - use the given template file. the line containing only the token '%%' - is replaced with the regular output of this command. - - -solver-option <option> <value> - emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write - the given option as a `(set-option ...)` command in the SMT-LIBv2. - -[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David -R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf - ---------------------------------------------------------------------------- - -Example: - -Consider the following module (test.v). We want to prove that the output can -never transition from a non-zero value to a zero value. - - module test(input clk, output reg [3:0] y); - always @(posedge clk) - y <= (y << 1) | ^y; - endmodule - -For this proof we create the following template (test.tpl). - - ; we need QF_UFBV for this proof - (set-logic QF_UFBV) - - ; insert the auto-generated code here - %% - - ; declare two state variables s1 and s2 - (declare-fun s1 () test_s) - (declare-fun s2 () test_s) - - ; state s2 is the successor of state s1 - (assert (test_t s1 s2)) - - ; we are looking for a model with y non-zero in s1 - (assert (distinct (|test_n y| s1) #b0000)) - - ; we are looking for a model with y zero in s2 - (assert (= (|test_n y| s2) #b0000)) - - ; is there such a model? - (check-sat) - -The following yosys script will create a 'test.smt2' file for our proof: - - read_verilog test.v - hierarchy -check; proc; opt; check -assert - write_smt2 -bv -tpl test.tpl test.smt2 - -Running 'cvc4 test.smt2' will print 'unsat' because y can never transition -from non-zero to zero in the test design. -\end{lstlisting} - -\section{write\_smv -- write design to SMV file} -\label{cmd:write_smv} -\begin{lstlisting}[numbers=left,frame=single] - write_smv [options] [filename] - -Write an SMV description of the current design. - - -verbose - this will print the recursive walk used to export the modules. - - -tpl <template_file> - use the given template file. the line containing only the token '%%' - is replaced with the regular output of this command. - -THIS COMMAND IS UNDER CONSTRUCTION -\end{lstlisting} - -\section{write\_spice -- write design to SPICE netlist file} -\label{cmd:write_spice} -\begin{lstlisting}[numbers=left,frame=single] - write_spice [options] [filename] - -Write the current design to an SPICE netlist file. - - -big_endian - generate multi-bit ports in MSB first order - (default is LSB first) - - -neg net_name - set the net name for constant 0 (default: Vss) - - -pos net_name - set the net name for constant 1 (default: Vdd) - - -buf DC|subckt_name - set the name for jumper element (default: DC) - (used to connect different nets) - - -nc_prefix - prefix for not-connected nets (default: _NC) - - -inames - include names of internal ($-prefixed) nets in outputs - (default is to use net numbers instead) - - -top top_module - set the specified module as design top module -\end{lstlisting} - -\section{write\_table -- write design as connectivity table} -\label{cmd:write_table} -\begin{lstlisting}[numbers=left,frame=single] - write_table [options] [filename] - -Write the current design as connectivity table. The output is a tab-separated -ASCII table with the following columns: - - module name - cell name - cell type - cell port - direction - signal - -module inputs and outputs are output using cell type and port '-' and with -'pi' (primary input) or 'po' (primary output) or 'pio' as direction. -\end{lstlisting} - -\section{write\_verilog -- write design to Verilog file} -\label{cmd:write_verilog} -\begin{lstlisting}[numbers=left,frame=single] - write_verilog [options] [filename] - -Write the current design to a Verilog file. - - -sv - with this option, SystemVerilog constructs like always_comb are used - - -norename - without this option all internal object names (the ones with a dollar - instead of a backslash prefix) are changed to short names in the - format '_<number>_'. - - -renameprefix <prefix> - insert this prefix in front of auto-generated instance names - - -noattr - with this option no attributes are included in the output - - -attr2comment - with this option attributes are included as comments in the output - - -noexpr - without this option all internal cells are converted to Verilog - expressions. - - -siminit - add initial statements with hierarchical refs to initialize FFs when - in -noexpr mode. - - -nodec - 32-bit constant values are by default dumped as decimal numbers, - not bit pattern. This option deactivates this feature and instead - will write out all constants in binary. - - -decimal - dump 32-bit constants in decimal and without size and radix - - -nohex - constant values that are compatible with hex output are usually - dumped as hex values. This option deactivates this feature and - instead will write out all constants in binary. - - -nostr - Parameters and attributes that are specified as strings in the - original input will be output as strings by this back-end. This - deactivates this feature and instead will write string constants - as binary numbers. - - -simple-lhs - Connection assignments with simple left hand side without - concatenations. - - -extmem - instead of initializing memories using assignments to individual - elements, use the '$readmemh' function to read initialization data - from a file. This data is written to a file named by appending - a sequential index to the Verilog filename and replacing the extension - with '.mem', e.g. 'write_verilog -extmem foo.v' writes 'foo-1.mem', - 'foo-2.mem' and so on. - - -defparam - use 'defparam' statements instead of the Verilog-2001 syntax for - cell parameters. - - -blackboxes - usually modules with the 'blackbox' attribute are ignored. with - this option set only the modules with the 'blackbox' attribute - are written to the output file. - - -selected - only write selected modules. modules must be selected entirely or - not at all. - - -v - verbose output (print new names of all renamed wires and cells) - -Note that RTLIL processes can't always be mapped directly to Verilog -always blocks. This frontend should only be used to export an RTLIL -netlist, i.e. after the "proc" pass has been used to convert all -processes to logic networks and registers. A warning is generated when -this command is called on a design with RTLIL processes. -\end{lstlisting} - -\section{write\_xaiger -- write design to XAIGER file} -\label{cmd:write_xaiger} -\begin{lstlisting}[numbers=left,frame=single] - write_xaiger [options] [filename] - -Write the top module (according to the (* top *) attribute or if only one module -is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, (optionally -$_DFF_N_, $_DFF_P_), or non (* abc9_box *) cells will be converted into psuedo- -inputs and pseudo-outputs. Whitebox contents will be taken from the equivalent -module in the '$abc9_holes' design, if it exists. - - -ascii - write ASCII version of AIGER format - - -map <filename> - write an extra file with port and box symbols - - -dff - write $_DFF_[NP]_ cells -\end{lstlisting} - -\section{xilinx\_dffopt -- Xilinx: optimize FF control signal usage} -\label{cmd:xilinx_dffopt} -\begin{lstlisting}[numbers=left,frame=single] - xilinx_dffopt [options] [selection] - -Converts hardware clock enable and set/reset signals on FFs to emulation -using LUTs, if doing so would improve area. Operates on post-techmap Xilinx -cells (LUT*, FD*). - - -lut4 - Assume a LUT4-based device (instead of a LUT6-based device). -\end{lstlisting} - -\section{xilinx\_dsp -- Xilinx: pack resources into DSPs} -\label{cmd:xilinx_dsp} -\begin{lstlisting}[numbers=left,frame=single] - xilinx_dsp [options] [selection] - -Pack input registers (A2, A1, B2, B1, C, D, AD; with optional enable/reset), -pipeline registers (M; with optional enable/reset), output registers (P; with -optional enable/reset), pre-adder and/or post-adder into Xilinx DSP resources. - -Multiply-accumulate operations using the post-adder with feedback on the 'C' -input will be folded into the DSP. In this scenario only, the 'C' input can be -used to override the current accumulation result with a new value, which will -be added to the multiplier result to form the next accumulation result. - -Use of the dedicated 'PCOUT' -> 'PCIN' cascade path is detected for 'P' -> 'C' -connections (optionally, where 'P' is right-shifted by 17-bits and used as an -input to the post-adder -- a pattern common for summing partial products to -implement wide multipliers). Limited support also exists for similar cascading -for A and B using '[AB]COUT' -> '[AB]CIN'. Currently, cascade chains are limited -to a maximum length of 20 cells, corresponding to the smallest Xilinx 7 Series -device. - -This pass is a no-op if the scratchpad variable 'xilinx_dsp.multonly' is set -to 1. - - -Experimental feature: addition/subtractions less than 12 or 24 bits with the -'(* use_dsp="simd" *)' attribute attached to the output wire or attached to -the add/subtract operator will cause those operations to be implemented using -the 'SIMD' feature of DSPs. - -Experimental feature: the presence of a `$ge' cell attached to the registered -P output implementing the operation "(P >= <power-of-2>)" will be transformed -into using the DSP48E1's pattern detector feature for overflow detection. - - -family {xcup|xcu|xc7|xc6v|xc5v|xc4v|xc6s|xc3sda} - select the family to target - default: xc7 -\end{lstlisting} - -\section{xilinx\_srl -- Xilinx shift register extraction} -\label{cmd:xilinx_srl} -\begin{lstlisting}[numbers=left,frame=single] - xilinx_srl [options] [selection] - -This pass converts chains of built-in flops (bit-level: $_DFF_[NP]_, $_DFFE_* -and word-level: $dff, $dffe) as well as Xilinx flops (FDRE, FDRE_1) into a -$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock -polarity, enable, and enable polarity (where relevant). -Flops with resets cannot be mapped to Xilinx devices and will not be inferred. - - -minlen N - min length of shift register (default = 3) - - -fixed - infer fixed-length shift registers. - - -variable - infer variable-length shift registers (i.e. fixed-length shifts where - each element also fans-out to a $shiftx cell). -\end{lstlisting} - -\section{zinit -- add inverters so all FF are zero-initialized} -\label{cmd:zinit} -\begin{lstlisting}[numbers=left,frame=single] - zinit [options] [selection] - -Add inverters as needed to make all FFs zero-initialized. - - -all - also add zero initialization to uninitialized FFs -\end{lstlisting} - |