diff options
| -rw-r--r-- | CodingReadme | 2 | ||||
| -rw-r--r-- | manual/CHAPTER_Appnotes.tex | 4 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 374 |
3 files changed, 364 insertions, 16 deletions
diff --git a/CodingReadme b/CodingReadme index 5d5d9b32c..ba184be58 100644 --- a/CodingReadme +++ b/CodingReadme @@ -94,7 +94,7 @@ creates a bijective map from K to the integers. For example: It is not possible to remove elements from an idict. Finally mfp<K> implements a merge-find set data structure (aka. disjoint-set or -union–find) over the type K ("mfp" = merge-find-promote). +union-find) over the type K ("mfp" = merge-find-promote). 2. Standard STL data types diff --git a/manual/CHAPTER_Appnotes.tex b/manual/CHAPTER_Appnotes.tex index cbb01ed1b..e0d093290 100644 --- a/manual/CHAPTER_Appnotes.tex +++ b/manual/CHAPTER_Appnotes.tex @@ -15,6 +15,7 @@ This appendix contains copies of the Yosys application notes. \begin{itemize} \item Yosys AppNote 010: Converting Verilog to BLIF \dotfill Page \pageref{app:010} \hskip2cm\null \item Yosys AppNote 011: Interactive Design Investigation \dotfill Page \pageref{app:011} \hskip2cm\null +\item Yosys AppNote 012: Converting Verilog to BTOR \dotfill Page \pageref{app:012} \hskip2cm\null \end{itemize} \eject\label{app:010} @@ -23,3 +24,6 @@ This appendix contains copies of the Yosys application notes. \eject\label{app:011} \includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_011_Design_Investigation.pdf} +\eject\label{app:012} +\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_012_Verilog_to_BTOR.pdf} + diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index dfef1bb05..99d4a1fa0 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -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 @@ -450,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] @@ -485,12 +503,26 @@ Print all commands to log before executing them. Do not print all commands to log before executing them. (default) \end{lstlisting} +\section{edgetypes -- list all types of edges in selection} +\label{cmd:edgetypes} +\begin{lstlisting}[numbers=left,frame=single] + edgetypes [options] [selection] + +This command lists all unique types of 'edges' found in the selection. An 'edge' +is a 4-tuple of source and sink cell type and port name. +\end{lstlisting} + \section{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} @@ -546,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] @@ -566,6 +609,16 @@ This creates a miter module for further analysis of the selected $equiv cells. Create compare logic that handles undefs correctly \end{lstlisting} +\section{equiv\_purge -- purge equivalence checking module} +\label{cmd:equiv_purge} +\begin{lstlisting}[numbers=left,frame=single] + equiv_purge [options] [selection] + +This command removes the proven part of an equivalence checking module, leaving +only the unproven segments in the design. This will also remove and add module +ports as needed. +\end{lstlisting} + \section{equiv\_remove -- remove \$equiv cells} \label{cmd:equiv_remove} \begin{lstlisting}[numbers=left,frame=single] @@ -612,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] @@ -949,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} @@ -1044,6 +1131,15 @@ 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] @@ -1078,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>] @@ -1149,6 +1245,14 @@ 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] @@ -1196,7 +1300,7 @@ rules. A block ram description looks like this: 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) + 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 @@ -1391,6 +1495,22 @@ Cover trees of $_MUX_ cells with $_MUX{4,8,16}_ cells 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} \label{cmd:opt} \begin{lstlisting}[numbers=left,frame=single] @@ -1554,6 +1674,49 @@ Load and list loaded plugins. 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] @@ -1650,6 +1813,32 @@ 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] @@ -1705,8 +1894,8 @@ Verilog-2005 is supported. of SystemVerilog is supported) -formal - enable support for assert() and assume() statements - (assert support is also enabled with -sv) + enable support for assert() and assume() from SystemVerilog + replace the implicit -D SYNTHESIS with -D FORMAL -dump_ast1 dump abstract syntax tree (before simplification) @@ -1757,6 +1946,9 @@ Verilog-2005 is supported. -nopp do not run the pre-processor + -nodpi + disable DPI-C support + -lib only create empty blackbox modules. This implies -DBLACKBOX. @@ -1870,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 @@ -2254,6 +2449,9 @@ The following actions can be performed on the top sets on the stack: %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: @@ -2455,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] @@ -2533,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. @@ -2541,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 @@ -2554,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} @@ -2601,6 +2822,7 @@ The following commands are executed by this synthesis command: coarse: proc + opt_const opt_clean check opt @@ -2628,6 +2850,79 @@ The following commands are executed by this synthesis command: 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] @@ -2663,6 +2958,9 @@ This command runs synthesis for iCE40 FPGAs. This work is experimental. -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: @@ -2673,6 +2971,7 @@ The following commands are executed by this synthesis command: flatten: (unless -noflatten) proc flatten + tribuf -logic coarse: synth -run coarse @@ -2690,14 +2989,18 @@ The following commands are executed by this synthesis command: 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 @@ -2759,7 +3062,6 @@ The following commands are executed by this synthesis command: coarse: synth -run coarse - dff2dffe bram: memory_bram -rules +/xilinx/brams.txt @@ -2772,12 +3074,14 @@ The following commands are executed by this synthesis command: 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: @@ -3040,6 +3344,9 @@ 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 @@ -3047,6 +3354,21 @@ cell types. Use for example 'all /$add' for all cell types except $add. 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} \label{cmd:trace} \begin{lstlisting}[numbers=left,frame=single] @@ -3056,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] @@ -3191,6 +3529,9 @@ file *.blif when any of this options is used. -param 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. @@ -3526,6 +3867,9 @@ to the initial state. -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. |