From 6d5adb6a65d8a2c224f16cd3c8c5ede173223e29 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 6 Sep 2022 08:08:41 +0200 Subject: [PATCH] Update documentation --- manual/command-reference-manual.tex | 458 +++++++++++++++++----------- 1 file changed, 288 insertions(+), 170 deletions(-) diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index bc25c35cd..671fabb81 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -23,27 +23,29 @@ library to a target architecture. if no -script parameter is given, the following scripts are used: for -liberty/-genlib without -constr: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + &get -n; &dch -f; &nf {D}; &put for -liberty/-genlib with -constr: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p + 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; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2; - lutpack {S} + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; if; mfs2; lutpack {S} for -lut/-luts (different LUT sizes): - strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2 + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; if; mfs2 for -sop: - strash; ifraig; scorr; dc2; dretime; strash; dch -f; - cover {I} {P} + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; cover {I} {P} otherwise: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put + 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 @@ -125,7 +127,8 @@ library to a target architecture. 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: + 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 @@ -169,8 +172,8 @@ library to a target architecture. -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). + 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. @@ -190,8 +193,8 @@ you want to use ABC to convert your design into another format. \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 +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 : @@ -337,8 +340,8 @@ externally if you want to use ABC to convert your design into another format. 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. +(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. @@ -413,14 +416,14 @@ 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. + 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. + $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 @@ -438,33 +441,35 @@ the `abc9' script pass. Only fully-selected modules are supported. -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 + 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). + 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. + 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. + 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}. + 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 @@ -482,8 +487,8 @@ the `abc9' script pass. Only fully-selected modules are supported. -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. + by first recovering ABC9 boxes, and then stitching in the remaining + primary inputs and outputs. \end{lstlisting} \section{add -- add objects to the design} @@ -686,10 +691,10 @@ This pass transforms $bmux cells to trees of $mux cells. 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. +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`. @@ -807,8 +812,8 @@ Options: 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: +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 @@ -997,12 +1002,12 @@ of JSON. Frontend responds with data or error message by replying with exactly 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 parsed - by a built-in Yosys , allowing the RPC frontend to return any - convenient representation of the module. the derived module is cached, - so the response should be the same whenever the same set of parameters - is provided. + 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} @@ -1294,7 +1299,9 @@ and can be specified as allowed targets): - $_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) + +- 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) @@ -1307,7 +1314,8 @@ The following transformations are performed by this pass: 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 dffis available), an error is raised. +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} @@ -1330,7 +1338,8 @@ 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 argumentsthat would be passed to the dfflegalize pass. The design will not be +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} @@ -1340,8 +1349,8 @@ changed. 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. +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. @@ -1690,8 +1699,8 @@ inputs. 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. +to be preserved, even if quoted. stdin and stderr are not connected, while +stdout is logged unless the "-q" option is specified. -q @@ -2036,6 +2045,49 @@ model. 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] @@ -2227,8 +2279,8 @@ one-hot encoding and binary encoding is supported. \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 +This command generates testbench for the circuit using the given top-level +module and simulus signal from FST file -tb generated testbench name. @@ -2271,44 +2323,46 @@ and CC_L2T5 cells as created by LUT tree mapping. \begin{lstlisting}[numbers=left,frame=single] glift [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. +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: + 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: + 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`) + 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`) + y_t = a_t | b_t (like `-create-imprecise-model`) Options: @@ -2318,27 +2372,30 @@ Options: (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. + 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) + 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) + 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: + 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 @@ -2657,8 +2714,9 @@ 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. + 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. @@ -2830,7 +2888,8 @@ 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. +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 '@