diff options
Diffstat (limited to 'manual')
| -rw-r--r-- | manual/command-reference-manual.tex | 1340 |
1 files changed, 1200 insertions, 140 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index fea2354e6..bed6326e2 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -23,45 +23,47 @@ library to a target architecture. if no -script parameter is given, the following scripts are used: for -liberty without -constr: - strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; - map {D} + strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; + &nf {D}; &put for -liberty with -constr: - strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; - map {D}; buffer; upsize {D}; dnsize {D}; stime -p + strash; ifraig; 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; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs; - lutpack + strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2; + lutpack {S} for -lut/-luts (different LUT sizes): - strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs + strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2 for -sop: - strash; dc2; scorr; ifraig; retime -o; strash; dch -f; + strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P} otherwise: - strash; dc2; scorr; ifraig; retime -o; strash; dch -f; map + strash; ifraig; 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 without -constr: - retime -o {D}; map {D} + strash; dretime; map {D} for -liberty with -constr: - retime -o {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p + strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; + stime -p for -lut/-luts: - retime -o; if + strash; dretime; if for -sop: - retime -o; cover -I {I} -P {P} + strash; dretime; cover -I {I} -P {P} otherwise: - retime -o; map + strash; dretime; map -liberty <file> generate netlists for the specified cell library (using the liberty @@ -81,6 +83,8 @@ library to a target architecture. -D <picoseconds> set delay target. the string {D} in the default scripts above is replaced by this option when used, and an empty string otherwise. + this also replaces 'dretime' with 'dretime; retime -o {D}' in the + default scripts above. -I <num> maximum number of SOP inputs. @@ -90,6 +94,10 @@ library to a target architecture. maximum number of SOP products. (replaces {P} in the default scripts above) + -S <num> + maximum number of LUT inputs shared. + (replaces {S} in the default scripts above, default: -S 1) + -lut <width> generate netlist using luts of (max) the specified width. @@ -107,10 +115,21 @@ library to a target architecture. map to sum-of-product cells and inverters -g type1,type2,... - Map the the specified list of gate types. Supported gates types are: - AND, NAND, OR, NOR, XOR, XNOR, MUX, AOI3, OAI3, AOI4, OAI4. + Map to the specified list of gate types. Supported gates types are: + AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX, 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 + gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT + aig: AND NAND OR NOR ANDNOT ORNOT + + Prefix a gate type with a '-' to remove it from the list. For example + the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent. + -dff also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many clock domains are automatically partitioned in clock domains and each @@ -140,8 +159,12 @@ library to a target architecture. When neither -liberty nor -lut is used, the Yosys standard cell library is loaded into ABC before the ABC script is executed. -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.) +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 the 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} @@ -206,6 +229,22 @@ This command adds asserts to the design that assert that all parallel muxes additional constrained 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. + +Currently only $adff cells are supported by this pass. +\end{lstlisting} + \section{attrmap -- renaming attributes} \label{cmd:attrmap} \begin{lstlisting}[numbers=left,frame=single] @@ -268,6 +307,15 @@ Move or copy attributes on wires to the cells driving them. multiple times. \end{lstlisting} +\section{blackbox -- change type of cells in the design} +\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{cd -- a shortcut for 'select -module <name>'} \label{cmd:cd} \begin{lstlisting}[numbers=left,frame=single] @@ -284,6 +332,12 @@ to 'cd <celltype>'. cd .. +Remove trailing substrings that start with '.' in current module name until +the name of a module in the current design is generated, then switch to that +module. Otherwise clear the current selection. + + cd + This is just a shortcut for 'select -clear'. \end{lstlisting} @@ -303,10 +357,49 @@ This pass identifies the following problems in the current design: When called with -noinit then this command also checks for wires which have the 'init' attribute set. +When called with -initdrv then this command also checks for wires which have +the 'init' attribute set and aren't driven by a FF cell type. + When called with -assert then the command will produce an 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 folling options is given, +the command will operate on all constraint types: + + -assert $assert cells, representing assert(...) constraints + -assume $assume cells, representing assume(...) constraints + -live $live cells, representing assert(s_eventually ...) + -fair $fair cells, representing assume(s_eventually ...) + -cover $cover cells, representing cover() statements + +Exactly one of the following modes must be specified: + + -remove + remove the cells and thus constraints from the design + + -early + bypass FFs that only delay the activation of a constraint + + -delay <N> + delay activation of the constraint by <N> clock cycles + + -skip <N> + ignore activation of the constraint in the first <N> clock cycles + + -assert2assume + -assume2assert + -live2fair + -fair2live + change the roles of cells as indicated. this options can be combined +\end{lstlisting} + \section{chparam -- re-evaluate modules with new parameters} \label{cmd:chparam} \begin{lstlisting}[numbers=left,frame=single] @@ -321,6 +414,20 @@ passed in double quotes ("). List the available parameters of the selected modules. \end{lstlisting} +\section{chtype -- change type of cells in the design} +\label{cmd:chtype} +\begin{lstlisting}[numbers=left,frame=single] + chtype [options] [selection] + +Change the types of cells in the design. + + -set <type> + set the cell type to the given type + + -map <old_type> <new_type> + change cells types that match <old_type> to <new_type> +\end{lstlisting} + \section{clean -- remove unused cells and wires} \label{cmd:clean} \begin{lstlisting}[numbers=left,frame=single] @@ -376,7 +483,7 @@ be selected or an active module must be set using the 'cd' command. This command does not operate on module with processes. \end{lstlisting} -\section{connwrappers -- replace undef values with defined constants} +\section{connwrappers -- match width of input-output port pairs} \label{cmd:connwrappers} \begin{lstlisting}[numbers=left,frame=single] connwrappers [options] [selection] @@ -397,6 +504,14 @@ the driving cell. The options -signed, -unsigned, and -port can be specified multiple times. \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] @@ -519,6 +634,19 @@ evaluated in the other design. design -copy-to <name> [-as <new_mod_name>] [selection] Copy modules from the current design into the specified one. + + + design -import <name> [-as <new_top_name>] [selection] + +Import the specified design into the current design. The source design must +either have a selected top module or the selection must contain exactly one +module that is then used as top module for this command. + + + design -reset-vlog + +The Verilog front-end remembers defined macros and top-level declarations +between calls to 'read_verilog'. This command resets this memory. \end{lstlisting} \section{dff2dffe -- transform \$dff cells to \$dffe cells} @@ -546,8 +674,18 @@ $_DFF_P_, $_DFF_N_ and $_MUX_. -direct-match <pattern> like -direct for all DFF cell types matching the expression. this will use $__DFFE_* as <external_gate_type> matching the - internal gate type $_DFF_*_, except for $_DFF_[NP]_, which is - converted to $_DFFE_[NP]_. + internal gate type $_DFF_*_, and $__DFFSE_* for those matching + $_DFFS_*_, except for $_DFF_[NP]_, which is converted to + $_DFFE_[NP]_. +\end{lstlisting} + +\section{dff2dffs -- process sync set/reset with SR over CE priority} +\label{cmd:dff2dffs} +\begin{lstlisting}[numbers=left,frame=single] + dff2dffs [options] [selection] + +Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before +dff2dffe for SR over CE priority. \end{lstlisting} \section{dffinit -- set INIT param on FF cells} @@ -561,6 +699,11 @@ drives. (This is primarily used in FPGA flows.) -ff <cell_name> <output_port> <init_param> operate on the specified cell type. this option can be used multiple times. + + -highlow + use the string values "high" and "low" to represent a single-bit + initial value of 1 or 0. (multi-bit values are not supported in this + mode.) \end{lstlisting} \section{dfflibmap -- technology mapping of flip-flops} @@ -767,6 +910,10 @@ This command tries to prove $equiv cells using a simple direct SAT approach. -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 @@ -852,6 +999,10 @@ outputs. 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. @@ -956,6 +1107,64 @@ 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 + + -pout X,Y,... + Only allow parallel output from the counter to the listed cell types + (if not specified, parallel outputs are not restricted) +\end{lstlisting} + +\section{extract\_fa -- find and extract full/half adders} +\label{cmd:extract_fa} +\begin{lstlisting}[numbers=left,frame=single] + extract_fa [options] [selection] + +This pass extracts full/half adders from a gate-level design. + + -fa, -ha + Enable cell types (fa=full adder, ha=half adder) + All types are enabled if none of this options is used + + -d <int> + Set maximum depth for extracted logic cones (default=20) + + -b <int> + Set maximum breadth for extracted logic cones (default=6) + + -v + Verbose output +\end{lstlisting} + +\section{extract\_reduce -- converts gate chains into \$reduce\_* cells} +\label{cmd:extract_reduce} +\begin{lstlisting}[numbers=left,frame=single] + extract_reduce [options] [selection] + +converts gate chains into $reduce_* cells + +This command finds chains of $_AND_, $_OR_, and $_XOR_ cells and replaces them +with their corresponding $reduce_* cells. Because this command only operates on +these cell types, it is recommended to map the design to only these cell types +using the `abc -g` command. Note that, in some cases, it may be more effective +to map the design to only $_AND_ cells, run extract_reduce, map the remaining +parts of the design to AND/OR/XOR cells, and run extract_reduce a second time. + + -allow-off-chain + Allows matching of cells that have loads outside the chain. These cells + will be replicated and folded into the $reduce_* cell, but the original + cell will remain, driving its original loads. +\end{lstlisting} + \section{flatten -- flatten design} \label{cmd:flatten} \begin{lstlisting}[numbers=left,frame=single] @@ -1155,21 +1364,12 @@ one-hot encoding and binary encoding is supported. .map <old_bitpattern> <new_bitpattern> \end{lstlisting} -\section{greenpak4\_counters -- Extract GreenPak4 counter cells} -\label{cmd:greenpak4_counters} -\begin{lstlisting}[numbers=left,frame=single] - greenpak4_counters [options] [selection] - -This pass converts non-resettable or async resettable down counters to GreenPak4 -counter cells (All other GreenPak4 counter modes must be instantiated manually.) -\end{lstlisting} - -\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFFs} +\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches} \label{cmd:greenpak4_dffinv} \begin{lstlisting}[numbers=left,frame=single] greenpak4_dffinv [options] [selection] -Merge GP_INV cells with GP_DFF* cells. +Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells. \end{lstlisting} \section{help -- display help messages} @@ -1199,6 +1399,10 @@ needed. also check the design hierarchy. this generates an error when an unknown module is used as cell type. + -simcheck + like -check, but also thow an error if blackbox modules are + instantiated, and throw an error if the design has no top module + -purge_lib by default the hierarchy command will not remove library (blackbox) modules. use this option to also remove unused blackbox modules. @@ -1212,6 +1416,11 @@ needed. per default this pass also converts positional arguments in cells to arguments using port names. this option disables this behavior. + -keep_portwidths + per default this pass adjusts the port width on cells that are + module instances when the width does not match the module port. this + option disables this behavior. + -nokeep_asserts per default this pass sets the "keep" attribute on all modules that directly or indirectly contain one or more $assert cells. this @@ -1416,6 +1625,18 @@ When no active module is selected, this prints a list of modules. When an active module is selected, this prints a list of objects in the module. \end{lstlisting} +\section{ltp -- print longest topological path} +\label{cmd:ltp} +\begin{lstlisting}[numbers=left,frame=single] + ltp [options] [selection] + +This command prints the longest topological path in the design. (Only considers +paths within a single module, so the design must be flattened.) + + -noff + automatically exclude FF cell types +\end{lstlisting} + \section{lut2mux -- convert \$lut to \$\_MUX\_} \label{cmd:lut2mux} \begin{lstlisting}[numbers=left,frame=single] @@ -1582,6 +1803,15 @@ This pass adds additional circuitry that emulates the Verilog simulation behavior for out-of-bounds memory reads and writes. \end{lstlisting} +\section{memory\_nordff -- extract read port FFs from memories} +\label{cmd:memory_nordff} +\begin{lstlisting}[numbers=left,frame=single] + memory_nordff [options] [selection] + +This pass extracts FFs from memory read ports. This results in a netlist +similar to what one would get from calling memory_dff with -nordff. +\end{lstlisting} + \section{memory\_share -- consolidate memory ports} \label{cmd:memory_share} \begin{lstlisting}[numbers=left,frame=single] @@ -1745,6 +1975,15 @@ This pass only operates on completely selected modules without processes. also remove internal nets if they have a public name \end{lstlisting} +\section{opt\_demorgan -- Optimize reductions with DeMorgan equivalents} +\label{cmd:opt_demorgan} +\begin{lstlisting}[numbers=left,frame=single] + opt_demorgan [selection] + +This pass pushes inverters through $reduce_* cells if this will reduce the +overall gate count of the circuit +\end{lstlisting} + \section{opt\_expr -- perform const folding and simple expression rewriting} \label{cmd:opt_expr} \begin{lstlisting}[numbers=left,frame=single] @@ -1884,15 +2123,16 @@ on partly selected designs. -memx simulate verilog simulation behavior for out-of-bounds memory accesses - using the 'memory_memx' pass. This option implies -nordff. + using the 'memory_memx' pass. -nomem do not run any of the memory_* passes - -nordff - passed to 'memory_dff'. prohibits merging of FFs into memory read ports + -rdff + do not pass -nordff to 'memory_dff'. This enables merging of FFs into + memory read ports. - -nokeepdc + -nokeepdc do not call opt_* with -keepdc -run <from_label>[:<to_label>] @@ -2058,6 +2298,38 @@ Note: This implementation of a quadratic wirelength placer uses exact dense matrix operations. It is only a toy-placer for small circuits. \end{lstlisting} +\section{read -- load HDL designs} +\label{cmd:read} +\begin{lstlisting}[numbers=left,frame=single] + read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>.. + +Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support +is only available via Verific.) + +Additional -D<macro>[=<value>] options may be added after the option indicating +the language version (and before file names) to set additional verilog defines. + + + read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>.. + +Load the specified VHDL files. (Requires Verific.) + + + read -define <macro>[=<value>].. + +Set global Verilog/SystemVerilog defines. + + + read -undef <macro>.. + +Unset global Verilog/SystemVerilog defines. + + + read -incdir <directory> + +Add directory to global Verilog/SystemVerilog include directories. +\end{lstlisting} + \section{read\_blif -- read BLIF file} \label{cmd:read_blif} \begin{lstlisting}[numbers=left,frame=single] @@ -2067,6 +2339,10 @@ Load modules from a BLIF file into the current design. -sop Create $sop cells instead of $lut cells + + -wideports + Merge ports that match the pattern 'name[int]' into a single + multi-bit port 'name'. \end{lstlisting} \section{read\_ilang -- read modules from ilang file} @@ -2078,6 +2354,15 @@ Load modules from an ilang file to the current design. (ilang is a text representation of a design in yosys's internal format.) \end{lstlisting} +\section{read\_json -- read JSON file} +\label{cmd:read_json} +\begin{lstlisting}[numbers=left,frame=single] + read_json [filename] + +Load modules from a JSON file into the current design See "help write_json" +for a description of the file format. +\end{lstlisting} + \section{read\_liberty -- read cells from liberty file} \label{cmd:read_liberty} \begin{lstlisting}[numbers=left,frame=single] @@ -2088,9 +2373,13 @@ Read cells from liberty file as modules into current design. -lib only create empty blackbox modules - -ignore_redef + -nooverwrite ignore re-definitions of modules. (the default behavior is to - create an error message.) + create an error message if the existing module is not a blackbox + module, and overwrite the existing module if it is a blackbox module.) + + -overwrite + overwrite existing modules with the same name -ignore_miss_func ignore cells with missing function specification of outputs @@ -2099,6 +2388,9 @@ Read cells from liberty file as modules into current design. ignore cells with a missing or invalid direction specification on a pin + -ignore_miss_data_latch + ignore latches with missing data and/or enable pins + -setattr <attribute_name> set the specified attribute (to the value 1) on all loaded modules \end{lstlisting} @@ -2131,6 +2423,9 @@ Verilog-2005 is supported. -dump_ast2 dump abstract syntax tree (after simplification) + -no_dump_ptr + do not include hex memory addresses in dump (easier to diff dumps) + -dump_vlog dump ast as Verilog code (after simplification) @@ -2190,9 +2485,13 @@ Verilog-2005 is supported. -icells interpret cell types starting with '$' as internal cell types - -ignore_redef + -nooverwrite ignore re-definitions of modules. (the default behavior is to - create an error message.) + create an error message if the existing module is not a black box + module, and overwrite the existing module otherwise.) + + -overwrite + overwrite existing modules with the same name -defer only read the abstract syntax tree and defer actual compilation @@ -2221,6 +2520,10 @@ verilog input, but has not very good error reporting. It generally is recommended to use a simulator (for example Icarus Verilog) for checking the syntax of the code, rather than to rely on read_verilog for that. +Depending on if read_verilog is run in -formal mode, either the macro +SYNTHESIS or FORMAL is defined automatically. In addition, read_verilog +always defines the macro YOSYS. + See the Yosys README file for a list of non-standard Verilog features supported by the Yosys Verilog front-end. \end{lstlisting} @@ -2251,6 +2554,15 @@ with public names. This ignores all selected ports. Rename top module. \end{lstlisting} +\section{rmports -- remove module ports with no connections} +\label{cmd:rmports} +\begin{lstlisting}[numbers=left,frame=single] + rmports [selection] + +This pass identifies ports in the selected modules which are not used or +driven and removes them. +\end{lstlisting} + \section{sat -- solve a SAT problem in the circuit} \label{cmd:sat} \begin{lstlisting}[numbers=left,frame=single] @@ -2457,11 +2769,9 @@ design. are assumed to be bidirectional 'inout' ports. -set_attr <name> <value> - -set_cell_attr <name> <value> - -set_wire_attr <name> <value> - set the specified attribute on all cells and/or wires that are part of - a logic loop. the special token {} in the value is replaced with a - unique identifier for the logic loop. + set the specified attribute on all cells that are part of a logic + loop. the special token {} in the value is replaced with a unique + identifier for the logic loop. -select replace the current selection with a selection of all cells and wires @@ -2497,7 +2807,7 @@ of the design to operate on. This command can be used to modify and view this list of selected objects. Note that many commands support an optional [selection] argument that can be -used to override the global selection for the command. The syntax of this +used to YS_OVERRIDE the global selection for the command. The syntax of this optional argument is identical to the syntax of the <selection> argument described here. @@ -2728,17 +3038,29 @@ The -type option can be used to change the cell type of the selected cells. \begin{lstlisting}[numbers=left,frame=single] setundef [options] [selection] -This command replaced undef (x) constants with defined (0/1) constants. +This command replaces undef (x) constants with defined (0/1) constants. -undriven also set undriven nets to constant values + -expose + also expose undriven nets as inputs (use with -undriven) + -zero replace with bits cleared (0) -one replace with bits set (1) + -undef + replace with undef (x) bits, may be used with -undriven + + -anyseq + replace with $anyseq drivers (for formal) + + -anyconst + replace with $anyconst drivers (for formal) + -random <seed> replace with random bits using the specified integer als seed value for the random number generator. @@ -2821,6 +3143,7 @@ to a graphics file (usually SVG or PostScript). -viewer <viewer> Run the specified command with the graphics file as parameter. + On Windows, this pauses yosys until the viewer exits. -format <format> Generate a graphics file in the specified format. Use 'dot' to just @@ -2882,7 +3205,7 @@ to a graphics file (usually SVG or PostScript). do not add the module name as graph title to the dot file When no <format> is specified, 'dot' is used. When no <format> and <viewer> is -specified, 'xdot' is used to display the schematic. +specified, 'xdot' is used to display the schematic (POSIX systems only). The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>', unless another prefix is specified using -prefix <prefix>. @@ -2949,6 +3272,47 @@ will use the same interface as the original $_DFF_*_ cells. The cell parameter map to greenpak4 shift registers. \end{lstlisting} +\section{sim -- simulate the circuit} +\label{cmd:sim} +\begin{lstlisting}[numbers=left,frame=single] + sim [options] [top-level] + +This command simulates the circuit using the given top-level module. + + -vcd <filename> + write the simulation results to the given VCD file + + -clock <portname> + name of top-level clock input + + -clockn <portname> + name of top-level clock input (inverse polarity) + + -reset <portname> + name of top-level reset input (active high) + + -resetn <portname> + name of top-level inverted reset input (active low) + + -rstlen <integer> + number of cycles reset should stay active (default: 1) + + -zinit + zero-initialize all uninitialized regs and memories + + -n <integer> + number of cycles to simulate (default: 20) + + -a + include all nets in VCD output, not just those with public names + + -w + writeback mode: use final simulation state as new init state + + -d + enable debug output +\end{lstlisting} + \section{simplemap -- mapping simple coarse-grain cells} \label{cmd:simplemap} \begin{lstlisting}[numbers=left,frame=single] @@ -2963,22 +3327,6 @@ primitives. The following internal cell types are mapped by this pass: $sr, $ff, $dff, $dffsr, $adff, $dlatch \end{lstlisting} -\section{singleton -- create singleton modules} -\label{cmd:singleton} -\begin{lstlisting}[numbers=left,frame=single] - singleton [selection] - -By default, a module that is instantiated by several other modules is only -kept once in the design. This preserves the original modularity of the design -and reduces the overall size of the design in memory. But it prevents certain -optimizations and other operations on the design. This pass creates singleton -modules for all selected cells. The created modules are marked with the -'singleton' attribute. - -This commands only operates on modules that by themself have the 'singleton' -attribute set (the 'top' module is a singleton implicitly). -\end{lstlisting} - \section{splice -- create explicit splicing cells} \label{cmd:splice} \begin{lstlisting}[numbers=left,frame=single] @@ -3122,6 +3470,9 @@ on partly selected designs. -nordff passed to 'memory'. prohibits merging of FFs into memory read ports + -noshare + do not run SAT-based resource sharing + -run <from_label>[:<to_label>] only run the commands between the labels (see below). an empty from label is synonymous to 'begin', and empty to label is @@ -3164,6 +3515,344 @@ The following commands are executed by this synthesis command: check \end{lstlisting} +\section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.} +\label{cmd:synth_achronix} +\begin{lstlisting}[numbers=left,frame=single] + synth_achronix [options] + +This command runs synthesis for Achronix Speedster eFPGAs. This work is still experimental. + + -top <module> + use the specified module as top module (default='top') + + -vout <file> + write the design to the specified Verilog netlist file. writing of an + output file is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -sv -lib +/achronix/speedster22i/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + deminout + + coarse: + synth -run coarse + + fine: + opt -fast -mux_undef -undriven -fine -full + memory_map + opt -undriven -fine + dffsr2dff + dff2dffe -direct-match $_DFF_* + opt -fine + techmap -map +/techmap.v + opt -full + clean -purge + setundef -undriven -zero + abc -markgroups -dff (only if -retime) + + map_luts: + abc -lut 4 + clean + + map_cells: + iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I + techmap -map +/achronix/speedster22i/cells_map.v + clean -purge + + check: + hierarchy -check + stat + check -noinit + + vout: + write_verilog -nodec -attr2comment -defparam -renameprefix syn_ <file-name> +\end{lstlisting} + +\section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs} +\label{cmd:synth_coolrunner2} +\begin{lstlisting}[numbers=left,frame=single] + synth_coolrunner2 [options] + +This command runs synthesis for Coolrunner-II CPLDs. This work is experimental. +It is intended to be used with https://github.com/azonenberg/openfpga as the +place-and-route. + + -top <module> + use the specified module as top module (default='top') + + -json <file> + write the design to the specified JSON file. writing of an output file + is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/coolrunner2/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + + coarse: + synth -run coarse + + fine: + opt -fast -full + techmap + techmap -map +/coolrunner2/cells_latch.v + dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib + + map_tff: + abc -g AND,XOR + clean + extract -map +/coolrunner2/tff_extract.v + + map_pla: + abc -sop -I 40 -P 56 + clean + + map_cells: + dfflibmap -liberty +/coolrunner2/xc2_dff.lib + dffinit -ff FDCP Q INIT + dffinit -ff FDCP_N Q INIT + dffinit -ff FTCP Q INIT + dffinit -ff FTCP_N Q INIT + dffinit -ff LDCP Q INIT + dffinit -ff LDCP_N Q INIT + coolrunner2_sop + iopadmap -bits -inpad IBUF O:I -outpad IOBUFE I:IO -inoutpad IOBUFE O:IO -toutpad IOBUFE E:I:IO -tinoutpad IOBUFE E:O:I:IO + attrmvcp -attr src -attr LOC t:IOBUFE n:* + attrmvcp -attr src -attr LOC -driven t:IBUF n:* + splitnets + clean + + check: + hierarchy -check + stat + check -noinit + + json: + write_json <file-name> +\end{lstlisting} + +\section{synth\_easic -- synthesis for eASIC platform} +\label{cmd:synth_easic} +\begin{lstlisting}[numbers=left,frame=single] + synth_easic [options] + +This command runs synthesis for eASIC platform. + + -top <module> + use the specified module as top module + + -vlog <file> + write the design to the specified structural Verilog file. writing of + an output file is omitted if this parameter is not specified. + + -etools <path> + set path to the eTools installation. (default=/opt/eTools) + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + +The following commands are executed by this synthesis command: + + begin: + read_liberty -lib <etools_phys_clk_lib> + read_liberty -lib <etools_logic_lut_lib> + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + + coarse: + synth -run coarse + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap + opt -fast + abc -dff (only if -retime) + opt_clean (only if -retime) + + map: + dfflibmap -liberty <etools_phys_clk_lib> + abc -liberty <etools_logic_lut_lib> + opt_clean + + check: + hierarchy -check + stat + check -noinit + + vlog: + write_verilog -noexpr -attr2comment <file-name> +\end{lstlisting} + +\section{synth\_ecp5 -- synthesis for ECP5 FPGAs} +\label{cmd:synth_ecp5} +\begin{lstlisting}[numbers=left,frame=single] + synth_ecp5 [options] + +This command runs synthesis for ECP5 FPGAs. + + -top <module> + use the specified module as top module + + -blif <file> + write the design to the specified BLIF file. writing of an output file + is omitted if this parameter is not specified. + + -edif <file> + write the design to the specified EDIF file. writing of an output file + is omitted if this parameter is not specified. + + -json <file> + write the design to the specified JSON file. writing of an output file + is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + -noccu2 + do not use CCU2 cells in output netlist + + -nodffe + do not use flipflops with CE in output netlist + + -nobram + do not use BRAM cells in output netlist + + -nodram + do not use distributed RAM cells in output netlist + + -nomux + do not use PFU muxes to implement LUTs larger than LUT4s + + -abc2 + run two passes of 'abc' for slightly improved logic density + + -vpr + generate an output netlist (and BLIF file) suitable for VPR + (this feature is experimental and incomplete) + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/ecp5/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + deminout + + coarse: + synth -run coarse + + bram: (skip if -nobram) + + dram: (skip if -nodram) + memory_bram -rules +/ecp5/dram.txt + techmap -map +/ecp5/drams_map.v + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap -map +/techmap.v -map +/ecp5/arith_map.v + abc -dff (only if -retime) + + map_ffs: + dffsr2dff + dff2dffs + opt_clean + dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_* + techmap -D NO_LUT -map +/ecp5/cells_map.v + opt_expr -mux_undef + simplemap + + map_luts: + abc (only if -abc2) + abc -lut 4:7 + clean + + map_cells: + techmap -map +/ecp5/cells_map.v (with -D NO_LUT in vpr mode) + clean + + check: + hierarchy -check + stat + check -noinit + + blif: + opt_clean -purge (vpr mode) + write_blif -attr -cname -conn -param <file-name> (vpr mode) + write_blif -gates -attr -param <file-name> (non-vpr mode) + + edif: + write_edif <file-name> + + json: + write_json <file-name> +\end{lstlisting} + \section{synth\_gowin -- synthesis for Gowin FPGAs} \label{cmd:synth_gowin} \begin{lstlisting}[numbers=left,frame=single] @@ -3228,7 +3917,7 @@ The following commands are executed by this synthesis command: check -noinit vout: - write_verilog -attr2comment -defparam -renameprefix gen <file-name> + write_verilog -nodec -attr2comment -defparam -renameprefix gen <file-name> \end{lstlisting} \section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs} @@ -3237,6 +3926,8 @@ The following commands are executed by this synthesis command: synth_greenpak4 [options] This command runs synthesis for GreenPAK4 FPGAs. This work is experimental. +It is intended to be used with https://github.com/azonenberg/openfpga as the +place-and-route. -top <module> use the specified module as top module (default='top') @@ -3276,12 +3967,13 @@ The following commands are executed by this synthesis command: synth -run coarse fine: - greenpak4_counters + extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14 clean opt -fast -mux_undef -undriven -fine memory_map opt -undriven -fine techmap + techmap -map +/greenpak4/cells_latch.v dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib opt -fast abc -dff (only if -retime) @@ -3323,14 +4015,18 @@ The following commands are executed by this synthesis command: This command runs synthesis for iCE40 FPGAs. -top <module> - use the specified module as top module (default='top') + use the specified module as top module -blif <file> write the design to the specified BLIF file. writing of an output file is omitted if this parameter is not specified. -edif <file> - write the design to the specified edif file. writing of an output file + write the design to the specified EDIF file. writing of an output file + is omitted if this parameter is not specified. + + -json <file> + write the design to the specified JSON file. writing of an output file is omitted if this parameter is not specified. -run <from_label>:<to_label> @@ -3347,12 +4043,19 @@ This command runs synthesis for iCE40 FPGAs. -nocarry do not use SB_CARRY cells in output netlist + -nodffe + do not use SB_DFFE* cells in output netlist + -nobram do not use SB_RAM40_4K* cells in output netlist -abc2 run two passes of 'abc' for slightly improved logic density + -vpr + generate an output netlist (and BLIF file) suitable for VPR + (this feature is experimental and incomplete) + The following commands are executed by this synthesis command: @@ -3384,7 +4087,7 @@ The following commands are executed by this synthesis command: map_ffs: dffsr2dff dff2dffe -direct-match $_DFF_* - techmap -map +/ice40/cells_map.v + techmap -D NO_LUT -map +/ice40/cells_map.v opt_expr -mux_undef simplemap ice40_ffinit @@ -3399,7 +4102,7 @@ The following commands are executed by this synthesis command: clean map_cells: - techmap -map +/ice40/cells_map.v + techmap -map +/ice40/cells_map.v (with -D NO_LUT in vpr mode) clean check: @@ -3408,10 +4111,116 @@ The following commands are executed by this synthesis command: check -noinit blif: - write_blif -gates -attr -param <file-name> + opt_clean -purge (vpr mode) + write_blif -attr -cname -conn -param <file-name> (vpr mode) + write_blif -gates -attr -param <file-name> (non-vpr mode) edif: write_edif <file-name> + + json: + write_json <file-name> +\end{lstlisting} + +\section{synth\_intel -- synthesis for Intel (Altera) FPGAs.} +\label{cmd:synth_intel} +\begin{lstlisting}[numbers=left,frame=single] + synth_intel [options] + +This command runs synthesis for Intel FPGAs. + + -family < max10 | a10gx | cyclone10 | cyclonev | cycloneiv | cycloneive> + generate the synthesis netlist for the specified family. + MAX10 is the default target if not family argument specified. + For Cyclone GX devices, use cycloneiv argument; For Cyclone E, use cycloneive. + Cyclone V and Arria 10 GX devices are experimental, use it with a10gx argument. + + -top <module> + use the specified module as top module (default='top') + + -vqm <file> + write the design to the specified Verilog Quartus Mapping File. Writing of an + output file is omitted if this parameter is not specified. + + -vpr <file> + write BLIF files for VPR flow experiments. The synthesized BLIF output file is not + compatible with the Quartus flow. Writing of an + output file is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noiopads + do not use altsyncram cells in output netlist + + -nobram + do not use altsyncram cells in output netlist + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + +The following commands are executed by this synthesis command: + + begin: + + family: + read_verilog -sv -lib +/intel/max10/cells_sim.v + read_verilog -sv -lib +/intel/common/m9k_bb.v + read_verilog -sv -lib +/intel/common/altpll_bb.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + deminout + + coarse: + synth -run coarse + + bram: (skip if -nobram) + memory_bram -rules +/intel/common/brams.txt + techmap -map +/intel/common/brams_map.v + + fine: + opt -fast -mux_undef -undriven -fine -full + memory_map + opt -undriven -fine + dffsr2dff + dff2dffe -direct-match $_DFF_* + opt -fine + techmap -map +/techmap.v + opt -full + clean -purge + setundef -undriven -zero + abc -markgroups -dff (only if -retime) + + map_luts: + abc -lut 4 + clean + + map_cells: + iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I (unless -noiopads) + techmap -map +/intel/max10/cells_map.v + dffinit -highlow -ff dffeas q power_up + clean -purge + + check: + hierarchy -check + stat + check -noinit + + vqm: + write_verilog -attr2comment -defparam -nohex -decimal -renameprefix syn_ <file-name> + + vpr: + opt_clean -purge + write_blif <file-name> \end{lstlisting} \section{synth\_xilinx -- synthesis for Xilinx FPGAs} @@ -3430,6 +4239,14 @@ compatible with 7-Series Xilinx devices. write the design to the specified edif file. writing of an output file is omitted if this parameter is not specified. + -blif <file> + write the design to the specified BLIF file. writing of an output file + is omitted if this parameter is not specified. + + -vpr + generate an output netlist (and BLIF file) suitable for VPR + (this feature is experimental and incomplete) + -run <from_label>:<to_label> only run the commands between the labels (see below). an empty from label is synonymous to 'begin', and empty to label is @@ -3448,7 +4265,6 @@ The following commands are executed by this synthesis command: read_verilog -lib +/xilinx/cells_sim.v read_verilog -lib +/xilinx/cells_xtra.v read_verilog -lib +/xilinx/brams_bb.v - read_verilog -lib +/xilinx/drams_bb.v hierarchy -check -top <top> flatten: (only if -flatten) @@ -3480,7 +4296,7 @@ The following commands are executed by this synthesis command: clean map_cells: - techmap -map +/xilinx/cells_map.v + techmap -map +/xilinx/cells_map.v (with -D NO_LUT in vpr mode) dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT clean @@ -3491,6 +4307,9 @@ The following commands are executed by this synthesis command: edif: (only if -edif) write_edif <file-name> + + blif: (only if -blif) + write_blif <file-name> \end{lstlisting} \section{tcl -- execute a TCL script file} @@ -3502,9 +4321,9 @@ This command executes the tcl commands in the specified file. Use 'yosys cmd' to run the yosys command 'cmd' from tcl. The tcl command 'yosys -import' can be used to import all yosys -commands directly as tcl commands to the tcl shell. The yosys -command 'proc' is wrapped using the tcl command 'procs' in order -to avoid a name collision with the tcl builtin command 'proc'. +commands directly as tcl commands to the tcl shell. Yosys commands +'proc' and 'rename' are wrapped to tcl commands 'procs' and 'renames' +in order to avoid a name collision with the built in commands. \end{lstlisting} \section{techmap -- generic technology mapper} @@ -3548,7 +4367,7 @@ file. -D <define>, -I <incdir> this options are passed as-is to the Verilog frontend for loading the map file. Note that the Verilog frontend is also called with the - '-ignore_redef' option set. + '-nooverwrite' option set. When a module in the map file has the 'techmap_celltype' attribute set, it will match cells with a type that match the text value of this attribute. Otherwise @@ -3629,7 +4448,7 @@ the design is connected to a constant value. The parameter is then set to the constant value. A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name -of the cell that is being replaced. +and attributes of the cell that is being replaced. See 'help extract' for a pass that does the opposite thing. @@ -3795,24 +4614,134 @@ This pass transforms $mux cells with 'z' inputs to tristate buffers. to non-tristate logic. this option implies -merge. \end{lstlisting} +\section{uniquify -- create unique copies of modules} +\label{cmd:uniquify} +\begin{lstlisting}[numbers=left,frame=single] + uniquify [selection] + +By default, a module that is instantiated by several other modules is only +kept once in the design. This preserves the original modularity of the design +and reduces the overall size of the design in memory. But it prevents certain +optimizations and other operations on the design. This pass creates unique +modules for all selected cells. The created modules are marked with the +'unique' attribute. + +This commands only operates on modules that by themself have the 'unique' +attribute set (the 'top' module is unique implicitly). +\end{lstlisting} + \section{verific -- load Verilog and VHDL designs using Verific} \label{cmd:verific} \begin{lstlisting}[numbers=left,frame=single] - verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>.. + verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>.. Load the specified Verilog/SystemVerilog files into Verific. +All files specified in one call to this command are one compilation unit. +Files passed to different calls to this command are treated as belonging to +different compilation units. + +Additional -D<macro>[=<value>] options may be added after the option indicating +the language version (and before file names) to set additional verilog defines. +The macros SYNTHESIS and VERIFIC are defined implicitly. + + + verific -formal <verilog-file>.. - verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>.. +Like -sv, but define FORMAL instead of SYNTHESIS. + + + verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>.. Load the specified VHDL files into Verific. - verific -import [-gates] {-all | <top-module>..} + verific -work <libname> {-sv|-vhdl|...} <hdl-file> + +Load the specified Verilog/SystemVerilog/VHDL file into the specified library. +(default library when -work is not present: "work") + + + verific -vlog-incdir <directory>.. + +Add Verilog include directories. + + + verific -vlog-libdir <directory>.. + +Add Verilog library directories. Verific will search in this directories to +find undefined modules. + + + verific -vlog-define <macro>[=<value>].. + +Add Verilog defines. + + + verific -vlog-undef <macro>.. + +Remove Verilog defines previously set with -vlog-define. + + + verific -set-error <msg_id>.. + verific -set-warning <msg_id>.. + verific -set-info <msg_id>.. + verific -set-ignore <msg_id>.. + +Set message severity. <msg_id> is the string in square brackets when a message +is printed, such as VERI-1209. + + + verific -import [options] <top-module>.. Elaborate the design for the specified top modules, import to Yosys and -reset the internal state of Verific. A gate-level netlist is created -when called with -gates. +reset the internal state of Verific. + +Import options: + + -all + Elaborate all modules, not just the hierarchy below the given top + modules. With this option the list of modules to import is optional. + + -gates + Create a gate-level netlist. + + -flatten + Flatten the design in Verific before importing. + + -extnets + Resolve references to external nets by adding module ports as needed. + + -autocover + Generate automatic cover statements for all asserts + + -v, -vv + Verbose log messages. (-vv is even more verbose than -v.) + +The following additional import options are useful for debugging the Verific +bindings (for Yosys and/or Verific developers): + + -k + Keep going after an unsupported verific primitive is found. The + unsupported primitive is added as blockbox module to the design. + This will also add all SVA related cells to the design parallel to + the checker logic inferred by it. + + -V + Import Verific netlist as-is without translating to Yosys cell types. + + -nosva + Ignore SVA properties, do not infer checker logic. + + -L <int> + Maximum number of ctrl bits for SVA checker FSMs (default=16). + + -n + Keep all Verific names on instances and nets. By default only + user-declared names are preserved. + + -d <dump_file> + Dump the Verific netlist as a verilog file. Visit http://verific.com/ for more information on Verific. \end{lstlisting} @@ -3837,40 +4766,19 @@ Push or pop the list of default options to a stack. Note that -push does not imply -clear. \end{lstlisting} -\section{vhdl2verilog -- importing VHDL designs using vhdl2verilog} -\label{cmd:vhdl2verilog} +\section{verilog\_defines -- define and undefine verilog defines} +\label{cmd:verilog_defines} \begin{lstlisting}[numbers=left,frame=single] - vhdl2verilog [options] <vhdl-file>.. - -This command reads VHDL source files using the 'vhdl2verilog' tool and the -Yosys Verilog frontend. - - -out <out_file> - do not import the vhdl2verilog output. instead write it to the - specified file. - - -vhdl2verilog_dir <directory> - do use the specified vhdl2verilog installation. this is the directory - that contains the setup_env.sh file. when this option is not present, - it is assumed that vhdl2verilog is in the PATH environment variable. + verilog_defines [options] - -top <top-entity-name> - The name of the top entity. This option is mandatory. +Define and undefine verilog preprocessor macros. -The following options are passed as-is to vhdl2verilog: - - -arch <architecture_name> - -unroll_generate - -nogenericeval - -nouniquify - -oldparser - -suppress <list> - -quiet - -nobanner - -mapfile <file> + -Dname[=definition] + define the preprocessor symbol 'name' and set its optional value + 'definition' -vhdl2verilog can be obtained from: -http://www.edautils.com/vhdl2verilog.html + -Uname[=definition] + undefine the preprocessor symbol 'name' \end{lstlisting} \section{wreduce -- reduce the word size of operations if possible} @@ -3892,6 +4800,38 @@ Options: flows that use the 'memory_memx' pass. \end{lstlisting} +\section{write\_aiger -- write design to AIGER file} +\label{cmd:write_aiger} +\begin{lstlisting}[numbers=left,frame=single] + write_aiger [options] [filename] + +Write the current design to an AIGER file. The design must be flattened and +must not contain any cell types except $_AND_, $_NOT_, simple FF types, +$assert and $assume cells, and $initstate cells. + +$assert and $assume cells are converted to AIGER bad state properties and +invariant constraints. + + -ascii + write ASCII version of AGIER format + + -zinit + convert FFs to zero-initialized FFs, adding additional inputs for + uninitialized FFs. + + -miter + design outputs are AIGER bad state properties + + -symbols + include a symbol table in the generated AIGER file + + -map <filename> + write an extra file with port and latch symbols + + -vmap <filename> + like -map, but more verbose +\end{lstlisting} + \section{write\_blif -- write design to BLIF file} \label{cmd:write_blif} \begin{lstlisting}[numbers=left,frame=single] @@ -3949,6 +4889,11 @@ file *.blif when any of this options is used. -cname use the non-standard .cname statement to write cell names + -iname, -iattr + enable -cname and -attr functionality for .names statements + (the .cname and .attr statements will be included in the BLIF + output after the truth table for the .names statement) + -blackbox write blackbox cells with .blackbox statement. @@ -3959,9 +4904,15 @@ file *.blif when any of this options is used. \section{write\_btor -- write design to BTOR file} \label{cmd:write_btor} \begin{lstlisting}[numbers=left,frame=single] - write_btor [filename] + write_btor [options] [filename] + +Write a BTOR description of the current design. -Write the current design to an BTOR file. + -v + Add comments and indentation to BTOR output file + + -s + Output only a single bad property for all asserts \end{lstlisting} \section{write\_edif -- write design to EDIF netlist file} @@ -3979,6 +4930,10 @@ Write the current design to an EDIF netlist file. if the design contains constant nets. use "hilomap" to map to custom constant drivers first) + -pvector {par|bra|ang} + sets the delimiting character for module port rename clauses to + parentheses, square brackets, or angle brackets. + Unfortunately there are different "flavors" of the EDIF file format. This command generates EDIF files for the Xilinx place&route tools. It might be necessary to make small modifications to this command when a different tool @@ -4003,6 +4958,14 @@ Inside a script the input file can also can a here-document: EOT \end{lstlisting} +\section{write\_firrtl -- write design to a FIRRTL file} +\label{cmd:write_firrtl} +\begin{lstlisting}[numbers=left,frame=single] + write_firrtl [options] [filename] + +Write a FIRRTL netlist of the current design. +\end{lstlisting} + \section{write\_ilang -- write design to ilang file} \label{cmd:write_ilang} \begin{lstlisting}[numbers=left,frame=single] @@ -4123,6 +5086,10 @@ values referenced above are vectors of this integers. Signal bits that are connected to a constant driver are denoted as string "0" or "1" instead of a number. +Numeric parameter and attribute values up to 32 bits are written as decimal +values. Numbers larger than that are written as string holding the binary +representation of the value. + For example the following Verilog code: module test(input x, y); @@ -4242,43 +5209,109 @@ Future version of Yosys might add support for additional fields in the JSON format. A program processing this format must ignore all unknown fields. \end{lstlisting} -\section{write\_smt2 -- write design to SMT-LIBv2 file} -\label{cmd:write_smt2} +\section{write\_simplec -- convert design to simple C code} +\label{cmd:write_simplec} \begin{lstlisting}[numbers=left,frame=single] - write_smt2 [options] [filename] + write_simplec [options] [filename] -Write a SMT-LIBv2 [1] description of the current design. For a module with name -'<mod>' this will declare the sort '<mod>_s' (state of the module) and the -functions operating on that state. +Write simple C code for simulating the design. The C code writen can be used to +simulate the design in a C environment, but the purpose of this command is to +generate code that works well with C-based formal verification. -The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions -are provided that can be used to access the values of the signals in the module. -By default only ports, registers, and wires with the 'keep' attribute set are -made available via such functions. With the -nobv option, multi-bit wires are -exported as separate functions of type Bool for the individual bits. Without --nobv multi-bit wires are exported as single functions of type BitVec. + -verbose + this will print the recursive walk used to export the modules. -The '<mod>_t' function evaluates to 'true' when the given pair of states -describes a valid state transition. + -i8, -i16, -i32, -i64 + set the maximum integer bit width to use in the generated code. -The '<mod>_a' function evaluates to 'true' when the given state satisfies -the asserts in the module. +THIS COMMAND IS UNDER CONSTRUCTION +\end{lstlisting} -The '<mod>_u' function evaluates to 'true' when the given state satisfies -the assumptions in the module. +\section{write\_smt2 -- write design to SMT-LIBv2 file} +\label{cmd:write_smt2} +\begin{lstlisting}[numbers=left,frame=single] + write_smt2 [options] [filename] -The '<mod>_i' function evaluates to 'true' when the given state conforms -to the initial state. Furthermore the '<mod>_is' function should be asserted -to be true for initial states in addition to '<mod>_i', and should be -asserted to be false for non-initial states. +Write a SMT-LIBv2 [1] description of the current design. For a module with name +'<mod>' this will declare the sort '<mod>_s' (state of the module) and will +define and declare functions operating on that state. + +The following SMT2 functions are generated for a module with name '<mod>'. +Some declarations/definitions are printed with a special comment. A prover +using the SMT2 files can use those comments to collect all relevant metadata +about the design. + + ; yosys-smt2-module <mod> + (declare-sort |<mod>_s| 0) + The sort representing a state of module <mod>. + + (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...)) + This function must be asserted for each state to establish the + design hierarchy. + + ; yosys-smt2-input <wirename> <width> + ; yosys-smt2-output <wirename> <width> + ; yosys-smt2-register <wirename> <width> + ; yosys-smt2-wire <wirename> <width> + (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>)) + (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool) + For each port, register, and wire with the 'keep' attribute set an + accessor function is generated. Single-bit wires are returned as Bool, + multi-bit wires as BitVec. + + ; yosys-smt2-cell <submod> <instancename> + (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|) + There is a function like that for each hierarchical instance. It + returns the sort that represents the state of the sub-module that + implements the instance. + + (declare-fun |<mod>_is| (|<mod>_s|) Bool) + This function must be asserted 'true' for initial states, and 'false' + otherwise. + + (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...)) + This function must be asserted 'true' for initial states. For + non-initial states it must be left unconstrained. + + (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...)) + This function evaluates to 'true' if the states 'state' and + 'next_state' form a valid state transition. + + (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...)) + This function evaluates to 'true' if all assertions hold in the state. + + (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...)) + This function evaluates to 'true' if all assumptions hold in the state. + + ; yosys-smt2-assert <id> <filename:linenum> + (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...)) + Each $assert cell is converted into one of this functions. The function + evaluates to 'true' if the assert statement holds in the state. + + ; yosys-smt2-assume <id> <filename:linenum> + (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...)) + Each $assume cell is converted into one of this functions. The function + evaluates to 'true' if the assume statement holds in the state. + + ; yosys-smt2-cover <id> <filename:linenum> + (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...)) + Each $cover cell is converted into one of this functions. The function + evaluates to 'true' if the cover statement is activated in the state. -For hierarchical designs, the '<mod>_h' function must be asserted for each -state to establish the design hierarchy. The '<mod>_h <cellname>' function -evaluates to the state corresponding to the given cell within <mod>. +Options: -verbose this will print the recursive walk used to export the modules. + -stbv + Use a BitVec sort to represent a state instead of an uninterpreted + sort. As a side-effect this will prevent use of arrays to model + memories. + + -stdt + Use SMT-LIB 2.6 style datatypes to represent a state instead of an + uninterpreted sort. + -nobv disable support for BitVec (FixedSizeBitVectors theory). without this option multi-bit wires are represented using the BitVec sort and @@ -4394,6 +5427,25 @@ Write the current design to an SPICE netlist file. set the specified module as design top module \end{lstlisting} +\section{write\_table -- write design as connectivity table} +\label{cmd:write_table} +\begin{lstlisting}[numbers=left,frame=single] + write_table [options] [filename] + +Write the current design as connectivity table. The output is a tab-separated +ASCII table with the following columns: + + module name + cell name + cell type + cell port + direction + signal + +module inputs and outputs are output using cell type and port '-' and with +'pi' (primary input) or 'po' (primary output) or 'pio' as direction. +\end{lstlisting} + \section{write\_verilog -- write design to Verilog file} \label{cmd:write_verilog} \begin{lstlisting}[numbers=left,frame=single] @@ -4424,6 +5476,14 @@ Write the current design to a Verilog file. not bit pattern. This option deactivates this feature and instead will write out all constants in binary. + -decimal + dump 32-bit constants in decimal and without size and radix + + -nohex + constant values that are compatible with hex output are usually + dumped as hex values. This option deactivates this feature and + instead will write out all constants in binary. + -nostr Parameters and attributes that are specified as strings in the original input will be output as strings by this back-end. This |