From: Clifford Wolf Date: Mon, 9 Feb 2015 11:05:02 +0000 (+0100) Subject: Updated command reference in manual X-Git-Tag: yosys-0.5~2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b944fef925850ff53e6c02c3451d998790d56301;p=yosys.git Updated command reference in manual --- diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 697add159..047ec4214 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -23,36 +23,33 @@ library to a target architecture. if no -script parameter is given, the following scripts are used: for -liberty without -constr: - strash; scorr -v; ifraig -v; retime -v {D}; strash; dch -vf; - map -v {D} + strash; scorr; ifraig; retime {D}; strash; dch -f; map {D} for -liberty with -constr: - strash; scorr -v; ifraig -v; retime -v {D}; strash; dch -vf; - map -v {D}; buffer -v; upsize -v {D}; dnsize -v {D}; - stime -p + strash; scorr; ifraig; retime {D}; strash; dch -f; map {D}; + buffer; upsize {D}; dnsize {D}; stime -p for -lut: - strash; scorr -v; ifraig -v; retime -v; strash; dch -vf; if -v + strash; scorr; ifraig; retime; strash; dch -f; if otherwise: - strash; scorr -v; ifraig -v; retime -v; strash; dch -vf; map -v + strash; scorr; ifraig; retime; strash; dch -f; map -fast use different default scripts that are slightly faster (at the cost of output quality): for -liberty without -constr: - retime -v {D}; map -v {D} + retime {D}; map {D} for -liberty with -constr: - retime -v {D}; map -v {D}; buffer -v; upsize -v {D}; - dnsize -v {D}; stime -p + retime {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p for -lut: - retime -v; if -v + retime; if otherwise: - retime -v; map -v + retime; map -liberty generate netlists for the specified cell library (using the liberty @@ -76,15 +73,20 @@ library to a target architecture. -lut generate netlist using luts of (max) the specified width. + -lut : + generate netlist using luts of (max) the specified width . All + luts with width <= have constant cost. for luts larger than + the area cost doubles with each additional input bit. the delay cost + is still constant for all lut widths. + -dff - also pass $_DFF_?_ cells through ABC (only one clock domain, if many - clock domains are present in a module, the one with the largest number - of $_DFF_?_ cells in it is used) + also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many + clock domains are automatically partitioned in clock domains and each + domain is passed through ABC independently. - -clk [!] - use the specified clock domain. (when this option is used in combination - with -dff, then it falls back to the automatic dection of clock domain - if the specified clock is not found in a module.) + -clk [!][,[!]] + use only the specified clock domain. this is like -dff, but only FF + cells that belong to the specified clock domain are used. -keepff set the "keep" attribute on flip-flop output wires. (and thus preserve @@ -94,6 +96,15 @@ library to a target architecture. when this option is used, the temporary files created by this pass are not removed. this is useful for debugging. + -showtmp + print the temp dir name in log. usually this is suppressed so that the + command output is identical across runs. + + -markgroups + set a 'abcgroup' attribute on all objects created by ABC. The value of + this attribute is a unique integer for each ABC process started. This + is useful for debugging the partitioning of clock domains. + When neither -liberty nor -lut is used, the Yosys standard cell library is loaded into ABC before the ABC script is executed. @@ -130,8 +141,8 @@ selected modules. \begin{lstlisting}[numbers=left,frame=single] alumacc [selection] -This pass translates arithmetic operations $add, $mul, $lt, etc. to $alu and -$macc cells. +This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu +and $macc cells. \end{lstlisting} \section{cd -- a shortcut for 'select -module '} @@ -272,7 +283,7 @@ Hint: Use the following AWK command to consolidate Yosys coverage files: printf "%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3 -Coverage counters are only available in debug builds of Yosys for Linux. +Coverage counters are only available in Yosys for Linux. \end{lstlisting} \section{delete -- delete objects in the design} @@ -335,16 +346,43 @@ evaluated in the other design. Copy modules from the current design into the soecified one. \end{lstlisting} +\section{dff2dffe -- transform $dff cells to $dffe cells} +\label{cmd:dff2dffe} +\begin{lstlisting}[numbers=left,frame=single] + dff2dffe [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 +$_DFF_P_, $_DFF_N_ and $_MUX_. + + -unmap + operate in the opposite direction: replace $dffe cells with combinations + of $dff and $mux cells. the options below are ignore in unmap mode. + + -direct + map directly to external gate type. can + be any internal gate-level FF cell (except $_DFFE_??_). the + is the cell type name for a cell with an + identical interface to the , except it + also has an high-active enable port 'E'. + Usually is an intemediate cell type + that is then translated to the final type using 'techmap'. +\end{lstlisting} + \section{dfflibmap -- technology mapping of flip-flops} \label{cmd:dfflibmap} \begin{lstlisting}[numbers=left,frame=single] - dfflibmap -liberty [selection] + dfflibmap [-prepare] -liberty [selection] Map internal flip-flop cells to the flip-flop cells in the technology library specified in the given liberty file. This pass may add inverters as needed. Therefore it is recommended to first run this pass and then map the logic paths to the target technology. + +When called with -prepare, this command will convert the internal FF cells +to the internal cell types that best match the cells found in the given +liberty file. \end{lstlisting} \section{dump -- print parts of the design in ilang format} @@ -362,10 +400,10 @@ ilang format. -n only dump the module headers if the entire module is selected - -outfile + -o write to the specified file. - -append + -a like -outfile but append instead of overwrite \end{lstlisting} @@ -382,6 +420,133 @@ 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} +\label{cmd:equiv_add} +\begin{lstlisting}[numbers=left,frame=single] + equiv_add gold_sig gate_sig + +This command adds an $equiv cell for the specified signals. +\end{lstlisting} + +\section{equiv\_induct -- proving $equiv cells using temporal induction} +\label{cmd:equiv_induct} +\begin{lstlisting}[numbers=left,frame=single] + equiv_induct [options] [selection] + +Uses a version of temporal induction to prove $equiv cells. + +Only selected $equiv cells are proven and only selected cells are used to +perform the proof. + + -undef + enable modelling of undef states + + -seq + the max. number of time steps to be considered (default = 4) + +This command is very effective in proving complex sequential circuits, when +the internal state of the circuit quickly propagates to $equiv cells. + +However, this command uses a weak definition of 'equivalence': This command +proves that the two circuits will not diverge after they produce equal +outputs (observable points via $equiv) for at least cycles (the +specified via -seq). + +Combined with simulation this is very powerful because simulation can give +you confidence that the circuits start out synced for at least cycles +after reset. +\end{lstlisting} + +\section{equiv\_make -- prepare a circuit for equivalence checking} +\label{cmd:equiv_make} +\begin{lstlisting}[numbers=left,frame=single] + equiv_make [options] gold_module gate_module equiv_module + +This creates a module annotated with $equiv cells from two presumably +equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status' +to work with the created equivalent checking module. + + -inames + Also match cells and wires with $... names. + + -blacklist + Do not match cells or signals that match the names in the file. + + -encfile + Match FSM encodings using the desiption from the file. + See 'help fsm_recode' for details. + +Note: The circuit created by this command is not a miter (with something like +a trigger output), but instead uses $equiv cells to encode the equivalence +checking problem. Use 'miter -equiv' if you want to create a miter circuit. +\end{lstlisting} + +\section{equiv\_miter -- extract miter from equiv circuit} +\label{cmd:equiv_miter} +\begin{lstlisting}[numbers=left,frame=single] + equiv_miter [options] miter_module [selection] + +This creates a miter module for further analysis of the selected $equiv cells. + + -trigger + Create a trigger output + + -cmp + Create cmp_* outputs for individual unproven $equiv cells + + -assert + Create a $assert cell for each unproven $equiv cell + + -undef + Create compare logic that handles undefs correctly +\end{lstlisting} + +\section{equiv\_remove -- remove $equiv cells} +\label{cmd:equiv_remove} +\begin{lstlisting}[numbers=left,frame=single] + equiv_remove [options] [selection] + +This command removes the selected $equiv cells. If neither -gold nor -gate is +used then only proven cells are removed. + + -gold + keep gold circuit + + -gate + keep gate circuit +\end{lstlisting} + +\section{equiv\_simple -- try proving simple $equiv instances} +\label{cmd:equiv_simple} +\begin{lstlisting}[numbers=left,frame=single] + equiv_simple [options] [selection] + +This command tries to prove $equiv cells using a simple direct SAT approach. + + -v + verbose output + + -undef + enable modelling of undef states + + -nogroup + disabling grouping of $equiv cells by output wire + + -seq + the max. number of time steps to be considered (default = 1) +\end{lstlisting} + +\section{equiv\_status -- print status of equivalent checking module} +\label{cmd:equiv_status} +\begin{lstlisting}[numbers=left,frame=single] + equiv_status [options] [selection] + +This command prints status information for all selected $equiv cells. + + -assert + produce an error if any unproven $equiv cell is found +\end{lstlisting} + \section{eval -- evaluate the circuit given an input} \label{cmd:eval} \begin{lstlisting}[numbers=left,frame=single] @@ -596,6 +761,7 @@ Options: -encoding tye -fm_set_fsm_file file + -encfile file passed through to fsm_recode pass \end{lstlisting} @@ -692,16 +858,24 @@ combination with the 'opt_clean' pass (see also 'help fsm'). \section{fsm\_recode -- recoding finite state machines} \label{cmd:fsm_recode} \begin{lstlisting}[numbers=left,frame=single] - fsm_recode [-encoding type] [-fm_set_fsm_file file] [selection] + fsm_recode [options] [selection] This pass reassign the state encodings for FSM cells. At the moment only -one-hot encoding and binary encoding is supported. The option -encoding -can be used to specify the encoding scheme used for FSMs without the -`fsm_encoding' attribute (or with the attribute set to `auto'. +one-hot encoding and binary encoding is supported. + -encoding + specify the encoding scheme used for FSMs without the + 'fsm_encoding' attribute or with the attribute set to `auto'. + + -fm_set_fsm_file + generate a file containing the mapping from old to new FSM encoding + in form of Synopsys Formality set_fsm_* commands. -The option -fm_set_fsm_file can be used to generate a file containing the -mapping from old to new FSM encoding in form of Synopsys Formality set_fsm_* -commands. + -encfile + write the mappings from old to new FSM encoding to a file in the + following format: + + .fsm + .map \end{lstlisting} \section{help -- display help messages} @@ -826,8 +1000,8 @@ the resulting cells to more sophisticated PAD cells. -bits create individual bit-wide buffers even for ports that - are wider. (the default behavio is to create word-wide - buffers use -widthparam to set the word size on the cell.) + are wider. (the default behavior is to create word-wide + buffers using -widthparam to set the word size on the cell.) \end{lstlisting} \section{log -- print text and log files} @@ -857,17 +1031,11 @@ logfiles. \section{ls -- list modules or objects in modules} \label{cmd:ls} \begin{lstlisting}[numbers=left,frame=single] - ls [pattern] + ls [selection] -When no active module is selected, this prints a list of all modules. +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. - -If a pattern is given, the objects matching the pattern are printed - -Note that this command does not use the selection mechanism and always operates -on the whole design or whole active module. Use 'select -list' to show a list -of currently selected objects. \end{lstlisting} \section{maccmap -- mapping macc cells} @@ -882,7 +1050,7 @@ used then the $macc cell is mapped to $and, $sub, etc. cells instead. \section{memory -- translate memories to basic cells} \label{cmd:memory} \begin{lstlisting}[numbers=left,frame=single] - memory [-nomap] [selection] + memory [-nomap] [-bram ] [selection] This pass calls all the other memory_* passes in a useful order: @@ -891,12 +1059,98 @@ This pass calls all the other memory_* passes in a useful order: memory_share opt_clean memory_collect - memory_map (skipped if called with -nomap) + memory_bram -rules (when called with -bram) + memory_map (skipped if called with -nomap) This converts memories to word-wide DFFs and address decoders or multiport memory blocks if called with the -nomap option. \end{lstlisting} +\section{memory\_bram -- map memories to block rams} +\label{cmd:memory_bram} +\begin{lstlisting}[numbers=left,frame=single] + memory_bram -rules [selection] + +This pass converts the multi-port $mem memory cells into block ram instances. +The given rules file describes the available resources and how they should be +used. + +The rules file contains 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 + 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) + clocks 1 2 # clock configuration + clkpol 2 2 # clock polarity configuration + endbram + +For the option 'transp' the value 0 means non-transparent, 1 means transparent +and a value greater than 1 means configurable. All groups with the same +value greater than 1 share the same configuration bit. + +For the option 'clocks' the value 0 means non-clocked, and a value greater +than 0 means clocked. All groups with the same value share the same clock +signal. + +For the option 'clkpol' the value 0 means negative edge, 1 means positive edge +and a value greater than 1 means configurable. All groups with the same value +greater than 1 share the same configuration bit. + +Using the same bram name in different bram blocks will create different variants +of the bram. Verilog configration parameters for the bram are created as needed. + +It is also possible to create variants by repeating statements in the bram block +and appending '@