diff options
Diffstat (limited to 'manual/command-reference-manual.tex')
| -rw-r--r-- | manual/command-reference-manual.tex | 1188 |
1 files changed, 1074 insertions, 114 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 047ec4214..425d89b67 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -16,7 +16,7 @@ library to a target architecture. use the specified ABC script file instead of the default script. if <file> starts with a plus sign (+), then the rest of the filename - string is interprated as the command string to be passed to ABC. the + 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. @@ -79,6 +79,15 @@ library to a target architecture. the area cost doubles with each additional input bit. the delay cost is still constant for all lut widths. + -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,.. + generate netlist using luts. Use the specified costs for luts with 1, + 2, 3, .. inputs. + + -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. + (The NOT gate is always added to this list automatically.) + -dff also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many clock domains are automatically partitioned in clock domains and each @@ -90,7 +99,7 @@ library to a target architecture. -keepff set the "keep" attribute on flip-flop output wires. (and thus preserve - them, for example for equivialence checking.) + them, for example for equivalence checking.) -nocleanup when this option is used, the temporary files created by this pass @@ -136,6 +145,18 @@ Like 'add -input', but also connect the signal between instances of the selected modules. \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 +\end{lstlisting} + \section{alumacc -- extract ALU and MACC cells} \label{cmd:alumacc} \begin{lstlisting}[numbers=left,frame=single] @@ -156,7 +177,7 @@ This is just a shortcut for 'select -module <modname>'. cd <cellname> When no module with the specified name is found, but there is a cell -with the specified name in the current module, then this is equivialent +with the specified name in the current module, then this is equivalent to 'cd <celltype>'. cd .. @@ -164,6 +185,40 @@ to 'cd <celltype>'. 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 + +When called with -noinit then this command also checks for wires which have +the 'init' attribute set. + +When called with -assert then the command will produce an error if any +problems are found in the current design. +\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{clean -- remove unused cells and wires} \label{cmd:clean} \begin{lstlisting}[numbers=left,frame=single] @@ -183,8 +238,8 @@ in -purge mode between the commands. \begin{lstlisting}[numbers=left,frame=single] connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr> -Create a connection. This is equivialent to adding the statement 'assign -<lhs-expr> = <rhs-expr>;' to the verilog input. Per default, all existing +Create a connection. This is equivalent to adding the statement 'assign +<lhs-expr> = <rhs-expr>;' to the Verilog input. Per default, all existing drivers for <lhs-expr> are unconnected. This can be overwritten by using the -nounset option. @@ -216,8 +271,8 @@ This command does not operate on module with processes. 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 outut are signed/unsigned bit extended. This command uses this -knowlege to rewire the inputs of the driven cells to match the output of +of the wrapper output are signed/unsigned bit extended. This command uses this +knowledge to rewire the inputs of the driven cells to match the output of the driving cell. -signed <cell_type> <port_name> <width_param> @@ -343,13 +398,13 @@ evaluated in the other design. design -copy-to <name> [-as <new_mod_name>] [selection] -Copy modules from the current design into the soecified one. +Copy modules from the current design into the specified one. \end{lstlisting} -\section{dff2dffe -- transform $dff cells to $dffe cells} +\section{dff2dffe -- transform \$dff cells to \$dffe cells} \label{cmd:dff2dffe} \begin{lstlisting}[numbers=left,frame=single] - dff2dffe [selection] + dff2dffe [options] [selection] This pass transforms $dff cells driven by a tree of multiplexers with one or more feedback paths to $dffe cells. It also works on gate-level cells such as @@ -365,8 +420,27 @@ $_DFF_P_, $_DFF_N_ and $_MUX_. <external_gate_type> is the cell type name for a cell with an identical interface to the <internal_gate_type>, except it also has an high-active enable port 'E'. - Usually <external_gate_type> is an intemediate cell type + Usually <external_gate_type> is an intermediate cell type that is then translated to the final type using 'techmap'. + + -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]_. +\end{lstlisting} + +\section{dffinit -- set INIT param on FF cells} +\label{cmd:dffinit} +\begin{lstlisting}[numbers=left,frame=single] + dffinit [options] [selection] + +This pass sets an FF cell parameter to the the initial value of the net it +drives. (This is primarily used in FPGA flows.) + + -ff <cell_name> <output_port> <init_param> + operate on the specified cell type. this option can be used + multiple times. \end{lstlisting} \section{dfflibmap -- technology mapping of flip-flops} @@ -385,6 +459,15 @@ to the internal cell types that best match the cells found in the given liberty file. \end{lstlisting} +\section{dffsr2dff -- convert DFFSR cells to simpler FF cell types} +\label{cmd:dffsr2dff} +\begin{lstlisting}[numbers=left,frame=single] + dffsr2dff [options] [selection] + +This pass converts DFFSR cells ($dffsr, $_DFFSR_???_) and ADFF cells ($adff, +$_DFF_???_) to simpler FF cell types when any of the set/reset inputs is unused. +\end{lstlisting} + \section{dump -- print parts of the design in ilang format} \label{cmd:dump} \begin{lstlisting}[numbers=left,frame=single] @@ -420,15 +503,29 @@ Print all commands to log before executing them. Do not print all commands to log before executing them. (default) \end{lstlisting} -\section{equiv\_add -- add a $equiv cell} +\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{equiv\_add -- add a \$equiv cell} \label{cmd:equiv_add} \begin{lstlisting}[numbers=left,frame=single] - equiv_add gold_sig gate_sig + 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} +\section{equiv\_induct -- proving \$equiv cells using temporal induction} \label{cmd:equiv_induct} \begin{lstlisting}[numbers=left,frame=single] equiv_induct [options] [selection] @@ -473,7 +570,7 @@ to work with the created equivalent checking module. Do not match cells or signals that match the names in the file. -encfile <file> - Match FSM encodings using the desiption from the file. + Match FSM encodings using the description from the file. See 'help fsm_recode' for details. Note: The circuit created by this command is not a miter (with something like @@ -481,6 +578,17 @@ 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] @@ -501,7 +609,17 @@ This creates a miter module for further analysis of the selected $equiv cells. Create compare logic that handles undefs correctly \end{lstlisting} -\section{equiv\_remove -- remove $equiv cells} +\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] @@ -516,7 +634,7 @@ used then only proven cells are removed. keep gate circuit \end{lstlisting} -\section{equiv\_simple -- try proving simple $equiv instances} +\section{equiv\_simple -- try proving simple \$equiv instances} \label{cmd:equiv_simple} \begin{lstlisting}[numbers=left,frame=single] equiv_simple [options] [selection] @@ -547,6 +665,36 @@ This command prints status information for all selected $equiv cells. produce an error if any unproven $equiv cell is found \end{lstlisting} +\section{equiv\_struct -- structural equivalence checking} +\label{cmd:equiv_struct} +\begin{lstlisting}[numbers=left,frame=single] + equiv_struct [options] [selection] + +This command adds additional $equiv cells based on the assumption that the +gold and gate circuit are structurally equivalent. Note that this can introduce +bad $equiv cells in cases where the netlists are not structurally equivalent, +for example when analyzing circuits with cells with commutative inputs. This +command will also de-duplicate gates. + + -fwd + by default this command performans forward sweeps until nothing can + be merged by forwards sweeps, then backward sweeps until forward + sweeps are effective again. with this option set only forward sweeps + are performed. + + -fwonly <cell_type> + add the specified cell type to the list of cell types that are only + merged in forward sweeps and never in backward sweeps. $equiv is in + this list automatically. + + -icells + by default, the internal RTL and gate cell types are ignored. add + this option to also process those cell types with this command. + + -maxiter <N> + maximum number of iterations to run before aborting +\end{lstlisting} + \section{eval -- evaluate the circuit given an input} \label{cmd:eval} \begin{lstlisting}[numbers=left,frame=single] @@ -585,8 +733,8 @@ outputs. signal path at that wire. -shared - only expose those signals that are shared ammong the selected modules. - this is useful for preparing modules for equivialence checking. + 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 @@ -609,7 +757,7 @@ outputs. 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 ilang file (*.il). +map file can be a Verilog source file (*.v) or an ilang file (*.il). -map <map_file> use the modules in this file as reference. This option can be used @@ -638,11 +786,11 @@ map file can be a verilog source file (*.v) or an ilang file (*.il). match. This option can be used multiple times. -swap <needle_type> <port1>,<port2>[,...] - Register a set of swapable ports for a needle cell type. + Register a set of swappable ports for a needle cell type. This option can be used multiple times. -perm <needle_type> <port1>,<port2>[,...] <portA>,<portB>[,...] - Register a valid permutation of swapable ports for a needle + Register a valid permutation of swappable ports for a needle cell type. This option can be used multiple times. -cell_attr <attribute_name> @@ -657,7 +805,7 @@ map file can be a verilog source file (*.v) or an ilang file (*.il). -ignore_param <cell_type> <parameter_name> Do not use this parameter when matching cells. -This pass does not operate on modules with uprocessed processes in it. +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 @@ -694,8 +842,11 @@ See 'help techmap' for a pass that does the opposite thing. flatten [selection] This pass flattens the design by replacing cells by their implementation. This -pass is very simmilar to the 'techmap' pass. The only difference is that 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. \end{lstlisting} \section{freduce -- perform functional reduction} @@ -704,7 +855,7 @@ pass is using the current design as mapping library. freduce [options] [selection] This pass performs functional reduction in the circuit. I.e. if two nodes are -equivialent, they are merged to one node and one of the redundant drivers is +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 @@ -722,7 +873,7 @@ disconnected. A subsequent call to 'clean' will remove the redundant drivers. 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 -equivialent nodes. +equivalent nodes. All selected wires are considered for rewiring. The selected cells cover the circuit that is analyzed. @@ -734,7 +885,7 @@ circuit that is analyzed. fsm [options] [selection] This pass calls all the other fsm_* passes in a useful order. This performs -FSM extraction and optimiziation. It also calls opt_clean as needed: +FSM extraction and optimization. It also calls opt_clean as needed: fsm_detect unless got option -nodetect fsm_extract @@ -759,7 +910,7 @@ Options: -expand, -norecode, -export, -nomap enable or disable passes as indicated above - -encoding tye + -encoding type -fm_set_fsm_file file -encfile file passed through to fsm_recode pass @@ -787,7 +938,7 @@ Signals can be protected from being detected by this pass by setting the 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 finate state machine. +the finite state machine. \end{lstlisting} \section{fsm\_export -- exporting FSMs to KISS2 files} @@ -881,9 +1032,13 @@ one-hot encoding and binary encoding is supported. \section{help -- display help messages} \label{cmd:help} \begin{lstlisting}[numbers=left,frame=single] - help ............. list all commands - help <command> ... print help message for given command - help -all ........ print complete command reference + help ................ list all commands + help <command> ...... print help message for given command + help -all ........... print complete command reference + + help -cells .......... list all cell types + help <celltype> ..... print help message for given cell type + help <celltype>+ .... print verilog code for given cell type \end{lstlisting} \section{hierarchy -- check, expand and clean up design hierarchy} @@ -903,7 +1058,7 @@ needed. -purge_lib by default the hierarchy command will not remove library (blackbox) - module. use this options to also remove unused blackbox modules. + modules. use this option to also remove unused blackbox modules. -libdir <directory> search for files named <module_name>.v in the specified directory @@ -927,6 +1082,9 @@ needed. specified top module. otherwise a module with the 'top' attribute set will implicitly be used as top module, if such a module exists. + -auto-top + automatically determine the top of the design hierarchy and mark it. + In -generate mode this pass generates blackbox modules for the given cell types (wildcards supported). For this the design is searched for cells that match the given types and then the given port declarations are used to @@ -936,7 +1094,7 @@ determine the direction of the ports. The syntax for a port declaration is: Input ports are specified with the 'i' prefix, output ports with the 'o' prefix and inout ports with the 'io' prefix. The optional <num> specifies -the position of the port in the parameter list (needed when instanciated +the position of the port in the parameter list (needed when instantiated using positional arguments). When <num> is not specified, the <portname> can also contain wildcard characters. @@ -973,6 +1131,39 @@ all commands executed in an interactive session, but not the commands from executed scripts. \end{lstlisting} +\section{ice40\_ffinit -- iCE40: handle FF init values} +\label{cmd:ice40_ffinit} +\begin{lstlisting}[numbers=left,frame=single] + ice40_ffinit [options] [selection] + +Remove zero init values for FF output signals. Add inverters to implement +nonzero init values. +\end{lstlisting} + +\section{ice40\_ffssr -- iCE40: merge synchronous set/reset into FF cells} +\label{cmd:ice40_ffssr} +\begin{lstlisting}[numbers=left,frame=single] + ice40_ffssr [options] [selection] + +Merge synchronous set/reset $_MUX_ cells into iCE40 FFs. +\end{lstlisting} + +\section{ice40\_opt -- iCE40: perform simple optimizations} +\label{cmd:ice40_opt} +\begin{lstlisting}[numbers=left,frame=single] + ice40_opt [options] [selection] + +This command executes the following script: + + do + <ice40 specific optimizations> + opt_const -mux_undef -undriven [-full] + opt_share + opt_rmdff + opt_clean + while <changed design> +\end{lstlisting} + \section{iopadmap -- technology mapping of i/o pads (or buffers)} \label{cmd:iopadmap} \begin{lstlisting}[numbers=left,frame=single] @@ -983,10 +1174,10 @@ can only map to very simple PAD cells. Use 'techmap' to further map the resulting cells to more sophisticated PAD cells. -inpad <celltype> <portname>[:<portname>] - Map module input ports to the given cell type with - the given port name. if a 2nd portname is given, the + Map module input ports to the given cell type with the + given output port name. if a 2nd portname is given, the signal is passed through the pad call, using the 2nd - portname as output. + portname as input. -outpad <celltype> <portname>[:<portname>] -inoutpad <celltype> <portname>[:<portname>] @@ -1004,6 +1195,22 @@ the resulting cells to more sophisticated PAD cells. buffers using -widthparam to set the word size on the cell.) \end{lstlisting} +\section{json -- write design in JSON format} +\label{cmd:json} +\begin{lstlisting}[numbers=left,frame=single] + json [options] [selection] + +Write a JSON netlist of all selected objects. + + -o <filename> + write to the specified file. + + -aig + also include AIG models for the different gate types + +See 'help write_json' for a description of the JSON format used. +\end{lstlisting} + \section{log -- print text and log files} \label{cmd:log} \begin{lstlisting}[numbers=left,frame=single] @@ -1038,23 +1245,31 @@ 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{lut2mux -- convert \$lut to \$\_MUX\_} +\label{cmd:lut2mux} +\begin{lstlisting}[numbers=left,frame=single] + lut2mux [options] [selection] + +This pass converts $lut cells to $_MUX_ gates. +\end{lstlisting} + \section{maccmap -- mapping macc cells} \label{cmd:maccmap} \begin{lstlisting}[numbers=left,frame=single] maccmap [-unmap] [selection] -This pass maps $macc cells to yosys gate primitives. When the -unmap option is -used then the $macc cell is mapped to $and, $sub, etc. cells instead. +This pass maps $macc cells to yosys $fa and $alu cells. When the -unmap option +is used then the $macc cell is mapped to $add, $sub, etc. cells instead. \end{lstlisting} \section{memory -- translate memories to basic cells} \label{cmd:memory} \begin{lstlisting}[numbers=left,frame=single] - memory [-nomap] [-bram <bram_rules>] [selection] + memory [-nomap] [-nordff] [-bram <bram_rules>] [selection] This pass calls all the other memory_* passes in a useful order: - memory_dff + memory_dff [-nordff] opt_clean memory_share opt_clean @@ -1079,13 +1294,14 @@ The rules file contains a set of block ram description and a sequence of match rules. A block ram description looks like this: bram RAMB1024X32 # name of BRAM cell + init 1 # set to '1' if BRAM can be initialized abits 10 # number of address bits dbits 32 # number of data bits groups 2 # number of port groups ports 1 1 # number of ports in each group wrmode 1 0 # set to '1' if this groups is write ports - enable 4 0 # number of enable bits (for write ports) - transp 0 2 # transparatent (for read ports) + enable 4 1 # number of enable bits + transp 0 2 # transparent (for read ports) clocks 1 2 # clock configuration clkpol 2 2 # clock polarity configuration endbram @@ -1103,7 +1319,7 @@ 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 configration 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 '@<label>' to the individual statements. @@ -1136,7 +1352,7 @@ It is possible to match against the following values with min/max rules: dcells ....... number of cells in 'data-direction' cells ........ total number of cells (acells*dcells*dups) -The interface for the created bram instances is dervived from the bram +The interface for the created bram instances is derived from the bram description. Use 'techmap' to convert the created bram instances into instances of the actual bram cells of your target architecture. @@ -1147,6 +1363,9 @@ the next also has 'or_next_if_better' set, and so forth). A match containing the command 'make_transp' will add external circuitry to simulate 'transparent read', if necessary. +A match containing the command 'make_outreg' will add external flip-flops +to implement synchronous read ports, if necessary. + A match containing the command 'shuffle_enable A' will re-organize the data bits to accommodate the enable pattern of port A. \end{lstlisting} @@ -1169,7 +1388,7 @@ This pass detects DFFs at memory ports and merges them into the memory port. I.e. it consumes an asynchronous memory port and the flip-flops at its interface and yields a synchronous memory port. - -wr_only + -nordfff do not merge registers on read ports \end{lstlisting} @@ -1221,7 +1440,7 @@ $memwr cells. It is the counterpart to the memory_collect pass. \begin{lstlisting}[numbers=left,frame=single] miter -equiv [options] gold_name gate_name miter_name -Creates a miter circuit for equivialence checking. The gold- and gate- modules +Creates a miter circuit for equivalence checking. The gold- and gate- modules must have the same interfaces. The miter circuit will have all inputs of the two source modules, prefixed with 'in_'. The miter circuit has a 'trigger' output that goes high if an output mismatch between the two source modules is @@ -1243,6 +1462,53 @@ detected. -flatten call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. + + + miter -assert [options] module [miter_name] + +Creates a miter circuit for property checking. All input ports are kept, +output ports are discarded. An additional output 'trigger' is created that +goes high when an assert is violated. Without a miter_name, the existing +module is modified. + + -make_outputs + keep module output ports. + + -flatten + call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. +\end{lstlisting} + +\section{muxcover -- cover trees of MUX cells with wider MUXes} +\label{cmd:muxcover} +\begin{lstlisting}[numbers=left,frame=single] + muxcover [options] [selection] + +Cover trees of $_MUX_ cells with $_MUX{4,8,16}_ cells + + -mux4, -mux8, -mux16 + Use the specified types of MUXes. If none of those options are used, + the effect is the same as if all of them where used. + + -nodecode + Do not insert decoder logic. This reduces the number of possible + substitutions, but guarantees that the resulting circuit is not + less efficient than the original circuit. +\end{lstlisting} + +\section{nlutmap -- map to LUTs of different sizes} +\label{cmd:nlutmap} +\begin{lstlisting}[numbers=left,frame=single] + nlutmap [options] [selection] + +This pass uses successive calls to 'abc' to map to an architecture. That +provides a small number of differently sized LUTs. + + -luts N_1,N_2,N_3,... + The number of LUTs with 1, 2, 3, ... inputs that are + available in the target architecture. + +Excess logic that does not fit into the specified LUTs is mapped back +to generic logic gates ($_AND_, etc.). \end{lstlisting} \section{opt -- perform simple optimizations} @@ -1254,23 +1520,23 @@ This pass calls all the other opt_* passes in a useful order. This performs a series of trivial optimizations and cleanups. This pass executes the other passes in the following order: - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] - opt_share -nomux + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_share [-share_all] -nomux do opt_muxtree opt_reduce [-fine] [-full] - opt_share + opt_share [-share_all] opt_rmdff opt_clean [-purge] - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] while <changed design> When called with -fast the following script is used instead: do - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] - opt_share + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_share [-share_all] opt_rmdff opt_clean [-purge] while <changed design in opt_rmdff> @@ -1311,6 +1577,9 @@ This pass performs const folding on internal cell types with constant inputs. -undriven replace undriven nets with undef (x) constants + -clkinv + optimize clock inverters by changing FF types + -fine perform fine-grain optimizations @@ -1368,13 +1637,16 @@ a constant driver. \section{opt\_share -- consolidate identical cells} \label{cmd:opt_share} \begin{lstlisting}[numbers=left,frame=single] - opt_share [-nomux] [selection] + opt_share [options] [selection] This pass identifies cells with identical type and input signals. Such cells are then merged to one cell. -nomux Do not merge MUX cells. + + -share_all + Operate on all cell types, not just built-in types. \end{lstlisting} \section{plugin -- load and list loaded plugins} @@ -1394,6 +1666,57 @@ Load and list loaded plugins. List loaded plugins \end{lstlisting} +\section{pmuxtree -- transform \$pmux cells to trees of \$mux cells} +\label{cmd:pmuxtree} +\begin{lstlisting}[numbers=left,frame=single] + pmuxtree [options] [selection] + +This pass transforms $pmux cells to a trees of $mux cells. +\end{lstlisting} + +\section{prep -- generic synthesis script} +\label{cmd:prep} +\begin{lstlisting}[numbers=left,frame=single] + prep [options] + +This command runs a conservative RTL synthesis. A typical application for this +is the preparation stage of a verification flow. This command does not operate +on partly selected designs. + + -top <module> + use the specified module as top module (default='top') + + -nordff + passed to 'memory_dff'. prohibits merging of FFs into memory read ports + + -run <from_label>[:<to_label>] + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + +The following commands are executed by this synthesis command: + + begin: + hierarchy -check [-top <top>] + + prep: + proc + opt_const + opt_clean + check + opt -keepdc + wreduce + memory_dff [-nordff] + opt_clean + memory_collect + opt -keepdc -fast + + check: + stat + check +\end{lstlisting} + \section{proc -- translate processes to netlists} \label{cmd:proc} \begin{lstlisting}[numbers=left,frame=single] @@ -1406,10 +1729,12 @@ This pass calls all the other proc_* passes in the most common order. proc_init proc_arst proc_mux + proc_dlatch proc_dff proc_clean -This replaces the processes in the design with multiplexers and flip-flops. +This replaces the processes in the design with multiplexers, +flip-flops and latches. The following options are supported: @@ -1452,12 +1777,21 @@ This pass identifies flip-flops in the processes and converts them to d-type flip-flop cells. \end{lstlisting} +\section{proc\_dlatch -- extract latches from processes} +\label{cmd:proc_dlatch} +\begin{lstlisting}[numbers=left,frame=single] + proc_dlatch [selection] + +This pass identifies latches in the processes and converts them to +d-type latches. +\end{lstlisting} + \section{proc\_init -- convert initial block to init attributes} \label{cmd:proc_init} \begin{lstlisting}[numbers=left,frame=single] proc_init [selection] -This pass extracts the 'init' actions from processes (generated from verilog +This pass extracts the 'init' actions from processes (generated from Verilog 'initial' blocks) and sets the initial value to the 'init' attribute on the respective wire. \end{lstlisting} @@ -1479,6 +1813,40 @@ and case statements) to trees of multiplexer cells. This pass identifies unreachable branches in decision trees and removes them. \end{lstlisting} +\section{qwp -- quadratic wirelength placer} +\label{cmd:qwp} +\begin{lstlisting}[numbers=left,frame=single] + qwp [options] [selection] + +This command runs quadratic wirelength placement on the selected modules and +annotates the cells in the design with 'qwp_position' attributes. + + -ltr + Add left-to-right constraints: constrain all inputs on the left border + outputs to the right border. + + -alpha + Add constraints for inputs/outputs to be placed in alphanumerical + order along the y-axis (top-to-bottom). + + -grid N + Number of grid divisions in x- and y-direction. (default=16) + + -dump <html_file_name> + Dump a protocol of the placement algorithm to the html file. + +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\_blif -- read BLIF file} +\label{cmd:read_blif} +\begin{lstlisting}[numbers=left,frame=single] + read_blif [filename] + +Load modules from a BLIF file into the current design. +\end{lstlisting} + \section{read\_ilang -- read modules from ilang file} \label{cmd:read_ilang} \begin{lstlisting}[numbers=left,frame=single] @@ -1513,18 +1881,22 @@ Read cells from liberty file as modules into current design. set the specified attribute (to the value 1) on all loaded modules \end{lstlisting} -\section{read\_verilog -- read modules from verilog file} +\section{read\_verilog -- read modules from Verilog file} \label{cmd:read_verilog} \begin{lstlisting}[numbers=left,frame=single] read_verilog [options] [filename] -Load modules from a verilog file to the current design. A large subset of +Load modules from a Verilog file to the current design. A large subset of Verilog-2005 is supported. -sv enable support for SystemVerilog features. (only a small subset of SystemVerilog is supported) + -formal + enable support for assert() and assume() from SystemVerilog + replace the implicit -D SYNTHESIS with -D FORMAL + -dump_ast1 dump abstract syntax tree (before simplification) @@ -1532,7 +1904,7 @@ Verilog-2005 is supported. dump abstract syntax tree (after simplification) -dump_vlog - dump ast as verilog code (after simplification) + dump ast as Verilog code (after simplification) -yydebug enable parser debug output @@ -1554,19 +1926,31 @@ Verilog-2005 is supported. this can also be achieved by setting the 'nomem2reg' attribute on the respective module or register. + This is potentially dangerous. Usually the front-end has good + reasons for converting an array to a list of registers. + Prohibiting this step will likely result in incorrect synthesis + results. + -mem2reg always convert memories to registers. this can also be achieved by setting the 'mem2reg' attribute on the respective module or register. + -nomeminit + do not infer $meminit cells and instead convert initialized + memories to registers directly in the front-end. + -ppdump - dump verilog code after pre-processor + dump Verilog code after pre-processor -nopp do not run the pre-processor + -nodpi + disable DPI-C support + -lib - only create empty blackbox modules + only create empty blackbox modules. This implies -DBLACKBOX. -noopt don't perform basic optimizations (such as const folding) in the @@ -1584,6 +1968,9 @@ Verilog-2005 is supported. to a later 'hierarchy' command. Useful in cases where the default parameters of modules yield invalid or not synthesizable code. + -noautowire + make the default of `default_nettype be "none" instead of "wire". + -setattr <attribute_name> set the specified attribute (to the value 1) on all loaded modules @@ -1600,7 +1987,7 @@ subsequent calls to 'read_verilog'. Note that the Verilog frontend does a pretty good job of processing valid verilog input, but has not very good error reporting. It generally is -recommended to use a simulator (for example icarus verilog) for checking +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. \end{lstlisting} @@ -1624,6 +2011,10 @@ pattern is '_%_'. Assign private names (the ones with $-prefix) to all selected wires and cells with public names. This ignores all selected ports. + + rename -top new_name + +Rename top module. \end{lstlisting} \section{sat -- solve a SAT problem in the circuit} @@ -1671,6 +2062,9 @@ and additional constraints passed as parameters. -show-inputs, -show-outputs, -show-ports add all module (input/output) ports to the list of shown signals + -show-regs, -show-public, -show-all + show all registers, show signals with 'public' names, show all signals + -ignore_div_by_zero ignore all solutions that involve a division by zero @@ -1683,11 +2077,17 @@ The following options can be used to set up a sequential problem: set up a sequential problem with <N> time steps. The steps will be numbered from 1 to N. + note: for large <N> it can be significantly faster to use + -tempinduct-baseonly -maxsteps <N> instead of -seq <N>. + -set-at <N> <signal> <value> -unset-at <N> <signal> set or unset the specified signal to the specified value in the given timestep. this has priority over a -set for the same signal. + -set-assumes + set all assumptions provided via $assume cells + -set-def-at <N> <signal> -set-any-undef-at <N> <signal> -set-all-undef-at <N> <signal> @@ -1708,6 +2108,9 @@ The following options can be used to set up a sequential problem: -dump_vcd <vcd-file-name> dump SAT model (counter example in proof) to VCD file + -dump_json <json-file-name> + dump SAT model (counter example in proof) to a WaveJSON file. + -dump_cnf <cnf-file-name> dump CNF of SAT problem (in DIMACS format). in temporal induction proofs this is the CNF of the first induction step. @@ -1716,7 +2119,7 @@ The following additional options can be used to set up a proof. If also -seq is passed, a temporal induction proof is performed. -tempinduct - Perform a temporal induction proof. In a temporalinduction proof it is + Perform a temporal induction proof. In a temporal induction proof it is proven that the condition holds forever after the number of time steps specified using -seq. @@ -1724,12 +2127,26 @@ is passed, a temporal induction proof is performed. Perform a temporal induction proof. Assume an initial state with all registers set to defined values for the induction step. + -tempinduct-baseonly + Run only the basecase half of temporal induction (requires -maxsteps) + + -tempinduct-inductonly + Run only the induction half of temporal induction + + -tempinduct-skip <N> + Skip the first <N> steps of the induction proof. + + note: this will assume that the base case holds for <N> steps. + this must be proven independently with "-tempinduct-baseonly + -maxsteps <N>". Use -initsteps if you just want to set a + minimal induction length. + -prove <signal> <value> Attempt to proof that <signal> is always <value>. -prove-x <signal> <value> Like -prove, but an undef (x) bit in the lhs matches any value on - the right hand side. Useful for equivialence checking. + the right hand side. Useful for equivalence checking. -prove-asserts Prove that all asserts in the design hold. @@ -1742,6 +2159,13 @@ is passed, a temporal induction proof is performed. -initsteps <N> Set initial length for the induction. + This will speed up the search of the right induction length + for deep induction proofs. + + -stepsize <N> + Increase the size of the induction proof in steps of <N>. + This will speed up the search of the right induction length + for deep induction proofs. -timeout <N> Maximum number of seconds a single SAT instance may take. @@ -1780,10 +2204,18 @@ Use the opt_clean command to get rid of the additional nets. This command identifies strongly connected components (aka logic loops) in the design. + -expect <num> + expect to find exactly <num> SSCs. A different number of SSCs will + produce an error. + -max_depth <num> - limit to loops not longer than the specified number of cells. This can - e.g. be useful in identifying local loops in a module that turns out - to be one gigantic SCC. + limit to loops not longer than the specified number of cells. This + can e.g. be useful in identifying small local loops in a module that + implements one large SCC. + + -nofeedback + do not count cells that have their output fed back into one of their + inputs as single-cell scc. -all_cell_types Usually this command only considers internal non-memory cells. With @@ -1978,7 +2410,7 @@ The following actions can be performed on the top sets on the stack: like %d but swap the roles of two top sets on the stack %c - create a copy of the top set rom the stack and push it + create a copy of the top set from the stack and push it %x[<num1>|*][.<num2>][:<rule>[:<rule>..]] expand top set <num1> num times according to the specified rules. @@ -1995,19 +2427,31 @@ The following actions can be performed on the top sets on the stack: %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]] %co[<num1>|*][.<num2>][:<rule>[:<rule>..]] - simmilar to %x, but only select input (%ci) or output cones (%co) + similar to %x, but only select input (%ci) or output cones (%co) + + %xe[...] %cie[...] %coe + like %x, %ci, and %co but only consider combinatorial cells %a expand top set by selecting all wires that are (at least in part) aliases for selected wires. %s - expand top set by adding all modules of instantiated cells in selected + expand top set by adding all modules that implement cells in selected modules %m expand top set by selecting all modules that contain selected objects + %M + select modules that implement selected cells + + %C + select cells that implement selected modules + + %R[<num>] + select <num> random objects from top selection (default 1) + Example: the following command selects all wires that are connected to a 'GATE' input of a 'SWITCH' cell: @@ -2080,7 +2524,7 @@ is used to determine if two resources are share-able. -fast Only consider the simple part of the control logic in SAT solving, resulting - in much easier SAT problems at the cost of maybe missing some oportunities + in much easier SAT problems at the cost of maybe missing some opportunities for resource sharing. -limit N @@ -2140,6 +2584,10 @@ to a graphics file (usually SVG or PostScript). inputs or outputs. This option can be used multiple times to specify more than one library. + note: in most cases it is better to load the library before calling + show with 'read_verilog -lib <filename>'. it is also possible to + load liberty files with 'read_liberty -lib <filename>'. + -prefix <prefix> generate <prefix>.* instead of ~/.yosys_show.* @@ -2156,7 +2604,7 @@ to a graphics file (usually SVG or PostScript). -colors <seed> Randomly assign colors to the wires. The integer argument is the seed for the random number generator. Change the seed value if the colored - graph still is ambigous. A seed of zero deactivates the coloring. + graph still is ambiguous. A seed of zero deactivates the coloring. -colorattr <attribute_name> Use the specified attribute to assign colors. A unique color is @@ -2166,7 +2614,7 @@ to a graphics file (usually SVG or PostScript). annotate busses with a label indicating the width of the bus. -signed - mark ports (A, B) that are declarted as signed (using the [AB]_SIGNED + mark ports (A, B) that are declared as signed (using the [AB]_SIGNED cell parameter) with an asterisk next to the port name. -stretch @@ -2180,7 +2628,7 @@ to a graphics file (usually SVG or PostScript). enumerate objects with internal ($-prefixed) names -long - do not abbeviate objects with internal ($-prefixed) names + do not abbreviate objects with internal ($-prefixed) names -notitle do not add the module name as graph title to the dot file @@ -2190,6 +2638,9 @@ specified, 'xdot' is used to display the schematic. The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>', unless another prefix is specified using -prefix <prefix>. + +Yosys on Windows and YosysJS use different defaults: The output is written +to 'show.dot' in the current directory and new viewer is launched. \end{lstlisting} \section{simplemap -- mapping simple coarse-grain cells} @@ -2202,10 +2653,26 @@ primitives. The following internal cell types are mapped by this pass: $not, $pos, $and, $or, $xor, $xnor $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool - $logic_not, $logic_and, $logic_or, $mux + $logic_not, $logic_and, $logic_or, $mux, $tribuf $sr, $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] @@ -2213,7 +2680,7 @@ primitives. The following internal cell types are mapped by this pass: This command adds $slice and $concat cells to the design to make the splicing of multi-bit signals explicit. This for example is useful for coarse grain -synthesis, where dedidacted hardware is needed to splice signals. +synthesis, where dedicated hardware is needed to splice signals. -sel_by_cell only select the cell ports to rewire by the cell. if the selection @@ -2228,6 +2695,9 @@ synthesis, where dedidacted hardware is needed to splice signals. it is sufficient if the driver of any bit of a cell port is selected. by default all bits must be selected. + -wires + also add $slice and $concat cells to drive otherwise unused wires. + -no_outputs do not rewire selected module outputs. @@ -2277,6 +2747,9 @@ design. selected and a module has the 'top' attribute set, this module is used default value for this option. + -liberty <liberty_file> + use cell area information from the provided liberty file + -width annotate internal cell types with their word width. e.g. $add_8 for an 8 bit wide $add cell. @@ -2285,7 +2758,7 @@ design. \section{submod -- moving part of a module to a new submodule} \label{cmd:submod} \begin{lstlisting}[numbers=left,frame=single] - submod [selection] + submod [-copy] [selection] This pass identifies all cells with the 'submod' attribute and moves them to a newly created module. The value of the attribute is used as name for the @@ -2298,11 +2771,15 @@ This pass only operates on completely selected modules with no processes or memories. - submod -name <name> [selection] + submod -name <name> [-copy] [selection] As above, but don't use the 'submod' attribute but instead use the selection. Only objects from one module might be selected. The value of the -name option is used as the value of the 'submod' attribute above. + +By default the cells are 'moved' from the source module and the source module +will use an instance of the new module after this command is finished. Call +with -copy to not modify the source module. \end{lstlisting} \section{synth -- generic synthesis script} @@ -2319,9 +2796,19 @@ on partly selected designs. -encfile <file> passed to 'fsm_recode' via 'fsm' + -nofsm + do not run FSM optimization + -noabc do not run abc (as if yosys was compiled without ABC support) + -noalumacc + do not run 'alumacc' pass. i.e. keep arithmetic operators in + their direct form ($add, $sub, etc.). + + -nordff + passed to 'memory'. prohibits merging of FFs into memory read ports + -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 @@ -2335,6 +2822,9 @@ The following commands are executed by this synthesis command: coarse: proc + opt_const + opt_clean + check opt wreduce alumacc @@ -2351,10 +2841,183 @@ The following commands are executed by this synthesis command: opt -full techmap opt -fast - - abc: abc -fast opt -fast + + check: + hierarchy -check + stat + check +\end{lstlisting} + +\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs} +\label{cmd:synth_greenpak4} +\begin{lstlisting}[numbers=left,frame=single] + synth_greenpak4 [options] + +This command runs synthesis for GreenPAK4 FPGAs. This work is experimental. + + -top <module> + use the specified module as top module (default='top') + + -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. + + -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 +/greenpak4/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + + coarse: + synth -run coarse + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap + dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib + opt -fast + abc -dff (only if -retime) + + map_luts: + nlutmap -luts 0,8,16,2 + clean + + map_cells: + techmap -map +/greenpak4/cells_map.v + clean + + check: + hierarchy -check + stat + check -noinit + + blif: + write_blif -gates -attr -param <file-name> + + edif: + write_edif <file-name> +\end{lstlisting} + +\section{synth\_ice40 -- synthesis for iCE40 FPGAs} +\label{cmd:synth_ice40} +\begin{lstlisting}[numbers=left,frame=single] + synth_ice40 [options] + +This command runs synthesis for iCE40 FPGAs. This work is experimental. + + -top <module> + use the specified module as top module (default='top') + + -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. + + -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 + + -nocarry + do not use SB_CARRY 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 + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/ice40/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + + coarse: + synth -run coarse + + bram: (skip if -nobram) + memory_bram -rules +/ice40/brams.txt + techmap -map +/ice40/brams_map.v + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap -map +/techmap.v [-map +/ice40/arith_map.v] + abc -dff (only if -retime) + ice40_opt + + map_ffs: + dffsr2dff + dff2dffe -direct-match $_DFF_* + techmap -map +/ice40/cells_map.v + opt_const -mux_undef + simplemap + ice40_ffinit + ice40_ffssr + ice40_opt -full + + map_luts: + abc (only if -abc2) + ice40_opt (only if -abc2) + abc -lut 4 + clean + + map_cells: + techmap -map +/ice40/cells_map.v + clean + + check: + hierarchy -check + stat + check -noinit + + blif: + write_blif -gates -attr -param <file-name> + + edif: + write_edif <file-name> \end{lstlisting} \section{synth\_xilinx -- synthesis for Xilinx FPGAs} @@ -2367,7 +3030,7 @@ partly selected designs. At the moment this command creates netlists that are compatible with 7-Series Xilinx devices. -top <module> - use the specified module as top module (default='top') + use the specified module as top module -edif <file> write the design to the specified edif file. writing of an output file @@ -2389,6 +3052,8 @@ The following commands are executed by this synthesis command: begin: read_verilog -lib +/xilinx/cells_sim.v + read_verilog -lib +/xilinx/brams_bb.v + read_verilog -lib +/xilinx/drams_bb.v hierarchy -check -top <top> flatten: (only if -flatten) @@ -2397,29 +3062,40 @@ The following commands are executed by this synthesis command: coarse: synth -run coarse - dff2dffe bram: memory_bram -rules +/xilinx/brams.txt techmap -map +/xilinx/brams_map.v + dram: + memory_bram -rules +/xilinx/drams.txt + techmap -map +/xilinx/drams_map.v + fine: opt -fast -full memory_map + dffsr2dff + dff2dffe opt -full techmap -map +/techmap.v -map +/xilinx/arith_map.v opt -fast map_luts: - abc -lut 5:8 [-dff] + abc -luts 2:2,3,6:5,10,20 [-dff] clean map_cells: techmap -map +/xilinx/cells_map.v + dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT clean - edif: - write_edif synth.edif + check: + hierarchy -check + stat + check -noinit + + edif: (only if -edif) + write_edif <file-name> \end{lstlisting} \section{tcl -- execute a TCL script file} @@ -2433,7 +3109,7 @@ 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 builting command 'proc'. +to avoid a name collision with the tcl builtin command 'proc'. \end{lstlisting} \section{techmap -- generic technology mapper} @@ -2442,7 +3118,7 @@ to avoid a name collision with the tcl builting command 'proc'. techmap [-map filename] [selection] This pass implements a very simple technology mapper that replaces cells in -the design with implementations given in form of a verilog or ilang source +the design with implementations given in form of a Verilog or ilang source file. -map filename @@ -2454,11 +3130,6 @@ file. -map %<design-name> like -map above, but with an in-memory design instead of a file. - -share_map filename - like -map, but look for the file in the share directory (where the - yosys data files are). this is mainly used internally when techmap - is called from other commands. - -extern load the cell implementations as separate modules into the design instead of inlining them. @@ -2468,7 +3139,7 @@ file. -recursive instead of the iterative breadth-first algorithm use a recursive - depth-first algorithm. both methods should yield equivialent results, + depth-first algorithm. both methods should yield equivalent results, but may differ in performance. -autoproc @@ -2480,8 +3151,8 @@ file. as final cell types by this mode. -D <define>, -I <incdir> - this options are passed as-is to the verilog frontend for loading the - map file. Note that the verilog frontend is also called with the + 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. When a module in the map file has the 'techmap_celltype' attribute set, it will @@ -2527,7 +3198,7 @@ wires are supported: of constant inputs and shorted inputs at this point and import the constant and connected bits into the map module. All further commands are executed in this copy. This is a very convenient way of creating - optimizied specializations of techmap modules without using the special + optimized specializations of techmap modules without using the special parameters described below. A _TECHMAP_DO_* command may start with the special token 'RECURSION; '. @@ -2563,12 +3234,12 @@ 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 beeing replaced. +of the cell that is being replaced. See 'help extract' for a pass that does the opposite thing. See 'help flatten' for a pass that does flatten the design (which is -esentially techmap but using the design itself as map library). +essentially techmap but using the design itself as map library). \end{lstlisting} \section{tee -- redirect command output to file} @@ -2608,7 +3279,7 @@ Test handling of logic loops in ABC. \begin{lstlisting}[numbers=left,frame=single] test_autotb [options] [filename] -Automatically create primitive verilog test benches for all modules in the +Automatically create primitive Verilog test benches for all modules in the design. The generated testbenches toggle the input pins of the module in a semi-random manner and dumps the resulting output signals. @@ -2624,7 +3295,7 @@ value after initialization. This can e.g. be used to force a reset signal low in order to explore more inner states in a state machine. -n <int> - number of iterations the test bench shuld run (default = 1000) + number of iterations the test bench should run (default = 1000) \end{lstlisting} \section{test\_cell -- automatically test the implementation of a cell type} @@ -2657,6 +3328,9 @@ cell types. Use for example 'all /$add' for all cell types except $add. -simlib use "techmap -map +/simlib.v -max_iter 2 -autoproc" + -aigmap + instead of calling "techmap", call "aigmap" + -muxdiv when creating test benches with dividers, create an additional mux to mask out the division-by-zero case @@ -2670,11 +3344,29 @@ cell types. Use for example 'all /$add' for all cell types except $add. -nosat do not check SAT model or run SAT equivalence checking + -noeval + do not check const-eval models + -v print additional debug information to the console -vlog {filename} - create a verilog test bench to test simlib and write_verilog + create a Verilog test bench to test simlib and write_verilog +\end{lstlisting} + +\section{torder -- print cells in topological order} +\label{cmd:torder} +\begin{lstlisting}[numbers=left,frame=single] + torder [options] [selection] + +This command prints the selected cells in topological order. + + -stop <cell_type> <cell_port> + do not use the specified cell port in topological sorting + + -noautostop + by default Q outputs of internal FF cells and memory read port outputs + are not used in topological sorting. this option deactivates that. \end{lstlisting} \section{trace -- redirect command output to file} @@ -2686,6 +3378,22 @@ Execute the specified command, logging all changes the command performs on the design in real time. \end{lstlisting} +\section{tribuf -- infer tri-state buffers} +\label{cmd:tribuf} +\begin{lstlisting}[numbers=left,frame=single] + tribuf [options] [selection] + +This pass transforms $mux cells with 'z' inputs to tristate buffers. + + -merge + merge multiple tri-state buffers driving the same net + into a single buffer. + + -logic + convert tri-state buffers that do not drive output ports + to non-tristate logic. this option implies -merge. +\end{lstlisting} + \section{verific -- load Verilog and VHDL designs using Verific} \label{cmd:verific} \begin{lstlisting}[numbers=left,frame=single] @@ -2701,7 +3409,7 @@ Load the specified VHDL files into Verific. verific -import [-gates] {-all | <top-module>..} -Elaborate the design for the sepcified top modules, import to Yosys and +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. @@ -2713,11 +3421,11 @@ Visit http://verific.com/ for more information on Verific. \begin{lstlisting}[numbers=left,frame=single] verilog_defaults -add [options] -Add the sepcified options to the list of default options to read_verilog. +Add the specified options to the list of default options to read_verilog. verilog_defaults -clear -Clear the list of verilog default options. +Clear the list of Verilog default options. verilog_defaults -push verilog_defaults -pop @@ -2761,7 +3469,7 @@ vhdl2verilog can be obtained from: http://www.edautils.com/vhdl2verilog.html \end{lstlisting} -\section{wreduce -- reduce the word size of operations is possible} +\section{wreduce -- reduce the word size of operations if possible} \label{cmd:wreduce} \begin{lstlisting}[numbers=left,frame=single] wreduce [options] [selection] @@ -2815,8 +3523,14 @@ file *.blif when any of this options is used. do not generate buffers for connected wires. instead use the non-standard .conn statement. + -attr + use the non-standard .attr statement to write cell attributes + -param - use the non-standard .param statement to write module parameters + use the non-standard .param statement to write cell parameters + + -cname + use the non-standard .cname statement to write cell names -blackbox write blackbox cells with .blackbox statement. @@ -2854,7 +3568,7 @@ is targeted. \begin{lstlisting}[numbers=left,frame=single] write_file [options] output_file [input_file] -Write the text fron the input file to the output file. +Write the text from the input file to the output file. -a Append to output file (instead of overwriting) @@ -2903,14 +3617,217 @@ a tool for Coarse-Grain Example-Driven Interconnect Synthesis. http://www.clifford.at/intersynth/ \end{lstlisting} +\section{write\_json -- write design to a JSON file} +\label{cmd:write_json} +\begin{lstlisting}[numbers=left,frame=single] + write_json [options] [filename] + +Write a JSON netlist of the current design. + + -aig + include AIG models for the different gate types + + +The general syntax of the JSON output created by this command is as follows: + + { + "modules": { + <module_name>: { + "ports": { + <port_name>: <port_details>, + ... + }, + "cells": { + <cell_name>: <cell_details>, + ... + }, + "netnames": { + <net_name>: <net_details>, + ... + } + } + }, + "models": { + ... + }, + } + +Where <port_details> is: + + { + "direction": <"input" | "output" | "inout">, + "bits": <bit_vector> + } + +And <cell_details> is: + + { + "hide_name": <1 | 0>, + "type": <cell_type>, + "parameters": { + <parameter_name>: <parameter_value>, + ... + }, + "attributes": { + <attribute_name>: <attribute_value>, + ... + }, + "port_directions": { + <port_name>: <"input" | "output" | "inout">, + ... + }, + "connections": { + <port_name>: <bit_vector>, + ... + }, + } + +And <net_details> is: + + { + "hide_name": <1 | 0>, + "bits": <bit_vector> + } + +The "hide_name" fields are set to 1 when the name of this cell or net is +automatically created and is likely not of interest for a regular user. + +The "port_directions" section is only included for cells for which the +interface is known. + +Module and cell ports and nets can be single bit wide or vectors of multiple +bits. Each individual signal bit is assigned a unique integer. The <bit_vector> +values referenced above are vectors of this integers. Signal bits that are +connected to a constant driver are denoted as string "0" or "1" instead of +a number. + +For example the following Verilog code: + + module test(input x, y); + (* keep *) foo #(.P(42), .Q(1337)) + foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}})); + endmodule + +Translates to the following JSON output: + + { + "modules": { + "test": { + "ports": { + "x": { + "direction": "input", + "bits": [ 2 ] + }, + "y": { + "direction": "input", + "bits": [ 3 ] + } + }, + "cells": { + "foo_inst": { + "hide_name": 0, + "type": "foo", + "parameters": { + "Q": 1337, + "P": 42 + }, + "attributes": { + "keep": 1, + "src": "test.v:2" + }, + "connections": { + "C": [ 2, 2, 2, 2, "0", "1", "0", "1" ], + "B": [ 2, 3 ], + "A": [ 3, 2 ] + } + } + }, + "netnames": { + "y": { + "hide_name": 0, + "bits": [ 3 ], + "attributes": { + "src": "test.v:1" + } + }, + "x": { + "hide_name": 0, + "bits": [ 2 ], + "attributes": { + "src": "test.v:1" + } + } + } + } + } + } + +The models are given as And-Inverter-Graphs (AIGs) in the following form: + + "models": { + <model_name>: [ + /* 0 */ [ <node-spec> ], + /* 1 */ [ <node-spec> ], + /* 2 */ [ <node-spec> ], + ... + ], + ... + }, + +The following node-types may be used: + + [ "port", <portname>, <bitindex>, <out-list> ] + - the value of the specified input port bit + + [ "nport", <portname>, <bitindex>, <out-list> ] + - the inverted value of the specified input port bit + + [ "and", <node-index>, <node-index>, <out-list> ] + - the ANDed value of the specified nodes + + [ "nand", <node-index>, <node-index>, <out-list> ] + - the inverted ANDed value of the specified nodes + + [ "true", <out-list> ] + - the constant value 1 + + [ "false", <out-list> ] + - the constant value 0 + +All nodes appear in topological order. I.e. only nodes with smaller indices +are referenced by "and" and "nand" nodes. + +The optional <out-list> at the end of a node specification is a list of +output portname and bitindex pairs, specifying the outputs driven by this node. + +For example, the following is the model for a 3-input 3-output $reduce_and cell +inferred by the following code: + + module test(input [2:0] in, output [2:0] out); + assign in = &out; + endmodule + + "$reduce_and:3U:3": [ + /* 0 */ [ "port", "A", 0 ], + /* 1 */ [ "port", "A", 1 ], + /* 2 */ [ "and", 0, 1 ], + /* 3 */ [ "port", "A", 2 ], + /* 4 */ [ "and", 2, 3, "Y", 0 ], + /* 5 */ [ "false", "Y", 1, "Y", 2 ] + ] + +Future version of Yosys might add support for additional fields in the JSON +format. A program processing this format must ignore all unknown fields. +\end{lstlisting} + \section{write\_smt2 -- write design to SMT-LIBv2 file} \label{cmd:write_smt2} \begin{lstlisting}[numbers=left,frame=single] write_smt2 [options] [filename] Write a SMT-LIBv2 [1] description of the current design. For a module with name -'<mod>' this will declare the sort '<mod>_s' (state of the module) and the the -function '<mod>_t' (state transition function). +'<mod>' this will declare the sort '<mod>_s' (state of the module) and the +functions operating on that state. 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. @@ -2922,11 +3839,37 @@ multi-bit wires are exported as single functions of type BitVec. The '<mod>_t' function evaluates to 'true' when the given pair of states describes a valid state transition. +The '<mod>_a' function evaluates to 'true' when the given state satisfies +the asserts in the module. + +The '<mod>_u' function evaluates to 'true' when the given state satisfies +the assumptions in the module. + +The '<mod>_i' function evaluates to 'true' when the given state conforms +to the initial state. + + -verbose + this will print the recursive walk used to export the modules. + -bv enable support for BitVec (FixedSizeBitVectors theory). with this option set multi-bit wires are represented using the BitVec sort and support for coarse grain cells (incl. arithmetic) is enabled. + -mem + enable support for memories (via ArraysEx theory). this option + also implies -bv. only $mem cells without merged registers in + read ports are supported. call "memory" with -nordff to make sure + that no registers are merged into $mem read ports. '<mod>_m' functions + will be generated for accessing the arrays that are used to represent + memories. + + -regs + also create '<mod>_n' functions for all registers. + + -wires + also create '<mod>_n' functions for all public wires. + -tpl <template_file> use the given template file. the line containing only the token '%%' is replaced with the regular output of this command. @@ -2973,13 +3916,30 @@ For this proof we create the following template (test.tpl). The following yosys script will create a 'test.smt2' file for our proof: read_verilog test.v - hierarchy; proc; techmap; opt -fast + hierarchy -check; proc; opt; check -assert write_smt2 -bv -tpl test.tpl test.smt2 Running 'cvc4 test.smt2' will print 'unsat' because y can never transition from non-zero to zero in the test design. \end{lstlisting} +\section{write\_smv -- write design to SMV file} +\label{cmd:write_smv} +\begin{lstlisting}[numbers=left,frame=single] + write_smv [options] [filename] + +Write an SMV description of the current design. + + -verbose + this will print the recursive walk used to export the modules. + + -tpl <template_file> + use the given template file. the line containing only the token '%%' + is replaced with the regular output of this command. + +THIS COMMAND IS UNDER CONSTRUCTION +\end{lstlisting} + \section{write\_spice -- write design to SPICE netlist file} \label{cmd:write_spice} \begin{lstlisting}[numbers=left,frame=single] @@ -2988,7 +3948,7 @@ from non-zero to zero in the test design. Write the current design to an SPICE netlist file. -big_endian - generate multi-bit ports in MSB first order + generate multi-bit ports in MSB first order (default is LSB first) -neg net_name @@ -3004,12 +3964,12 @@ Write the current design to an SPICE netlist file. set the specified module as design top module \end{lstlisting} -\section{write\_verilog -- write design to verilog file} +\section{write\_verilog -- write design to Verilog file} \label{cmd:write_verilog} \begin{lstlisting}[numbers=left,frame=single] write_verilog [options] [filename] -Write the current design to a verilog file. +Write the current design to a Verilog file. -norename without this option all internal object names (the ones with a dollar @@ -3023,7 +3983,7 @@ Write the current design to a verilog file. with this option attributes are included as comments in the output -noexpr - without this option all internal cells are converted to verilog + without this option all internal cells are converted to Verilog expressions. -blackboxes |