From 1eec255e60f2854b4dd1fa212f02d57eb31c9f19 Mon Sep 17 00:00:00 2001 From: KrystalDelusion Date: Thu, 8 Dec 2022 05:54:08 +1300 Subject: Removing manual files --- manual/command-reference-manual.tex | 9592 ----------------------------------- 1 file changed, 9592 deletions(-) delete mode 100644 manual/command-reference-manual.tex (limited to 'manual/command-reference-manual.tex') 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 - use the specified command instead of "/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script - use the specified ABC script file instead of the default script. - - if 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 - generate netlists for the specified cell library (using the liberty - file format). - - -genlib - generate netlists for the specified cell library (using the SIS Genlib - file format). - - -constr - pass this file with timing constraints to ABC. - use with -liberty/-genlib. - - a constr file contains two lines: - set_driving_cell - set_load - - 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 - 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 - maximum number of SOP inputs. - (replaces {I} in the default scripts above) - - -P - maximum number of SOP products. - (replaces {P} in the default scripts above) - - -S - maximum number of LUT inputs shared. - (replaces {S} in the default scripts above, default: -S 1) - - -lut - generate netlist using luts of (max) the specified width. - - -lut : - generate netlist using luts of (max) the specified width . All - luts with width <= have constant cost. for luts larger than - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -luts ,,,:,.. - 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 [!][,[!]] - 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 : - 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 - use the specified command instead of "/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script - use the specified ABC script file instead of the default script. - - if 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 - 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 - generate netlist using luts of (max) the specified width. - - -lut : - generate netlist using luts of (max) the specified width . All - luts with width <= have constant cost. for luts larger than - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -lut - pass this file with lut library to ABC. - - -luts ,,,:,.. - generate netlist using luts. Use the specified costs for luts with 1, - 2, 3, .. inputs. - - -maxlut - 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 - 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 _$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 (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 /input.lut (skip if '-lut' or '-luts') - abc9_ops -write_box /input.box (skip if '-box') - write_xaiger -map /input.sym [-dff] /input.xaig - abc9_exe [options] -cwd -lut [/input.lut] -box [/input.box] - read_aiger -xaiger -wideports -module_name $abc9 -map /input.sym /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 - use the specified command instead of "/yosys-abc" to execute ABC. - This can e.g. be used to call a specific version of ABC or a wrapper. - - -script - use the specified ABC script file instead of the default script. - - if 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 - 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 - generate netlist using luts of (max) the specified width. - - -lut : - generate netlist using luts of (max) the specified width . All - luts with width <= have constant cost. for luts larger than - the area cost doubles with each additional input bit. the delay cost - is still constant for all lut widths. - - -lut - pass this file with lut library to ABC. - - -luts ,,,:,.. - 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 - pass this file with box library to ABC. - - -cwd - 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 = *) 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 - pre-compute the lut library by analysing all modules marked with - (* abc9_lut= *). - - -write_lut - write the pre-computed lut library to . - - -prep_box - pre-compute the box library by analysing all modules marked with - (* abc9_box *). - - -write_box - write the pre-computed box library to . - - -reintegrate - for each selected module, re-intergrate the module '$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 [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} [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 [selection] - -Like 'add -input', but also connect the signal between instances of the -selected modules. - - - add {-assert|-assume|-live|-fair|-cover} [-if ] - -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 - -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 - Match attribute names case-insensitively and set it to the specified - name. - - -rename - Rename attributes as specified - - -map = = - Map key/value pairs as indicated. - - -imap = = - Like -map, but use case-insensitive match for when - it is a string value. - - -remove = - 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 - 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 | -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 | -command "" - use this script file or command to crash Yosys. required. - - -yosys - use this Yosys binary. if not specified, `yosys` is used. - - -grep "" - 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 "" - child process wrapping command, e.g., "timeout 30", or valgrind. -\end{lstlisting} - -\section{cd -- a shortcut for 'select -module '} -\label{cmd:cd} -\begin{lstlisting}[numbers=left,frame=single] - cd - -This is just a shortcut for 'select -module '. - - - cd - -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 '. - - - 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 - delay activation of the constraint by clock cycles - - -skip - ignore activation of the constraint in the first 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 - set the cell type to the given type - - -map - change cells types that match to -\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 : - 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 : - 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 - -Create a connection. This is equivalent to adding the statement 'assign - = ;' to the Verilog input. Per default, all existing -drivers for are unconnected. This can be overwritten by using -the -nounset option. - - - connect [-nomap] -unset - -Unconnect all existing drivers for the specified expression. - - - connect [-nomap] [-assert] -port - -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 [args...] - connect_rpc -path - -Load modules using an out-of-process frontend. - - -exec [args...] - run with arguments [args...]. send requests on stdin, read - responses from stdout. - - -path - connect to Unix domain socket at . (Unix) - connect to bidirectional byte-type named pipe at . (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": ["", ...]} - <- {"error": ""} - 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 is instantiated in the design. - - -> {"method": "derive", "module": ", "parameters": { - "": {"type": "[unsigned|signed|string|real]", - "value": ""}, ...}} - <- {"frontend": "[rtlil|verilog|...]","source": ""}} - <- {"error": ""} - request for the module to be derived for a specific set of - parameters. starts with \ for named parameters, and with $ - for unnamed parameters, which are numbered starting at 1. - for integer parameters is always specified as a binary string of - unlimited precision. the returned by the frontend is - hygienically parsedby a built-in Yosys , 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 - -unsigned - consider the specified signed/unsigned wrapper output - - -port - 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 - -Save the current design under the given name. - - - design -stash - -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 - -Reset the current design and load the design previously saved under the given -name. - - - design -copy-from [-as ] - -Copy modules from the specified design into the current one. The selection is -evaluated in the other design. - - - design -copy-to [-as ] [selection] - -Copy modules from the current design into the specified one. - - - design -import [-as ] [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 - -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 - 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 - 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 - specifies a supported group of FF cells. - is a yosys internal fine cell name, where ? characters can be - as a wildcard matching any character. 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 - 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 - 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 [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 - write to the specified file. - - -a - 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 - 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 cycles (the -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 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 - Do not match cells or signals that match the names in the file. - - -encfile - 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 : - 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 - expand the modules in this file before proving equivalence. this is - useful for handling architecture-specific primitives. - - -blacklist - 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 ... - - prove: - clk2fflogic (only with -multiclock) - async2sync (only with -async2sync) - equiv_make -blacklist ... 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 - 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 - 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 - 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 - set the specified signal to the specified value. - - -set-undef - set all unspecified source signals to undef (x) - - -table - create a truth table using the specified input signals - - -show - 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 - 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 - Generate an error if the specified regex does not match any line - in subprocess's stdout. May be specified multiple times. - - -not-expect-stdout - 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 - 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 [options] [selection] - extract -mine [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 - use the modules in this file as reference. This option can be used - multiple times. - - -map % - 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 - 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 ,[,...] - Register a set of swappable ports for a needle cell type. - This option can be used multiple times. - - -perm ,[,...] ,[,...] - Register a valid permutation of swappable ports for a needle - cell type. This option can be used multiple times. - - -cell_attr - Attributes on cells with the given name must match. - - -wire_attr - Attributes on wires with the given name must match. - - -ignore_parameters - Do not use parameters when matching cells. - - -ignore_param - 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 - mine for frequent subcircuits and write them to the given RTLIL file - - -mine_cells_span - only mine for subcircuits with the specified number of cells - default value: 3 5 - - -mine_min_freq - only mine for subcircuits with at least the specified number of matches - default value: 10 - - -mine_limit_matches_per_module - when calculating the number of matches for a subcircuit, don't count - more than the specified number of matches per module - - -mine_max_fanout - don't consider internal signals with more than 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 - Set maximum depth for extracted logic cones (default=20) - - -b - 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 : - 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 [,,...] - 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] - -This pass creates init constraints (for example for reset sequences) in a formal -model. - - -seq - 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 - Add constant value constraint - - -posedge - -negedge - 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 - stop after reduction operations. this is mostly used for - debugging the freduce command itself. - - -dump - dump the design to __.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 - specify the encoding scheme used for FSMs without the - 'fsm_encoding' attribute or with the attribute set to `auto'. - - -fm_set_fsm_file - generate a file containing the mapping from old to new FSM encoding - in form of Synopsys Formality set_fsm_* commands. - - -encfile - write the mappings from old to new FSM encoding to a file in the - following format: - - .fsm - .map -\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 - generated testbench name. - files .v and .txt are created as result. - - -r - read simulation FST file - - -clock - name of top-level clock input - - -clockn - name of top-level clock input (inverse polarity) - - -scope - scope of simulation top model - - -start