sv: More tests for wildcard port connections
[yosys.git] / manual / command-reference-manual.tex
index 1c91cb66e7845480e53aeb3b4626424579b667cc..bed6326e2446a94fabaa79f967e709dce66aa3d9 100644 (file)
@@ -9,30 +9,162 @@ This pass uses the ABC tool [1] for technology mapping of yosys's internal gate
 library to a target architecture.
 
     -exe <command>
-        use the specified command name instead of "yosys-abc" to execute ABC.
+        use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC.
         This can e.g. be used to call a specific version of ABC or a wrapper.
 
     -script <file>
         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 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.
+
+        if no -script parameter is given, the following scripts are used:
+
+        for -liberty without -constr:
+          strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+               &nf {D}; &put
+
+        for -liberty with -constr:
+          strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+               &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p
+
+        for -lut/-luts (only one LUT size):
+          strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2;
+               lutpack {S}
+
+        for -lut/-luts (different LUT sizes):
+          strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2
+
+        for -sop:
+          strash; ifraig; scorr; dc2; dretime; strash; dch -f;
+               cover {I} {P}
+
+        otherwise:
+          strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+               &nf {D}; &put
+
+    -fast
+        use different default scripts that are slightly faster (at the cost
+        of output quality):
+
+        for -liberty without -constr:
+          strash; dretime; map {D}
+
+        for -liberty with -constr:
+          strash; dretime; map {D}; buffer; upsize {D}; dnsize {D};
+               stime -p
+
+        for -lut/-luts:
+          strash; dretime; if
+
+        for -sop:
+          strash; dretime; cover -I {I} -P {P}
+
+        otherwise:
+          strash; dretime; map
+
     -liberty <file>
         generate netlists for the specified cell library (using the liberty
-        file format). Without this option, ABC is used to optimize the netlist
-        but keeps using yosys's internal gate library. This option is ignored if
-        the -script option is also used.
+        file format).
 
     -constr <file>
-        pass this file with timing constraints to ABC
+        pass this file with timing constraints to ABC. use with -liberty.
+
+        a constr file contains two lines:
+            set_driving_cell <cell_name>
+            set_load <floating_point_number>
+
+        the set_driving_cell statement defines which cell type is assumed to
+        drive the primary inputs and the set_load statement sets the load in
+        femtofarads for each primary output.
+
+    -D <picoseconds>
+        set delay target. the string {D} in the default scripts above is
+        replaced by this option when used, and an empty string otherwise.
+        this also replaces 'dretime' with 'dretime; retime -o {D}' in the
+        default scripts above.
+
+    -I <num>
+        maximum number of SOP inputs.
+        (replaces {I} in the default scripts above)
+
+    -P <num>
+        maximum number of SOP products.
+        (replaces {P} in the default scripts above)
+
+    -S <num>
+        maximum number of LUT inputs shared.
+        (replaces {S} in the default scripts above, default: -S 1)
 
     -lut <width>
         generate netlist using luts of (max) the specified width.
 
+    -lut <w1>:<w2>
+        generate netlist using luts of (max) the specified width <w2>. All
+        luts with width <= <w1> have constant cost. for luts larger than <w1>
+        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.
+
+    -sop
+        map to sum-of-product cells and inverters
+
+    -g type1,type2,...
+        Map to the specified list of gate types. Supported gates types are:
+        AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX, AOI3, OAI3, AOI4, OAI4.
+        (The NOT gate is always added to this list automatically.)
+
+        The following aliases can be used to reference common sets of gate types:
+          simple: AND OR XOR MUX
+          cmos2: NAND NOR
+          cmos3: NAND NOR AOI3 OAI3
+          cmos4: NAND NOR AOI3 OAI3 AOI4 OAI4
+          gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT
+          aig: AND NAND OR NOR ANDNOT ORNOT
+
+        Prefix a gate type with a '-' to remove it from the list. For example
+        the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent.
+
+    -dff
+        also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many
+        clock domains are automatically partitioned in clock domains and each
+        domain is passed through ABC independently.
+
+    -clk [!]<clock-signal-name>[,[!]<enable-signal-name>]
+        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
+        them, for example for equivalence checking.)
+
     -nocleanup
         when this option is used, the temporary files created by this pass
         are not removed. this is useful for debugging.
 
-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.)
+    -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.
+
+Note that this is a logic optimization pass within Yosys that is calling ABC
+internally. This is not going to "run ABC on your design". It will instead run
+ABC on logic snippets extracted from your design. You will not get any useful
+output when passing an ABC script that writes a file. Instead write your full
+design as BLIF file with write_blif and the load that into ABC externally if
+you want to use ABC to convert your design into another format.
 
 [1] http://www.eecs.berkeley.edu/~alanmi/abc/
 \end{lstlisting}
@@ -59,6 +191,131 @@ 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]
+    alumacc [selection]
+
+This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu
+and $macc cells.
+\end{lstlisting}
+
+\section{assertpmux -- convert internal signals to module ports}
+\label{cmd:assertpmux}
+\begin{lstlisting}[numbers=left,frame=single]
+    assertpmux [options] [selection]
+
+This command adds asserts to the design that assert that all parallel muxes
+($pmux cells) have a maximum of one of their inputs enable at any time.
+
+    -noinit
+        do not enforce the pmux condition during the init state
+
+    -always
+        usually the $pmux condition is only checked when the $pmux output
+        is used be the mux tree it drives. this option will deactivate this
+        additional constrained and check the $pmux condition always.
+\end{lstlisting}
+
+\section{async2sync -- convert async FF inputs to sync circuits}
+\label{cmd:async2sync}
+\begin{lstlisting}[numbers=left,frame=single]
+    async2sync [options] [selection]
+
+This command replaces async FF inputs with sync circuits emulating the same
+behavior for when the async signals are actually synchronized to the clock.
+
+This pass assumes negative hold time for the async FF inputs. For example when
+a reset deasserts with the clock edge, then the FF output will still drive the
+reset value in the next cycle regardless of the data-in value at the time of
+the clock edge.
+
+Currently only $adff cells are supported by this pass.
+\end{lstlisting}
+
+\section{attrmap -- renaming attributes}
+\label{cmd:attrmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    attrmap [options] [selection]
+
+This command renames attributes and/or mapps key/value pairs to
+other key/value pairs.
+
+    -tocase <name>
+        Match attribute names case-insensitively and set it to the specified
+        name.
+
+    -rename <old_name> <new_name>
+        Rename attributes as specified
+
+    -map <old_name>=<old_value> <new_name>=<new_value>
+        Map key/value pairs as indicated.
+
+    -imap <old_name>=<old_value> <new_name>=<new_value>
+        Like -map, but use case-insensitive match for <old_value> when
+        it is a string value.
+
+    -remove <name>=<value>
+        Remove attributes matching this pattern.
+
+    -modattr
+        Operate on module attributes instead of attributes on wires and cells.
+
+For example, mapping Xilinx-style "keep" attributes to Yosys-style:
+
+    attrmap -tocase keep -imap keep="true" keep=1 \
+            -imap keep="false" keep=0 -remove keep=0
+\end{lstlisting}
+
+\section{attrmvcp -- move or copy attributes from wires to driving cells}
+\label{cmd:attrmvcp}
+\begin{lstlisting}[numbers=left,frame=single]
+    attrmvcp [options] [selection]
+
+Move or copy attributes on wires to the cells driving them.
+
+    -copy
+        By default, attributes are moved. This will only add
+        the attribute to the cell, without removing it from
+        the wire.
+
+    -purge
+        If no selected cell consumes the attribute, then it is
+        left on the wire by default. This option will cause the
+        attribute to be removed from the wire, even if no selected
+        cell takes it.
+
+    -driven
+        By default, attriburtes are moved to the cell driving the
+        wire. With this option set it will be moved to the cell
+        driven by the wire instead.
+
+    -attr <attrname>
+        Move or copy this attribute. This option can be used
+        multiple times.
+\end{lstlisting}
+
+\section{blackbox -- change type of cells in the design}
+\label{cmd:blackbox}
+\begin{lstlisting}[numbers=left,frame=single]
+    blackbox [options] [selection]
+
+Convert modules into blackbox modules (remove contents and set the blackbox
+module attribute).
+\end{lstlisting}
+
 \section{cd -- a shortcut for 'select -module <name>'}
 \label{cmd:cd}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -70,1088 +327,3900 @@ 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 ..
 
+Remove trailing substrings that start with '.' in current module name until
+the name of a module in the current design is generated, then switch to that
+module. Otherwise clear the current selection.
+
+    cd
+
 This is just a shortcut for 'select -clear'.
 \end{lstlisting}
 
-\section{clean -- remove unused cells and wires}
-\label{cmd:clean}
+\section{check -- check for obvious problems in the design}
+\label{cmd:check}
 \begin{lstlisting}[numbers=left,frame=single]
-    clean [options] [selection]
+    check [options] [selection]
 
-This is identical to 'opt_clean', but less verbose.
+This pass identifies the following problems in the current design:
 
-When commands are seperated using the ';;' token, this command will be executed
-between the commands.
+ - combinatorial loops
 
-When commands are seperated using the ';;;' token, this command will be executed
-in -purge mode between the commands.
+ - 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 -initdrv then this command also checks for wires which have
+the 'init' attribute set and aren't driven by a FF cell type.
+
+When called with -assert then the command will produce an error if any
+problems are found in the current design.
 \end{lstlisting}
 
-\section{design -- save, restore and reset current design}
-\label{cmd:design}
+\section{chformal -- change formal constraints of the design}
+\label{cmd:chformal}
 \begin{lstlisting}[numbers=left,frame=single]
-    design -reset
+    chformal [types] [mode] [options] [selection]
 
-Clear the current design.
+Make changes to the formal constraints of the design. The [types] options
+the type of constraint to operate on. If none of the folling options is given,
+the command will operate on all constraint types:
 
+    -assert       $assert cells, representing assert(...) constraints
+    -assume       $assume cells, representing assume(...) constraints
+    -live         $live cells, representing assert(s_eventually ...)
+    -fair         $fair cells, representing assume(s_eventually ...)
+    -cover        $cover cells, representing cover() statements
 
-    design -save <name>
+Exactly one of the following modes must be specified:
 
-Save the current design under the given name.
+    -remove
+        remove the cells and thus constraints from the design
 
+    -early
+        bypass FFs that only delay the activation of a constraint
 
-    design -load <name>
+    -delay <N>
+        delay activation of the constraint by <N> clock cycles
 
-Reset the current design and load the design previously saved under the given
-name.
+    -skip <N>
+        ignore activation of the constraint in the first <N> clock cycles
+
+    -assert2assume
+    -assume2assert
+    -live2fair
+    -fair2live
+        change the roles of cells as indicated. this options can be combined
 \end{lstlisting}
 
-\section{dfflibmap -- technology mapping of flip-flops}
-\label{cmd:dfflibmap}
+\section{chparam -- re-evaluate modules with new parameters}
+\label{cmd:chparam}
 \begin{lstlisting}[numbers=left,frame=single]
-    dfflibmap -liberty <file> [selection]
+    chparam [ -set name value ]... [selection]
 
-Map internal flip-flop cells to the flip-flop cells in the technology
-library specified in the given liberty file.
+Re-evaluate the selected modules with new parameters. String values must be
+passed in double quotes (").
 
-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.
+
+    chparam -list [selection]
+
+List the available parameters of the selected modules.
 \end{lstlisting}
 
-\section{dump -- print parts of the design in ilang format}
-\label{cmd:dump}
+\section{chtype -- change type of cells in the design}
+\label{cmd:chtype}
 \begin{lstlisting}[numbers=left,frame=single]
-    dump [options] [selection]
+    chtype [options] [selection]
 
-Write the selected parts of the design to the console or specified file in
-ilang format.
+Change the types of cells in the design.
+
+    -set <type>
+        set the cell type to the given type
 
-    -outfile <filename>
-        Write to the specified file.
+    -map <old_type> <new_type>
+        change cells types that match <old_type> to <new_type>
 \end{lstlisting}
 
-\section{eval -- evaluate the circuit given an input}
-\label{cmd:eval}
+\section{clean -- remove unused cells and wires}
+\label{cmd:clean}
 \begin{lstlisting}[numbers=left,frame=single]
-    eval [options] [selection]
+    clean [options] [selection]
 
-This command evaluates the value of a signal given the value of all required
-inputs.
+This is identical to 'opt_clean', but less verbose.
 
-    -set <signal> <value>
-        set the specified signal to the specified value.
+When commands are separated using the ';;' token, this command will be executed
+between the commands.
 
-    -show <signal>
-        show the value for the specified signal. if no -show option is passed
-        then all output ports of the current module are used.
+When commands are separated using the ';;;' token, this command will be executed
+in -purge mode between the commands.
 \end{lstlisting}
 
-\section{extract -- find subcircuits and replace them with cells}
-\label{cmd:extract}
+\section{clk2fflogic -- convert clocked FFs to generic \$ff cells}
+\label{cmd:clk2fflogic}
 \begin{lstlisting}[numbers=left,frame=single]
-    extract -map <map_file> [options] [selection]
-    extract -mine <out_file> [options] [selection]
-
-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).
+    clk2fflogic [options] [selection]
 
-    -map <map_file>
-        use the modules in this file as reference
+This command replaces clocked flip-flops with generic $ff cells that use the
+implicit global clock. This is useful for formal verification of designs with
+multiple clocks.
+\end{lstlisting}
 
-    -verbose
-        print debug output while analyzing
+\section{connect -- create or remove connections}
+\label{cmd:connect}
+\begin{lstlisting}[numbers=left,frame=single]
+    connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr>
 
-    -constports
-        also find instances with constant drivers. this may be much
-        slower than the normal operation.
+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.
 
-    -nodefaultswaps
-        normally builtin port swapping rules for internal cells are used per
-        default. This turns that off, so e.g. 'a^b' does not match 'b^a'
-        when this option is used.
 
-    -compat <needle_type> <haystack_type>
-        Per default, the cells in the map file (needle) must have the
-        type as the cells in the active design (haystack). This option
-        can be used to register additional pairs of types that should
-        match. This option can be used multiple times.
+    connect [-nomap] -unset <expr>
 
-    -swap <needle_type> <port1>,<port2>[,...]
-        Register a set of swapable ports for a needle cell type.
-        This option can be used multiple times.
+Unconnect all existing drivers for the specified expression.
 
-    -perm <needle_type> <port1>,<port2>[,...] <portA>,<portB>[,...]
-        Register a valid permutation of swapable ports for a needle
-        cell type. This option can be used multiple times.
 
-    -cell_attr <attribute_name>
-        Attributes on cells with the given name must match.
+    connect [-nomap] -port <cell> <port> <expr>
 
-    -wire_attr <attribute_name>
-        Attributes on wires with the given name must match.
+Connect the specified cell port to the specified cell port.
 
-This pass does not operate on modules with uprocessed 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
-the following options are to be used instead of the -map option.
+Per default signal alias names are resolved and all signal names are mapped
+the the signal name of the primary driver. Using the -nomap option deactivates
+this behavior.
 
-    -mine <out_file>
-        mine for frequent subcircuits and write them to the given ilang file
+The connect command operates in one module only. Either only one module must
+be selected or an active module must be set using the 'cd' command.
 
-    -mine_cells_span <min> <max>
-        only mine for subcircuits with the specified number of cells
-        default value: 3 5
+This command does not operate on module with processes.
+\end{lstlisting}
 
-    -mine_min_freq <num>
-        only mine for subcircuits with at least the specified number of matches
-        default value: 10
+\section{connwrappers -- match width of input-output port pairs}
+\label{cmd:connwrappers}
+\begin{lstlisting}[numbers=left,frame=single]
+    connwrappers [options] [selection]
 
-    -mine_limit_matches_per_module <num>
-        when calculating the number of matches for a subcircuit, don't count
-        more than the specified number of matches per module
+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 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.
 
-    -mine_max_fanout <num>
-        don't consider internal signals with more than <num> connections
+    -signed <cell_type> <port_name> <width_param>
+    -unsigned <cell_type> <port_name> <width_param>
+        consider the specified signed/unsigned wrapper output
 
-The modules in the map file may have the attribute 'extract_order' set to an
-integer value. Then this value is used to determine the order in which the pass
-tries to map the modules to the design (ascending, default value is 0).
+    -port <cell_type> <port_name> <width_param> <sign_param>
+        use the specified parameter to decide if signed or unsigned
 
-See 'help techmap' for a pass that does the opposite thing.
+The options -signed, -unsigned, and -port can be specified multiple times.
 \end{lstlisting}
 
-\section{flatten -- flatten design}
-\label{cmd:flatten}
+\section{coolrunner2\_sop -- break \$sop cells into ANDTERM/ORTERM cells}
+\label{cmd:coolrunner2_sop}
 \begin{lstlisting}[numbers=left,frame=single]
-    flatten [selection]
+    coolrunner2_sop [options] [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 using the current design as mapping library.
+Break $sop cells into ANDTERM/ORTERM cells.
 \end{lstlisting}
 
-\section{freduce -- perform functional reduction}
-\label{cmd:freduce}
+\section{copy -- copy modules in the design}
+\label{cmd:copy}
 \begin{lstlisting}[numbers=left,frame=single]
-    freduce [options] [selection]
+    copy old_name new_name
 
-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
-removed.
-
-    -try
-        do not issue an error when the analysis fails.
-        (usually beacause of logic loops in the design)
+Copy the specified module. Note that selection patterns are not supported
+by this command.
 \end{lstlisting}
 
-\section{fsm -- extract and optimize finite state machines}
-\label{cmd:fsm}
+\section{cover -- print code coverage counters}
+\label{cmd:cover}
 \begin{lstlisting}[numbers=left,frame=single]
-    fsm [options] [selection]
+    cover [options] [pattern]
 
-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:
+Print the code coverage counters collected using the cover() macro in the Yosys
+C++ code. This is useful to figure out what parts of Yosys are utilized by a
+test bench.
 
-    fsm_detect          unless got option -nodetect
-    fsm_extract
+    -q
+        Do not print output to the normal destination (console and/or log file)
 
-    fsm_opt
-    opt_clean
-    fsm_opt
+    -o file
+        Write output to this file, truncate if exists.
 
-    fsm_expand          if got option -expand
-    opt_clean           if got option -expand
-    fsm_opt             if got option -expand
+    -a file
+        Write output to this file, append if exists.
 
-    fsm_recode          unless got option -norecode
+    -d dir
+        Write output to a newly created file in the specified directory.
 
-    fsm_info
+When one or more pattern (shell wildcards) are specified, then only counters
+matching at least one pattern are printed.
 
-    fsm_export          if got option -export
-    fsm_map             unless got option -nomap
 
-Options:
+It is also possible to instruct Yosys to print the coverage counters on program
+exit to a file using environment variables:
 
-    -expand, -norecode, -export, -nomap
-        enable or disable passes as indicated above
+    YOSYS_COVER_DIR="{dir-name}" yosys {args}
 
-    -encoding tye
-    -fm_set_fsm_file file
-        passed through to fsm_recode pass
-\end{lstlisting}
+        This will create a file (with an auto-generated name) in this
+        directory and write the coverage counters to it.
 
-\section{fsm\_detect -- finding FSMs in design}
-\label{cmd:fsm_detect}
-\begin{lstlisting}[numbers=left,frame=single]
-    fsm_detect [selection]
+    YOSYS_COVER_FILE="{file-name}" yosys {args}
 
-This pass detects finite state machines by identifying the state signal.
-The state signal is then marked by setting the attribute 'fsm_encoding'
-on the state signal to "auto".
+        This will append the coverage counters to the specified file.
 
-Existing 'fsm_encoding' attributes are not changed by this pass.
 
-Signals can be protected from being detected by this pass by setting the
-'fsm_encoding' attribute to "none".
-\end{lstlisting}
+Hint: Use the following AWK command to consolidate Yosys coverage files:
 
-\section{fsm\_expand -- expand FSM cells by merging logic into it}
-\label{cmd:fsm_expand}
-\begin{lstlisting}[numbers=left,frame=single]
-    fsm_expand [selection]
+    gawk '{ p[$3] = $1; c[$3] += $2; } END { for (i in p)
+      printf "%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3
 
-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.
+
+Coverage counters are only available in Yosys for Linux.
 \end{lstlisting}
 
-\section{fsm\_export -- exporting FSMs to KISS2 files}
-\label{cmd:fsm_export}
+\section{delete -- delete objects in the design}
+\label{cmd:delete}
 \begin{lstlisting}[numbers=left,frame=single]
-    fsm_export [-noauto] [-o filename] [-origenc] [selection]
+    delete [selection]
 
-This pass creates a KISS2 file for every selected FSM. For FSMs with the
-'fsm_export' attribute set, the attribute value is used as filename, otherwise
-the module and cell name is used as filename. If the parameter '-o' is given,
-the first exported FSM is written to the specified filename. This overwrites
-the setting as specified with the 'fsm_export' attribute. All other FSMs are
-exported to the default name as mentioned above.
+Deletes the selected objects. This will also remove entire modules, if the
+whole module is selected.
 
-    -noauto
-        only export FSMs that have the 'fsm_export' attribute set
 
-    -o filename
-        filename of the first exported FSM
+    delete {-input|-output|-port} [selection]
 
-    -origenc
-        use binary state encoding as state names instead of s0, s1, ...
+Does not delete any object but removes the input and/or output flag on the
+selected wires, thus 'deleting' module ports.
 \end{lstlisting}
 
-\section{fsm\_extract -- extracting FSMs in design}
-\label{cmd:fsm_extract}
+\section{deminout -- demote inout ports to input or output}
+\label{cmd:deminout}
 \begin{lstlisting}[numbers=left,frame=single]
-    fsm_extract [selection]
+    deminout [options] [selection]
 
-This pass operates on all signals marked as FSM state signals using the
-'fsm_encoding' attribute. It consumes the logic that creates the state signal
-and uses the state signal to generate control signal and replaces it with an
-FSM cell.
-
-The generated FSM cell still generates the original state signal with its
-original encoding. The 'fsm_opt' pass can be used in combination with the
-'opt_clean' pass to eliminate this signal.
+"Demote" inout ports to input or output ports, if possible.
 \end{lstlisting}
 
-\section{fsm\_info -- print information on finite state machines}
-\label{cmd:fsm_info}
+\section{design -- save, restore and reset current design}
+\label{cmd:design}
 \begin{lstlisting}[numbers=left,frame=single]
-    fsm_info [selection]
+    design -reset
 
-This pass dumps all internal information on FSM cells. It can be useful for
-analyzing the synthesis process and is called automatically by the 'fsm'
-pass so that this information is included in the synthesis log file.
-\end{lstlisting}
+Clear the current design.
 
-\section{fsm\_map -- mapping FSMs to basic logic}
-\label{cmd:fsm_map}
-\begin{lstlisting}[numbers=left,frame=single]
-    fsm_map [selection]
 
-This pass translates FSM cells to flip-flops and logic.
-\end{lstlisting}
+    design -save <name>
 
-\section{fsm\_opt -- optimize finite state machines}
-\label{cmd:fsm_opt}
-\begin{lstlisting}[numbers=left,frame=single]
-    fsm_opt [selection]
+Save the current design under the given name.
 
-This pass optimizes FSM cells. It detects which output signals are actually
-not used and removes them from the FSM. This pass is usually used in
-combination with the 'opt_clean' pass (see also 'help fsm').
-\end{lstlisting}
 
-\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]
+    design -stash <name>
 
-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'.
+Save the current design under the given name and then clear the current design.
 
-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.
-\end{lstlisting}
 
-\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
-\end{lstlisting}
+    design -push
 
-\section{hierarchy -- check, expand and clean up design hierarchy}
-\label{cmd:hierarchy}
-\begin{lstlisting}[numbers=left,frame=single]
-    hierarchy [-check] [-top <module>]
-    hierarchy -generate <cell-types> <port-decls>
+Push the current design to the stack and then clear the current design.
 
-In parametric designs, a module might exists in serveral variations with
-different parameter values. This pass looks at all modules in the current
-design an re-runs the language frontends for the parametric modules as
-needed.
 
-    -check
-        also check the design hierarchy. this generates an error when
-        an unknown module is used as cell type.
+    design -pop
 
-    -keep_positionals
-        per default this pass also converts positional arguments in cells
-        to arguments using port names. this option disables this behavior.
+Reset the current design and pop the last design from the stack.
 
-    -top <module>
-        use the specified top module to built a design hierarchy. modules
-        outside this tree (unused modules) are removed.
 
-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
-determine the direction of the ports. The syntax for a port declaration is:
+    design -load <name>
 
-    {i|o|io}[@<num>]:<portname>
+Reset the current design and load the design previously saved under the given
+name.
 
-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
-using positional arguments). When <num> is not specified, the <portname> can
-also contain wildcard characters.
 
-This pass ignores the current selection and always operates on all modules
-in the current design.
-\end{lstlisting}
+    design -copy-from <name> [-as <new_mod_name>] <selection>
 
-\section{iopadmap -- technology mapping of i/o pads (or buffers)}
-\label{cmd:iopadmap}
-\begin{lstlisting}[numbers=left,frame=single]
-    iopadmap [options] [selection]
+Copy modules from the specified design into the current one. The selection is
+evaluated in the other design.
 
-Map module inputs/outputs to PAD cells from a library. This pass
-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
-        signal is passed through the pad call, using the 2nd
-        portname as output.
+    design -copy-to <name> [-as <new_mod_name>] [selection]
 
-    -outpad <celltype> <portname>[:<portname>]
-    -inoutpad <celltype> <portname>[:<portname>]
-        Similar to -inpad, but for output and inout ports.
+Copy modules from the current design into the specified one.
 
-    -widthparam <param_name>
-        Use the specified parameter name to set the port width.
 
-    -nameparam <param_name>
-        Use the specified parameter to set the port name.
+    design -import <name> [-as <new_top_name>] [selection]
+
+Import the specified design into the current design. The source design must
+either have a selected top module or the selection must contain exactly one
+module that is then used as top module for this command.
+
+
+    design -reset-vlog
+
+The Verilog front-end remembers defined macros and top-level declarations
+between calls to 'read_verilog'. This command resets this memory.
 \end{lstlisting}
 
-\section{ls -- list modules or objects in modules}
-\label{cmd:ls}
+\section{dff2dffe -- transform \$dff cells to \$dffe cells}
+\label{cmd:dff2dffe}
 \begin{lstlisting}[numbers=left,frame=single]
-    ls
+    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
+$_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 <internal_gate_type> <external_gate_type>
+        map directly to external gate type. <internal_gate_type> can
+        be any internal gate-level FF cell (except $_DFFE_??_). the
+        <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 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_*_, and $__DFFSE_* for those matching
+        $_DFFS_*_, except for $_DFF_[NP]_, which is converted to 
+        $_DFFE_[NP]_.
+\end{lstlisting}
 
-When no active module is selected, this prints a list of all module.
+\section{dff2dffs -- process sync set/reset with SR over CE priority}
+\label{cmd:dff2dffs}
+\begin{lstlisting}[numbers=left,frame=single]
+    dff2dffs [options] [selection]
 
-When an active module is selected, this prints a list of objects in the module.
+Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before
+dff2dffe for SR over CE priority.
 \end{lstlisting}
 
-\section{memory -- translate memories to basic cells}
-\label{cmd:memory}
+\section{dffinit -- set INIT param on FF cells}
+\label{cmd:dffinit}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory [-nomap] [selection]
+    dffinit [options] [selection]
 
-This pass calls all the other memory_* passes in a useful order:
+This pass sets an FF cell parameter to the the initial value of the net it
+drives. (This is primarily used in FPGA flows.)
 
-    memory_dff
-    memory_collect
-    memory_map          (skipped if called with -nomap)
+    -ff <cell_name> <output_port> <init_param>
+        operate on the specified cell type. this option can be used
+        multiple times.
 
-This converts memories to word-wide DFFs and address decoders
-or multiport memory blocks if called with the -nomap option.
+    -highlow
+        use the string values "high" and "low" to represent a single-bit
+        initial value of 1 or 0. (multi-bit values are not supported in this
+        mode.)
 \end{lstlisting}
 
-\section{memory\_collect -- creating multi-port memory cells}
-\label{cmd:memory_collect}
+\section{dfflibmap -- technology mapping of flip-flops}
+\label{cmd:dfflibmap}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory_collect [selection]
+    dfflibmap [-prepare] -liberty <file> [selection]
 
-This pass collects memories and memory ports and creates generic multiport
-memory cells.
-\end{lstlisting}
+Map internal flip-flop cells to the flip-flop cells in the technology
+library specified in the given liberty file.
 
-\section{memory\_dff -- merge input/output DFFs into memories}
-\label{cmd:memory_dff}
-\begin{lstlisting}[numbers=left,frame=single]
-    memory_dff [selection]
+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.
 
-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.
+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{memory\_map -- translate multiport memories to basic cells}
-\label{cmd:memory_map}
+\section{dffsr2dff -- convert DFFSR cells to simpler FF cell types}
+\label{cmd:dffsr2dff}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory_map [selection]
+    dffsr2dff [options] [selection]
 
-This pass converts multiport memory cells as generated by the memory_collect
-pass to word-wide DFFs and address decoders.
+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{opt -- perform simple optimizations}
-\label{cmd:opt}
+\section{dump -- print parts of the design in ilang format}
+\label{cmd:dump}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt [selection]
+    dump [options] [selection]
 
-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:
+Write the selected parts of the design to the console or specified file in
+ilang format.
 
-    opt_const
-    opt_share -nomux
+    -m
+        also dump the module headers, even if only parts of a single
+        module is selected
 
-    do
-        opt_muxtree
-        opt_reduce
-        opt_share
-        opt_rmdff
-        opt_clean
-        opt_const
-    while [changed design]
+    -n
+        only dump the module headers if the entire module is selected
+
+    -o <filename>
+        write to the specified file.
+
+    -a <filename>
+        like -outfile but append instead of overwrite
 \end{lstlisting}
 
-\section{opt\_clean -- remove unused cells and wires}
-\label{cmd:opt_clean}
+\section{echo -- turning echoing back of commands on and off}
+\label{cmd:echo}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_clean [options] [selection]
+    echo on
 
-This pass identifies wires and cells that are unused and removes them. Other
-passes often remove cells but leave the wires in the design or reconnect the
-wires but leave the old cells in the design. This pass can be used to clean up
-after the passes that do the actual work.
+Print all commands to log before executing them.
 
-This pass only operates on completely selected modules without processes.
 
-    -purge
-        also remove internal nets if they have a public name
+    echo off
+
+Do not print all commands to log before executing them. (default)
 \end{lstlisting}
 
-\section{opt\_const -- perform const folding}
-\label{cmd:opt_const}
+\section{edgetypes -- list all types of edges in selection}
+\label{cmd:edgetypes}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_const [selection]
+    edgetypes [options] [selection]
 
-This pass performs const folding on internal cell types with constant inputs.
+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{opt\_muxtree -- eliminate dead trees in multiplexer trees}
-\label{cmd:opt_muxtree}
+\section{equiv\_add -- add a \$equiv cell}
+\label{cmd:equiv_add}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_muxtree [selection]
+    equiv_add [-try] gold_sig gate_sig
 
-This pass analyzes the control signals for the multiplexer trees in the design
-and identifies inputs that can never be active. It then removes this dead
-branches from the multiplexer trees.
+This command adds an $equiv cell for the specified signals.
 
-This pass only operates on completely selected modules without processes.
+
+    equiv_add [-try] -cell gold_cell gate_cell
+
+This command adds $equiv cells for the ports of the specified cells.
 \end{lstlisting}
 
-\section{opt\_reduce -- simplify large MUXes and AND/OR gates}
-\label{cmd:opt_reduce}
+\section{equiv\_induct -- proving \$equiv cells using temporal induction}
+\label{cmd:equiv_induct}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_reduce [selection]
-
-This pass performs two interlinked optimizations:
+    equiv_induct [options] [selection]
 
-1. it consolidates trees of large AND gates or OR gates and eliminates
-duplicated inputs.
+Uses a version of temporal induction to prove $equiv cells.
 
-2. it identifies duplicated inputs to MUXes and replaces them with a single
-input with the original control signals OR'ed together.
-\end{lstlisting}
+Only selected $equiv cells are proven and only selected cells are used to
+perform the proof.
 
-\section{opt\_rmdff -- remove DFFs with constant inputs}
-\label{cmd:opt_rmdff}
-\begin{lstlisting}[numbers=left,frame=single]
-    opt_rmdff [selection]
+    -undef
+        enable modelling of undef states
 
-This pass identifies flip-flops with constant inputs and replaces them with
-a constant driver.
-\end{lstlisting}
+    -seq <N>
+        the max. number of time steps to be considered (default = 4)
 
-\section{opt\_share -- consolidate identical cells}
-\label{cmd:opt_share}
-\begin{lstlisting}[numbers=left,frame=single]
-    opt_share [-nomux] [selection]
+This command is very effective in proving complex sequential circuits, when
+the internal state of the circuit quickly propagates to $equiv cells.
 
-This pass identifies cells with identical type and input signals. Such cells
-are then merged to one cell.
+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 <N> cycles (the <N>
+specified via -seq).
 
-    -nomux
-        Do not merge MUX cells.
+Combined with simulation this is very powerful because simulation can give
+you confidence that the circuits start out synced for at least <N> cycles
+after reset.
 \end{lstlisting}
 
-\section{proc -- translate processes to netlists}
-\label{cmd:proc}
+\section{equiv\_make -- prepare a circuit for equivalence checking}
+\label{cmd:equiv_make}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc [options] [selection]
+    equiv_make [options] gold_module gate_module equiv_module
 
-This pass calls all the other proc_* passes in the most common order.
+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.
 
-    proc_clean
-    proc_rmdead
-    proc_init
-    proc_arst
-    proc_mux
-    proc_dff
-    proc_clean
+    -inames
+        Also match cells and wires with $... names.
 
-This replaces the processes in the design with multiplexers and flip-flops.
+    -blacklist <file>
+        Do not match cells or signals that match the names in the file.
 
-The following options are supported:
+    -encfile <file>
+        Match FSM encodings using the description from the file.
+        See 'help fsm_recode' for details.
 
-    -global_arst [!]<netname>
-        This option is passed through to proc_arst.
+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{proc\_arst -- detect asynchronous resets}
-\label{cmd:proc_arst}
+\section{equiv\_mark -- mark equivalence checking regions}
+\label{cmd:equiv_mark}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc_arst [-global_arst [!]<netname>] [selection]
-
-This pass identifies asynchronous resets in the processes and converts them
-to a different internal representation that is suitable for generating
-flip-flop cells with asynchronous resets.
+    equiv_mark [options] [selection]
 
-    -global_arst [!]<netname>
-        In modules that have a net with the given name, use this net as async
-        reset for registers that have been assign initial values in their
-        declaration ('reg foobar = constant_value;'). Use the '!' modifier for
-        active low reset signals. Note: the frontend stores the default value
-        in the 'init' attribute on the net.
+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{proc\_clean -- remove empty parts of processes}
-\label{cmd:proc_clean}
+\section{equiv\_miter -- extract miter from equiv circuit}
+\label{cmd:equiv_miter}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc_clean [selection]
+    equiv_miter [options] miter_module [selection]
 
-This pass removes empty parts of processes and ultimately removes a process
-if it contains only empty structures.
-\end{lstlisting}
+This creates a miter module for further analysis of the selected $equiv cells.
 
-\section{proc\_dff -- extract flip-flops from processes}
-\label{cmd:proc_dff}
-\begin{lstlisting}[numbers=left,frame=single]
-    proc_dff [selection]
+    -trigger
+        Create a trigger output
 
-This pass identifies flip-flops in the processes and converts them to
-d-type flip-flop cells.
-\end{lstlisting}
+    -cmp
+        Create cmp_* outputs for individual unproven $equiv cells
 
-\section{proc\_init -- convert initial block to init attributes}
-\label{cmd:proc_init}
-\begin{lstlisting}[numbers=left,frame=single]
-    proc_init [selection]
+    -assert
+        Create a $assert cell for each unproven $equiv cell
 
-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.
+    -undef
+        Create compare logic that handles undefs correctly
 \end{lstlisting}
 
-\section{proc\_mux -- convert decision trees to multiplexers}
-\label{cmd:proc_mux}
+\section{equiv\_purge -- purge equivalence checking module}
+\label{cmd:equiv_purge}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc_mux [selection]
+    equiv_purge [options] [selection]
 
-This pass converts the decision trees in processes (originating from if-else
-and case statements) to trees of multiplexer cells.
+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{proc\_rmdead -- eliminate dead trees in decision trees}
-\label{cmd:proc_rmdead}
+\section{equiv\_remove -- remove \$equiv cells}
+\label{cmd:equiv_remove}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc_rmdead [selection]
+    equiv_remove [options] [selection]
 
-This pass identifies unreachable branches in decision trees and removes them.
-\end{lstlisting}
+This command removes the selected $equiv cells. If neither -gold nor -gate is
+used then only proven cells are removed.
 
-\section{read\_ilang -- read modules from ilang file}
-\label{cmd:read_ilang}
-\begin{lstlisting}[numbers=left,frame=single]
-    read_ilang [filename]
+    -gold
+        keep gold circuit
 
-Load modules from an ilang file to the current design. (ilang is a text
-representation of a design in yosys's internal format.)
+    -gate
+        keep gate circuit
 \end{lstlisting}
 
-\section{read\_verilog -- read modules from verilog file}
-\label{cmd:read_verilog}
+\section{equiv\_simple -- try proving simple \$equiv instances}
+\label{cmd:equiv_simple}
 \begin{lstlisting}[numbers=left,frame=single]
-    read_verilog [filename]
+    equiv_simple [options] [selection]
 
-Load modules from a verilog file to the current design. A large subset of
-Verilog-2005 is supported.
+This command tries to prove $equiv cells using a simple direct SAT approach.
 
-    -dump_ast1
-        dump abstract syntax tree (before simplification)
+    -v
+        verbose output
 
-    -dump_ast2
-        dump abstract syntax tree (after simplification)
+    -undef
+        enable modelling of undef states
 
-    -dump_vlog
-        dump ast as verilog code (after simplification)
+    -short
+        create shorter input cones that stop at shared nodes. This yields
+        simpler SAT problems but sometimes fails to prove equivalence.
 
-    -yydebug
-        enable parser debug output
+    -nogroup
+        disabling grouping of $equiv cells by output wire
 
-    -nolatches
-        usually latches are synthesized into logic loops
+    -seq <N>
+        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{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]
+    eval [options] [selection]
+
+This command evaluates the value of a signal given the value of all required
+inputs.
+
+    -set <signal> <value>
+        set the specified signal to the specified value.
+
+    -set-undef
+        set all unspecified source signals to undef (x)
+
+    -table <signal>
+        create a truth table using the specified input signals
+
+    -show <signal>
+        show the value for the specified signal. if no -show option is passed
+        then all output ports of the current module are used.
+\end{lstlisting}
+
+\section{expose -- convert internal signals to module ports}
+\label{cmd:expose}
+\begin{lstlisting}[numbers=left,frame=single]
+    expose [options] [selection]
+
+This command exposes all selected internal signals of a module as additional
+outputs.
+
+    -dff
+        only consider wires that are directly driven by register cell.
+
+    -cut
+        when exposing a wire, create an input/output pair and cut the internal
+        signal path at that wire.
+
+    -input
+        when exposing a wire, create an input port and disconnect the internal
+        driver.
+
+    -shared
+        only expose those signals that are shared among the selected modules.
+        this is useful for preparing modules for equivalence checking.
+
+    -evert
+        also turn connections to instances of other modules to additional
+        inputs and outputs and remove the module instances.
+
+    -evert-dff
+        turn flip-flops to sets of inputs and outputs.
+
+    -sep <separator>
+        when creating new wire/port names, the original object name is suffixed
+        with this separator (default: '.') and the port name or a type
+        designator for the exposed signal.
+\end{lstlisting}
+
+\section{extract -- find subcircuits and replace them with cells}
+\label{cmd:extract}
+\begin{lstlisting}[numbers=left,frame=single]
+    extract -map <map_file> [options] [selection]
+    extract -mine <out_file> [options] [selection]
+
+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 <map_file>
+        use the modules in this file as reference. This option can be used
+        multiple times.
+
+    -map %<design-name>
+        use the modules in this in-memory design as reference. This option can
+        be used multiple times.
+
+    -verbose
+        print debug output while analyzing
+
+    -constports
+        also find instances with constant drivers. this may be much
+        slower than the normal operation.
+
+    -nodefaultswaps
+        normally builtin port swapping rules for internal cells are used per
+        default. This turns that off, so e.g. 'a^b' does not match 'b^a'
+        when this option is used.
+
+    -compat <needle_type> <haystack_type>
+        Per default, the cells in the map file (needle) must have the
+        type as the cells in the active design (haystack). This option
+        can be used to register additional pairs of types that should
+        match. This option can be used multiple times.
+
+    -swap <needle_type> <port1>,<port2>[,...]
+        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 swappable ports for a needle
+        cell type. This option can be used multiple times.
+
+    -cell_attr <attribute_name>
+        Attributes on cells with the given name must match.
+
+    -wire_attr <attribute_name>
+        Attributes on wires with the given name must match.
+
+    -ignore_parameters
+        Do not use parameters when matching cells.
+
+    -ignore_param <cell_type> <parameter_name>
+        Do not use this parameter when matching cells.
+
+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
+the following options are to be used instead of the -map option.
+
+    -mine <out_file>
+        mine for frequent subcircuits and write them to the given ilang file
+
+    -mine_cells_span <min> <max>
+        only mine for subcircuits with the specified number of cells
+        default value: 3 5
+
+    -mine_min_freq <num>
+        only mine for subcircuits with at least the specified number of matches
+        default value: 10
+
+    -mine_limit_matches_per_module <num>
+        when calculating the number of matches for a subcircuit, don't count
+        more than the specified number of matches per module
+
+    -mine_max_fanout <num>
+        don't consider internal signals with more than <num> connections
+
+The modules in the map file may have the attribute 'extract_order' set to an
+integer value. Then this value is used to determine the order in which the pass
+tries to map the modules to the design (ascending, default value is 0).
+
+See 'help techmap' for a pass that does the opposite thing.
+\end{lstlisting}
+
+\section{extract\_counter -- Extract GreenPak4 counter cells}
+\label{cmd:extract_counter}
+\begin{lstlisting}[numbers=left,frame=single]
+    extract_counter [options] [selection]
+
+This pass converts non-resettable or async resettable down counters to
+counter cells. Use a target-specific 'techmap' map file to convert those cells
+to the actual target cells.
+
+    -maxwidth N
+        Only extract counters up to N bits wide
+
+    -pout X,Y,...
+        Only allow parallel output from the counter to the listed cell types
+        (if not specified, parallel outputs are not restricted)
+\end{lstlisting}
+
+\section{extract\_fa -- find and extract full/half adders}
+\label{cmd:extract_fa}
+\begin{lstlisting}[numbers=left,frame=single]
+    extract_fa [options] [selection]
+
+This pass extracts full/half adders from a gate-level design.
+
+    -fa, -ha
+        Enable cell types (fa=full adder, ha=half adder)
+        All types are enabled if none of this options is used
+
+    -d <int>
+        Set maximum depth for extracted logic cones (default=20)
+
+    -b <int>
+        Set maximum breadth for extracted logic cones (default=6)
+
+    -v
+        Verbose output
+\end{lstlisting}
+
+\section{extract\_reduce -- converts gate chains into \$reduce\_* cells}
+\label{cmd:extract_reduce}
+\begin{lstlisting}[numbers=left,frame=single]
+    extract_reduce [options] [selection]
+
+converts gate chains into $reduce_* cells
+
+This command finds chains of $_AND_, $_OR_, and $_XOR_ cells and replaces them
+with their corresponding $reduce_* cells. Because this command only operates on
+these cell types, it is recommended to map the design to only these cell types
+using the `abc -g` command. Note that, in some cases, it may be more effective
+to map the design to only $_AND_ cells, run extract_reduce, map the remaining
+parts of the design to AND/OR/XOR cells, and run extract_reduce a second time.
+
+    -allow-off-chain
+        Allows matching of cells that have loads outside the chain. These cells
+        will be replicated and folded into the $reduce_* cell, but the original
+        cell will remain, driving its original loads.
+\end{lstlisting}
+
+\section{flatten -- flatten design}
+\label{cmd:flatten}
+\begin{lstlisting}[numbers=left,frame=single]
+    flatten [selection]
+
+This pass flattens the design by replacing cells by their implementation. 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}
+\label{cmd:freduce}
+\begin{lstlisting}[numbers=left,frame=single]
+    freduce [options] [selection]
+
+This pass performs functional reduction in the circuit. I.e. if two nodes are
+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
+        enable verbose or very verbose output
+
+    -inv
+        enable explicit handling of inverted signals
+
+    -stop <n>
+        stop after <n> reduction operations. this is mostly used for
+        debugging the freduce command itself.
+
+    -dump <prefix>
+        dump the design to <prefix>_<module>_<num>.il after each reduction
+        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
+equivalent nodes.
+
+All selected wires are considered for rewiring. The selected cells cover the
+circuit that is analyzed.
+\end{lstlisting}
+
+\section{fsm -- extract and optimize finite state machines}
+\label{cmd:fsm}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm [options] [selection]
+
+This pass calls all the other fsm_* passes in a useful order. This performs
+FSM extraction and optimization. It also calls opt_clean as needed:
+
+    fsm_detect          unless got option -nodetect
+    fsm_extract
+
+    fsm_opt
+    opt_clean
+    fsm_opt
+
+    fsm_expand          if got option -expand
+    opt_clean           if got option -expand
+    fsm_opt             if got option -expand
+
+    fsm_recode          unless got option -norecode
+
+    fsm_info
+
+    fsm_export          if got option -export
+    fsm_map             unless got option -nomap
+
+Options:
+
+    -expand, -norecode, -export, -nomap
+        enable or disable passes as indicated above
+
+    -fullexpand
+        call expand with -full option
+
+    -encoding type
+    -fm_set_fsm_file file
+    -encfile file
+        passed through to fsm_recode pass
+\end{lstlisting}
+
+\section{fsm\_detect -- finding FSMs in design}
+\label{cmd:fsm_detect}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_detect [selection]
+
+This pass detects finite state machines by identifying the state signal.
+The state signal is then marked by setting the attribute 'fsm_encoding'
+on the state signal to "auto".
+
+Existing 'fsm_encoding' attributes are not changed by this pass.
+
+Signals can be protected from being detected by this pass by setting the
+'fsm_encoding' attribute to "none".
+\end{lstlisting}
+
+\section{fsm\_expand -- expand FSM cells by merging logic into it}
+\label{cmd:fsm_expand}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_expand [-full] [selection]
+
+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 finite state machine.
+
+By default, fsm_expand is still a bit conservative regarding merging larger
+word-wide cells. Call with -full to consider all cells for merging.
+\end{lstlisting}
+
+\section{fsm\_export -- exporting FSMs to KISS2 files}
+\label{cmd:fsm_export}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_export [-noauto] [-o filename] [-origenc] [selection]
+
+This pass creates a KISS2 file for every selected FSM. For FSMs with the
+'fsm_export' attribute set, the attribute value is used as filename, otherwise
+the module and cell name is used as filename. If the parameter '-o' is given,
+the first exported FSM is written to the specified filename. This overwrites
+the setting as specified with the 'fsm_export' attribute. All other FSMs are
+exported to the default name as mentioned above.
+
+    -noauto
+        only export FSMs that have the 'fsm_export' attribute set
+
+    -o filename
+        filename of the first exported FSM
+
+    -origenc
+        use binary state encoding as state names instead of s0, s1, ...
+\end{lstlisting}
+
+\section{fsm\_extract -- extracting FSMs in design}
+\label{cmd:fsm_extract}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_extract [selection]
+
+This pass operates on all signals marked as FSM state signals using the
+'fsm_encoding' attribute. It consumes the logic that creates the state signal
+and uses the state signal to generate control signal and replaces it with an
+FSM cell.
+
+The generated FSM cell still generates the original state signal with its
+original encoding. The 'fsm_opt' pass can be used in combination with the
+'opt_clean' pass to eliminate this signal.
+\end{lstlisting}
+
+\section{fsm\_info -- print information on finite state machines}
+\label{cmd:fsm_info}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_info [selection]
+
+This pass dumps all internal information on FSM cells. It can be useful for
+analyzing the synthesis process and is called automatically by the 'fsm'
+pass so that this information is included in the synthesis log file.
+\end{lstlisting}
+
+\section{fsm\_map -- mapping FSMs to basic logic}
+\label{cmd:fsm_map}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_map [selection]
+
+This pass translates FSM cells to flip-flops and logic.
+\end{lstlisting}
+
+\section{fsm\_opt -- optimize finite state machines}
+\label{cmd:fsm_opt}
+\begin{lstlisting}[numbers=left,frame=single]
+    fsm_opt [selection]
+
+This pass optimizes FSM cells. It detects which output signals are actually
+not used and removes them from the FSM. This pass is usually used in
+combination with the 'opt_clean' pass (see also 'help fsm').
+\end{lstlisting}
+
+\section{fsm\_recode -- recoding finite state machines}
+\label{cmd:fsm_recode}
+\begin{lstlisting}[numbers=left,frame=single]
+    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.
+    -encoding <type>
+        specify the encoding scheme used for FSMs without the
+        'fsm_encoding' attribute or with the attribute set to `auto'.
+
+    -fm_set_fsm_file <file>
+        generate a file containing the mapping from old to new FSM encoding
+        in form of Synopsys Formality set_fsm_* commands.
+
+    -encfile <file>
+        write the mappings from old to new FSM encoding to a file in the
+        following format:
+
+            .fsm <module_name> <state_signal>
+            .map <old_bitpattern> <new_bitpattern>
+\end{lstlisting}
+
+\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches}
+\label{cmd:greenpak4_dffinv}
+\begin{lstlisting}[numbers=left,frame=single]
+    greenpak4_dffinv [options] [selection]
+
+Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells.
+\end{lstlisting}
+
+\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 -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}
+\label{cmd:hierarchy}
+\begin{lstlisting}[numbers=left,frame=single]
+    hierarchy [-check] [-top <module>]
+    hierarchy -generate <cell-types> <port-decls>
+
+In parametric designs, a module might exists in several variations with
+different parameter values. This pass looks at all modules in the current
+design an re-runs the language frontends for the parametric modules as
+needed.
+
+    -check
+        also check the design hierarchy. this generates an error when
+        an unknown module is used as cell type.
+
+    -simcheck
+        like -check, but also thow an error if blackbox modules are
+        instantiated, and throw an error if the design has no top module
+
+    -purge_lib
+        by default the hierarchy command will not remove library (blackbox)
+        modules. use this option to also remove unused blackbox modules.
+
+    -libdir <directory>
+        search for files named <module_name>.v in the specified directory
+        for unknown modules and automatically run read_verilog for each
+        unknown module.
+
+    -keep_positionals
+        per default this pass also converts positional arguments in cells
+        to arguments using port names. this option disables this behavior.
+
+    -keep_portwidths
+        per default this pass adjusts the port width on cells that are
+        module instances when the width does not match the module port. this
+        option disables this behavior.
+
+    -nokeep_asserts
+        per default this pass sets the "keep" attribute on all modules
+        that directly or indirectly contain one or more $assert cells. this
+        option disables this behavior.
+
+    -top <module>
+        use the specified top module to built a design hierarchy. modules
+        outside this tree (unused modules) are removed.
+
+        when the -top option is used, the 'top' attribute will be set on the
+        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
+determine the direction of the ports. The syntax for a port declaration is:
+
+    {i|o|io}[@<num>]:<portname>
+
+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 instantiated
+using positional arguments). When <num> is not specified, the <portname> can
+also contain wildcard characters.
+
+This pass ignores the current selection and always operates on all modules
+in the current design.
+\end{lstlisting}
+
+\section{hilomap -- technology mapping of constant hi- and/or lo-drivers}
+\label{cmd:hilomap}
+\begin{lstlisting}[numbers=left,frame=single]
+    hilomap [options] [selection]
+
+Map constants to 'tielo' and 'tiehi' driver cells.
+
+    -hicell <celltype> <portname>
+        Replace constant hi bits with this cell.
+
+    -locell <celltype> <portname>
+        Replace constant lo bits with this cell.
+
+    -singleton
+        Create only one hi/lo cell and connect all constant bits
+        to that cell. Per default a separate cell is created for
+        each constant bit.
+\end{lstlisting}
+
+\section{history -- show last interactive commands}
+\label{cmd:history}
+\begin{lstlisting}[numbers=left,frame=single]
+    history
+
+This command prints all commands in the shell history buffer. This are
+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_expr -mux_undef -undriven [-full]
+        opt_merge
+        opt_rmdff
+        opt_clean
+    while <changed design>
+
+When called with the option -unlut, this command will transform all already
+mapped SB_LUT4 cells back to logic.
+\end{lstlisting}
+
+\section{insbuf -- insert buffer cells for connected wires}
+\label{cmd:insbuf}
+\begin{lstlisting}[numbers=left,frame=single]
+    insbuf [options] [selection]
+
+Insert buffer cells into the design for directly connected wires.
+
+    -buf <celltype> <in-portname> <out-portname>
+        Use the given cell type instead of $_BUF_. (Notice that the next
+        call to "clean" will remove all $_BUF_ in the design.)
+\end{lstlisting}
+
+\section{iopadmap -- technology mapping of i/o pads (or buffers)}
+\label{cmd:iopadmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    iopadmap [options] [selection]
+
+Map module inputs/outputs to PAD cells from a library. This pass
+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 output port name. if a 2nd portname is given, the
+        signal is passed through the pad call, using the 2nd
+        portname as the port facing the module port.
+
+    -outpad <celltype> <portname>[:<portname>]
+    -inoutpad <celltype> <portname>[:<portname>]
+        Similar to -inpad, but for output and inout ports.
+
+    -toutpad <celltype> <portname>:<portname>[:<portname>]
+        Merges $_TBUF_ cells into the output pad cell. This takes precedence
+        over the other -outpad cell. The first portname is the enable input
+        of the tristate driver.
+
+    -tinoutpad <celltype> <portname>:<portname>:<portname>[:<portname>]
+        Merges $_TBUF_ cells into the inout pad cell. This takes precedence
+        over the other -inoutpad cell. The first portname is the enable input
+        of the tristate driver and the 2nd portname is the internal output
+        buffering the external signal.
+
+    -widthparam <param_name>
+        Use the specified parameter name to set the port width.
+
+    -nameparam <param_name>
+        Use the specified parameter to set the port name.
+
+    -bits
+        create individual bit-wide buffers even for ports that
+        are wider. (the default behavior is to create word-wide
+        buffers using -widthparam to set the word size on the cell.)
+
+Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode.
+\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]
+    log string
+
+Print the given string to the screen and/or the log file. This is useful for TCL
+scripts, because the TCL command "puts" only goes to stdout but not to
+logfiles.
+
+    -stdout
+        Print the output to stdout too. This is useful when all Yosys is executed
+        with a script and the -q (quiet operation) argument to notify the user.
+
+    -stderr
+        Print the output to stderr too.
+
+    -nolog
+        Don't use the internal log() command. Use either -stdout or -stderr,
+        otherwise no output will be generated at all.
+
+    -n
+        do not append a newline
+\end{lstlisting}
+
+\section{ls -- list modules or objects in modules}
+\label{cmd:ls}
+\begin{lstlisting}[numbers=left,frame=single]
+    ls [selection]
+
+When no active module is selected, this prints a list of modules.
+
+When an active module is selected, this prints a list of objects in the module.
+\end{lstlisting}
+
+\section{ltp -- print longest topological path}
+\label{cmd:ltp}
+\begin{lstlisting}[numbers=left,frame=single]
+    ltp [options] [selection]
+
+This command prints the longest topological path in the design. (Only considers
+paths within a single module, so the design must be flattened.)
+
+    -noff
+        automatically exclude FF cell types
+\end{lstlisting}
+
+\section{lut2mux -- convert \$lut to \$\_MUX\_}
+\label{cmd:lut2mux}
+\begin{lstlisting}[numbers=left,frame=single]
+    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 $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] [-nordff] [-memx] [-bram <bram_rules>] [selection]
+
+This pass calls all the other memory_* passes in a useful order:
+
+    memory_dff [-nordff]                (-memx implies -nordff)
+    opt_clean
+    memory_share
+    opt_clean
+    memory_memx                         (when called with -memx)
+    memory_collect
+    memory_bram -rules <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 <rule_file> [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
+      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 1         # number of enable bits
+      transp 0 2         # transparent (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 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.
+
+A match rule looks like this:
+
+    match RAMB1024X32
+      max waste 16384    # only use this bram if <= 16k ram bits are unused
+      min efficiency 80  # only use this bram if efficiency is at least 80%
+    endmatch
+
+It is possible to match against the following values with min/max rules:
+
+    words  ........  number of words in memory in design
+    abits  ........  number of address bits on memory in design
+    dbits  ........  number of data bits on memory in design
+    wports  .......  number of write ports on memory in design
+    rports  .......  number of read ports on memory in design
+    ports  ........  number of ports on memory in design
+    bits  .........  number of bits in memory in design
+    dups ..........  number of duplications for more read ports
+
+    awaste  .......  number of unused address slots for this match
+    dwaste  .......  number of unused data bits for this match
+    bwaste  .......  number of unused bram bits for this match
+    waste  ........  total number of unused bram bits (bwaste*dups)
+    efficiency  ...  total percentage of used and non-duplicated bits
+
+    acells  .......  number of cells in 'address-direction'
+    dcells  .......  number of cells in 'data-direction'
+    cells  ........  total number of cells (acells*dcells*dups)
+
+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.
+
+A match containing the command 'or_next_if_better' is only used if it
+has a higher efficiency than the next match (and the one after that if
+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}
+
+\section{memory\_collect -- creating multi-port memory cells}
+\label{cmd:memory_collect}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_collect [selection]
+
+This pass collects memories and memory ports and creates generic multiport
+memory cells.
+\end{lstlisting}
+
+\section{memory\_dff -- merge input/output DFFs into memories}
+\label{cmd:memory_dff}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_dff [options] [selection]
+
+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.
+
+    -nordfff
+        do not merge registers on read ports
+\end{lstlisting}
+
+\section{memory\_map -- translate multiport memories to basic cells}
+\label{cmd:memory_map}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_map [selection]
+
+This pass converts multiport memory cells as generated by the memory_collect
+pass to word-wide DFFs and address decoders.
+\end{lstlisting}
+
+\section{memory\_memx -- emulate vlog sim behavior for mem ports}
+\label{cmd:memory_memx}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_memx [selection]
+
+This pass adds additional circuitry that emulates the Verilog simulation
+behavior for out-of-bounds memory reads and writes.
+\end{lstlisting}
+
+\section{memory\_nordff -- extract read port FFs from memories}
+\label{cmd:memory_nordff}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_nordff [options] [selection]
+
+This pass extracts FFs from memory read ports. This results in a netlist
+similar to what one would get from calling memory_dff with -nordff.
+\end{lstlisting}
+
+\section{memory\_share -- consolidate memory ports}
+\label{cmd:memory_share}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_share [selection]
+
+This pass merges share-able memory ports into single memory ports.
+
+The following methods are used to consolidate the number of memory ports:
+
+  - When write ports are connected to async read ports accessing the same
+    address, then this feedback path is converted to a write port with
+    byte/part enable signals.
+
+  - When multiple write ports access the same address then this is converted
+    to a single write port with a more complex data and/or enable logic path.
+
+  - When multiple write ports are never accessed at the same time (a SAT
+    solver is used to determine this), then the ports are merged into a single
+    write port.
+
+Note that in addition to the algorithms implemented in this pass, the $memrd
+and $memwr cells are also subject to generic resource sharing passes (and other
+optimizations) such as "share" and "opt_merge".
+\end{lstlisting}
+
+\section{memory\_unpack -- unpack multi-port memory cells}
+\label{cmd:memory_unpack}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_unpack [selection]
+
+This pass converts the multi-port $mem memory cells into individual $memrd and
+$memwr cells. It is the counterpart to the memory_collect pass.
+\end{lstlisting}
+
+\section{miter -- automatically create a miter circuit}
+\label{cmd:miter}
+\begin{lstlisting}[numbers=left,frame=single]
+    miter -equiv [options] gold_name gate_name miter_name
+
+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
+detected.
+
+    -ignore_gold_x
+        a undef (x) bit in the gold module output will match any value in
+        the gate module output.
+
+    -make_outputs
+        also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs
+        on the miter circuit.
+
+    -make_outcmp
+        also create a cmp_* output for each gold/gate output pair.
+
+    -make_assert
+        also create an 'assert' cell that checks if trigger is always low.
+
+    -flatten
+        call 'flatten; opt_expr -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_expr -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.
+
+    -assert
+        Create an error if not all logic can be mapped
+
+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]
+    opt [options] [selection]
+
+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_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+    opt_merge [-share_all] -nomux
+
+    do
+        opt_muxtree
+        opt_reduce [-fine] [-full]
+        opt_merge [-share_all]
+        opt_rmdff [-keepdc]
+        opt_clean [-purge]
+        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+    while <changed design>
+
+When called with -fast the following script is used instead:
+
+    do
+        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+        opt_merge [-share_all]
+        opt_rmdff [-keepdc]
+        opt_clean [-purge]
+    while <changed design in opt_rmdff>
+
+Note: Options in square brackets (such as [-keepdc]) are passed through to
+the opt_* commands when given to 'opt'.
+\end{lstlisting}
+
+\section{opt\_clean -- remove unused cells and wires}
+\label{cmd:opt_clean}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_clean [options] [selection]
+
+This pass identifies wires and cells that are unused and removes them. Other
+passes often remove cells but leave the wires in the design or reconnect the
+wires but leave the old cells in the design. This pass can be used to clean up
+after the passes that do the actual work.
+
+This pass only operates on completely selected modules without processes.
+
+    -purge
+        also remove internal nets if they have a public name
+\end{lstlisting}
+
+\section{opt\_demorgan -- Optimize reductions with DeMorgan equivalents}
+\label{cmd:opt_demorgan}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_demorgan [selection]
+
+This pass pushes inverters through $reduce_* cells if this will reduce the
+overall gate count of the circuit
+\end{lstlisting}
+
+\section{opt\_expr -- perform const folding and simple expression rewriting}
+\label{cmd:opt_expr}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_expr [options] [selection]
+
+This pass performs const folding on internal cell types with constant inputs.
+It also performs some simple expression rewritring.
+
+    -mux_undef
+        remove 'undef' inputs from $mux, $pmux and $_MUX_ cells
+
+    -mux_bool
+        replace $mux cells with inverters or buffers when possible
+
+    -undriven
+        replace undriven nets with undef (x) constants
+
+    -clkinv
+        optimize clock inverters by changing FF types
+
+    -fine
+        perform fine-grain optimizations
+
+    -full
+        alias for -mux_undef -mux_bool -undriven -fine
+
+    -keepdc
+        some optimizations change the behavior of the circuit with respect to
+        don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause
+        all result bits to be set to x. this behavior changes when 'a+0' is
+        replaced by 'a'. the -keepdc option disables all such optimizations.
+\end{lstlisting}
+
+\section{opt\_merge -- consolidate identical cells}
+\label{cmd:opt_merge}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_merge [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{opt\_muxtree -- eliminate dead trees in multiplexer trees}
+\label{cmd:opt_muxtree}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_muxtree [selection]
+
+This pass analyzes the control signals for the multiplexer trees in the design
+and identifies inputs that can never be active. It then removes this dead
+branches from the multiplexer trees.
+
+This pass only operates on completely selected modules without processes.
+\end{lstlisting}
+
+\section{opt\_reduce -- simplify large MUXes and AND/OR gates}
+\label{cmd:opt_reduce}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_reduce [options] [selection]
+
+This pass performs two interlinked optimizations:
+
+1. it consolidates trees of large AND gates or OR gates and eliminates
+duplicated inputs.
+
+2. it identifies duplicated inputs to MUXes and replaces them with a single
+input with the original control signals OR'ed together.
+
+    -fine
+      perform fine-grain optimizations
+
+    -full
+      alias for -fine
+\end{lstlisting}
+
+\section{opt\_rmdff -- remove DFFs with constant inputs}
+\label{cmd:opt_rmdff}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_rmdff [-keepdc] [selection]
+
+This pass identifies flip-flops with constant inputs and replaces them with
+a constant driver.
+\end{lstlisting}
+
+\section{plugin -- load and list loaded plugins}
+\label{cmd:plugin}
+\begin{lstlisting}[numbers=left,frame=single]
+    plugin [options]
+
+Load and list loaded plugins.
+
+    -i <plugin_filename>
+        Load (install) the specified plugin.
+
+    -a <alias_name>
+        Register the specified alias name for the loaded plugin
+
+    -l
+        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')
+
+    -auto-top
+        automatically determine the top of the design hierarchy
+
+    -flatten
+        flatten the design before synthesis. this will pass '-auto-top' to
+        'hierarchy' if no top module is specified.
+
+    -ifx
+        passed to 'proc'. uses verilog simulation behavior for verilog if/case
+        undef handling. this also prevents 'wreduce' from being run.
+
+    -memx
+        simulate verilog simulation behavior for out-of-bounds memory accesses
+        using the 'memory_memx' pass.
+
+    -nomem
+        do not run any of the memory_* passes
+
+    -rdff
+        do not pass -nordff to 'memory_dff'. This enables merging of FFs into
+        memory read ports.
+
+    -nokeepdc
+        do not call opt_* with -keepdc
+
+    -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> | -auto-top]
+
+    coarse:
+        proc [-ifx]
+        flatten    (if -flatten)
+        opt_expr -keepdc
+        opt_clean
+        check
+        opt -keepdc
+        wreduce [-memx]
+        memory_dff [-nordff]
+        memory_memx    (if -memx)
+        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]
+    proc [options] [selection]
+
+This pass calls all the other proc_* passes in the most common order.
+
+    proc_clean
+    proc_rmdead
+    proc_init
+    proc_arst
+    proc_mux
+    proc_dlatch
+    proc_dff
+    proc_clean
+
+This replaces the processes in the design with multiplexers,
+flip-flops and latches.
+
+The following options are supported:
+
+    -global_arst [!]<netname>
+        This option is passed through to proc_arst.
+
+    -ifx
+        This option is passed through to proc_mux. proc_rmdead is not
+        executed in -ifx mode.
+\end{lstlisting}
+
+\section{proc\_arst -- detect asynchronous resets}
+\label{cmd:proc_arst}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_arst [-global_arst [!]<netname>] [selection]
+
+This pass identifies asynchronous resets in the processes and converts them
+to a different internal representation that is suitable for generating
+flip-flop cells with asynchronous resets.
+
+    -global_arst [!]<netname>
+        In modules that have a net with the given name, use this net as async
+        reset for registers that have been assign initial values in their
+        declaration ('reg foobar = constant_value;'). Use the '!' modifier for
+        active low reset signals. Note: the frontend stores the default value
+        in the 'init' attribute on the net.
+\end{lstlisting}
+
+\section{proc\_clean -- remove empty parts of processes}
+\label{cmd:proc_clean}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_clean [selection]
+
+This pass removes empty parts of processes and ultimately removes a process
+if it contains only empty structures.
+\end{lstlisting}
+
+\section{proc\_dff -- extract flip-flops from processes}
+\label{cmd:proc_dff}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_dff [selection]
+
+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
+'initial' blocks) and sets the initial value to the 'init' attribute on the
+respective wire.
+\end{lstlisting}
+
+\section{proc\_mux -- convert decision trees to multiplexers}
+\label{cmd:proc_mux}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_mux [options] [selection]
+
+This pass converts the decision trees in processes (originating from if-else
+and case statements) to trees of multiplexer cells.
+
+    -ifx
+        Use Verilog simulation behavior with respect to undef values in
+        'case' expressions and 'if' conditions.
+\end{lstlisting}
+
+\section{proc\_rmdead -- eliminate dead trees in decision trees}
+\label{cmd:proc_rmdead}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_rmdead [selection]
+
+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.
+
+    -v
+        Verbose solver output for profiling or debugging
+
+Note: This implementation of a quadratic wirelength placer uses exact
+dense matrix operations. It is only a toy-placer for small circuits.
+\end{lstlisting}
+
+\section{read -- load HDL designs}
+\label{cmd:read}
+\begin{lstlisting}[numbers=left,frame=single]
+    read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..
+
+Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support
+is only available via Verific.)
+
+Additional -D<macro>[=<value>] options may be added after the option indicating
+the language version (and before file names) to set additional verilog defines.
+
+
+    read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..
+
+Load the specified VHDL files. (Requires Verific.)
+
+
+    read -define <macro>[=<value>]..
+
+Set global Verilog/SystemVerilog defines.
+
+
+    read -undef <macro>..
+
+Unset global Verilog/SystemVerilog defines.
+
+
+    read -incdir <directory>
+
+Add directory to global Verilog/SystemVerilog include directories.
+\end{lstlisting}
+
+\section{read\_blif -- read BLIF file}
+\label{cmd:read_blif}
+\begin{lstlisting}[numbers=left,frame=single]
+    read_blif [filename]
+
+Load modules from a BLIF file into the current design.
+
+    -sop
+        Create $sop cells instead of $lut cells
+
+    -wideports
+        Merge ports that match the pattern 'name[int]' into a single
+        multi-bit port 'name'.
+\end{lstlisting}
+
+\section{read\_ilang -- read modules from ilang file}
+\label{cmd:read_ilang}
+\begin{lstlisting}[numbers=left,frame=single]
+    read_ilang [filename]
+
+Load modules from an ilang file to the current design. (ilang is a text
+representation of a design in yosys's internal format.)
+\end{lstlisting}
+
+\section{read\_json -- read JSON file}
+\label{cmd:read_json}
+\begin{lstlisting}[numbers=left,frame=single]
+    read_json [filename]
+
+Load modules from a JSON file into the current design See "help write_json"
+for a description of the file format.
+\end{lstlisting}
+
+\section{read\_liberty -- read cells from liberty file}
+\label{cmd:read_liberty}
+\begin{lstlisting}[numbers=left,frame=single]
+    read_liberty [filename]
+
+Read cells from liberty file as modules into current design.
+
+    -lib
+        only create empty blackbox modules
+
+    -nooverwrite
+        ignore re-definitions of modules. (the default behavior is to
+        create an error message if the existing module is not a blackbox
+        module, and overwrite the existing module if it is  a blackbox module.)
+
+    -overwrite
+        overwrite existing modules with the same name
+
+    -ignore_miss_func
+        ignore cells with missing function specification of outputs
+
+    -ignore_miss_dir
+        ignore cells with a missing or invalid direction
+        specification on a pin
+
+    -ignore_miss_data_latch
+        ignore latches with missing data and/or enable pins
+
+    -setattr <attribute_name>
+        set the specified attribute (to the value 1) on all loaded modules
+\end{lstlisting}
+
+\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
+Verilog-2005 is supported.
+
+    -sv
+        enable support for SystemVerilog features. (only a small subset
+        of SystemVerilog is supported)
+
+    -formal
+        enable support for SystemVerilog assertions and some Yosys extensions
+        replace the implicit -D SYNTHESIS with -D FORMAL
+
+    -norestrict
+        ignore restrict() assertions
+
+    -assume-asserts
+        treat all assert() statements like assume() statements
+
+    -dump_ast1
+        dump abstract syntax tree (before simplification)
+
+    -dump_ast2
+        dump abstract syntax tree (after simplification)
+
+    -no_dump_ptr
+        do not include hex memory addresses in dump (easier to diff dumps)
+
+    -dump_vlog
+        dump ast as Verilog code (after simplification)
+
+    -dump_rtlil
+        dump generated RTLIL netlist
+
+    -yydebug
+        enable parser debug output
+
+    -nolatches
+        usually latches are synthesized into logic loops
         this option prohibits this and sets the output to 'x'
         in what would be the latches hold condition
 
-        this behavior can also be achieved by setting the
-        'nolatches' attribute on the respective module or
-        always block.
+        this behavior can also be achieved by setting the
+        'nolatches' attribute on the respective module or
+        always block.
+
+    -nomem2reg
+        under certain conditions memories are converted to registers
+        early during simplification to ensure correct handling of
+        complex corner cases. this option disables this behavior.
+
+        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
+
+    -nopp
+        do not run the pre-processor
+
+    -nodpi
+        disable DPI-C support
+
+    -lib
+        only create empty blackbox modules. This implies -DBLACKBOX.
+
+    -noopt
+        don't perform basic optimizations (such as const folding) in the
+        high-level front-end.
+
+    -icells
+        interpret cell types starting with '$' as internal cell types
+
+    -nooverwrite
+        ignore re-definitions of modules. (the default behavior is to
+        create an error message if the existing module is not a black box
+        module, and overwrite the existing module otherwise.)
+
+    -overwrite
+        overwrite existing modules with the same name
+
+    -defer
+        only read the abstract syntax tree and defer actual compilation
+        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
+
+    -Dname[=definition]
+        define the preprocessor symbol 'name' and set its optional value
+        'definition'
+
+    -Idir
+        add 'dir' to the directories which are used when searching include
+        files
+
+The command 'verilog_defaults' can be used to register default options for
+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
+the syntax of the code, rather than to rely on read_verilog for that.
+
+Depending on if read_verilog is run in -formal mode, either the macro
+SYNTHESIS or FORMAL is defined automatically. In addition, read_verilog
+always defines the macro YOSYS.
+
+See the Yosys README file for a list of non-standard Verilog features
+supported by the Yosys Verilog front-end.
+\end{lstlisting}
+
+\section{rename -- rename object in the design}
+\label{cmd:rename}
+\begin{lstlisting}[numbers=left,frame=single]
+    rename old_name new_name
+
+Rename the specified object. Note that selection patterns are not supported
+by this command.
+
+
+    rename -enumerate [-pattern <pattern>] [selection]
+
+Assign short auto-generated names to all selected wires and cells with private
+names. The -pattern option can be used to set the pattern for the new names.
+The character % in the pattern is replaced with a integer number. The default
+pattern is '_%_'.
+
+    rename -hide [selection]
+
+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{rmports -- remove module ports with no connections}
+\label{cmd:rmports}
+\begin{lstlisting}[numbers=left,frame=single]
+    rmports [selection]
+
+This pass identifies ports in the selected modules which are not used or
+driven and removes them.
+\end{lstlisting}
+
+\section{sat -- solve a SAT problem in the circuit}
+\label{cmd:sat}
+\begin{lstlisting}[numbers=left,frame=single]
+    sat [options] [selection]
+
+This command solves a SAT problem defined over the currently selected circuit
+and additional constraints passed as parameters.
+
+    -all
+        show all solutions to the problem (this can grow exponentially, use
+        -max <N> instead to get <N> solutions)
+
+    -max <N>
+        like -all, but limit number of solutions to <N>
+
+    -enable_undef
+        enable modeling of undef value (aka 'x-bits')
+        this option is implied by -set-def, -set-undef et. cetera
+
+    -max_undef
+        maximize the number of undef bits in solutions, giving a better
+        picture of which input bits are actually vital to the solution.
+
+    -set <signal> <value>
+        set the specified signal to the specified value.
+
+    -set-def <signal>
+        add a constraint that all bits of the given signal must be defined
+
+    -set-any-undef <signal>
+        add a constraint that at least one bit of the given signal is undefined
+
+    -set-all-undef <signal>
+        add a constraint that all bits of the given signal are undefined
+
+    -set-def-inputs
+        add -set-def constraints for all module inputs
+
+    -show <signal>
+        show the model for the specified signal. if no -show option is
+        passed then a set of signals to be shown is automatically selected.
+
+    -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
+
+    -ignore_unknown_cells
+        ignore all cells that can not be matched to a SAT model
+
+The following options can be used to set up a sequential problem:
+
+    -seq <N>
+        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>
+        add undef constraints in the given timestep.
+
+    -set-init <signal> <value>
+        set the initial value for the register driving the signal to the value
+
+    -set-init-undef
+        set all initial states (not set using -set-init) to undef
+
+    -set-init-def
+        do not force a value for the initial state but do not allow undef
+
+    -set-init-zero
+        set all initial states (not set using -set-init) to zero
+
+    -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.
+
+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 temporal induction proof it is
+        proven that the condition holds forever after the number of time steps
+        specified using -seq.
+
+    -tempinduct-def
+        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 equivalence checking.
+
+    -prove-asserts
+        Prove that all asserts in the design hold.
+
+    -prove-skip <N>
+        Do not enforce the prove-condition for the first <N> time steps.
+
+    -maxsteps <N>
+        Set a maximum length for the induction.
+
+    -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.
+
+    -verify
+        Return an error and stop the synthesis script if the proof fails.
+
+    -verify-no-timeout
+        Like -verify but do not return an error for timeouts.
+
+    -falsify
+        Return an error and stop the synthesis script if the proof succeeds.
+
+    -falsify-no-timeout
+        Like -falsify but do not return an error for timeouts.
+\end{lstlisting}
+
+\section{scatter -- add additional intermediate nets}
+\label{cmd:scatter}
+\begin{lstlisting}[numbers=left,frame=single]
+    scatter [selection]
+
+This command adds additional intermediate nets on all cell ports. This is used
+for testing the correct use of the SigMap helper in passes. If you don't know
+what this means: don't worry -- you only need this pass when testing your own
+extensions to Yosys.
+
+Use the opt_clean command to get rid of the additional nets.
+\end{lstlisting}
+
+\section{scc -- detect strongly connected components (logic loops)}
+\label{cmd:scc}
+\begin{lstlisting}[numbers=left,frame=single]
+    scc [options] [selection]
+
+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 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
+        this option set, all cells are considered. For unknown cells all ports
+        are assumed to be bidirectional 'inout' ports.
+
+    -set_attr <name> <value>
+        set the specified attribute on all cells that are part of a logic
+        loop. the special token {} in the value is replaced with a unique
+        identifier for the logic loop.
+
+    -select
+        replace the current selection with a selection of all cells and wires
+        that are part of a found logic loop
+\end{lstlisting}
+
+\section{script -- execute commands from script file}
+\label{cmd:script}
+\begin{lstlisting}[numbers=left,frame=single]
+    script <filename> [<from_label>:<to_label>]
+
+This command executes the yosys commands in the specified file.
+
+The 2nd argument can be used to only execute the section of the
+file between the specified labels. An empty from label is synonymous
+for the beginning of the file and an empty to label is synonymous
+for the end of the file.
+
+If only one label is specified (without ':') then only the block
+marked with that label (until the next label) is executed.
+\end{lstlisting}
+
+\section{select -- modify and view the list of selected objects}
+\label{cmd:select}
+\begin{lstlisting}[numbers=left,frame=single]
+    select [ -add | -del | -set <name> ] {-read <filename> | <selection>}
+    select [ <assert_option> ] {-read <filename> | <selection>}
+    select [ -list | -write <filename> | -count | -clear ]
+    select -module <modname>
+
+Most commands use the list of currently selected objects to determine which part
+of the design to operate on. This command can be used to modify and view this
+list of selected objects.
+
+Note that many commands support an optional [selection] argument that can be
+used to YS_OVERRIDE the global selection for the command. The syntax of this
+optional argument is identical to the syntax of the <selection> argument
+described here.
+
+    -add, -del
+        add or remove the given objects to the current selection.
+        without this options the current selection is replaced.
+
+    -set <name>
+        do not modify the current selection. instead save the new selection
+        under the given name (see @<name> below). to save the current selection,
+        use "select -set <name> %"
+
+    -assert-none
+        do not modify the current selection. instead assert that the given
+        selection is empty. i.e. produce an error if any object matching the
+        selection is found.
+
+    -assert-any
+        do not modify the current selection. instead assert that the given
+        selection is non-empty. i.e. produce an error if no object matching
+        the selection is found.
+
+    -assert-count N
+        do not modify the current selection. instead assert that the given
+        selection contains exactly N objects.
+
+    -assert-max N
+        do not modify the current selection. instead assert that the given
+        selection contains less than or exactly N objects.
+
+    -assert-min N
+        do not modify the current selection. instead assert that the given
+        selection contains at least N objects.
+
+    -list
+        list all objects in the current selection
+
+    -write <filename>
+        like -list but write the output to the specified file
+
+    -read <filename>
+        read the specified file (written by -write)
+
+    -count
+        count all objects in the current selection
+
+    -clear
+        clear the current selection. this effectively selects the whole
+        design. it also resets the selected module (see -module). use the
+        command 'select *' to select everything but stay in the current module.
+
+    -none
+        create an empty selection. the current module is unchanged.
+
+    -module <modname>
+        limit the current scope to the specified module.
+        the difference between this and simply selecting the module
+        is that all object names are interpreted relative to this
+        module after this command until the selection is cleared again.
+
+When this command is called without an argument, the current selection
+is displayed in a compact form (i.e. only the module name when a whole module
+is selected).
+
+The <selection> argument itself is a series of commands for a simple stack
+machine. Each element on the stack represents a set of selected objects.
+After this commands have been executed, the union of all remaining sets
+on the stack is computed and used as selection for the command.
+
+Pushing (selecting) object when not in -module mode:
+
+    <mod_pattern>
+        select the specified module(s)
+
+    <mod_pattern>/<obj_pattern>
+        select the specified object(s) from the module(s)
+
+Pushing (selecting) object when in -module mode:
+
+    <obj_pattern>
+        select the specified object(s) from the current module
+
+A <mod_pattern> can be a module name, wildcard expression (*, ?, [..])
+matching module names, or one of the following:
+
+    A:<pattern>, A:<pattern>=<pattern>
+        all modules with an attribute matching the given pattern
+        in addition to = also <, <=, >=, and > are supported
+
+An <obj_pattern> can be an object name, wildcard expression, or one of
+the following:
+
+    w:<pattern>
+        all wires with a name matching the given wildcard pattern
+
+    i:<pattern>, o:<pattern>, x:<pattern>
+        all inputs (i:), outputs (o:) or any ports (x:) with matching names
+
+    s:<size>, s:<min>:<max>
+        all wires with a matching width
+
+    m:<pattern>
+        all memories with a name matching the given pattern
+
+    c:<pattern>
+        all cells with a name matching the given pattern
+
+    t:<pattern>
+        all cells with a type matching the given pattern
+
+    p:<pattern>
+        all processes with a name matching the given pattern
+
+    a:<pattern>
+        all objects with an attribute name matching the given pattern
+
+    a:<pattern>=<pattern>
+        all objects with a matching attribute name-value-pair.
+        in addition to = also <, <=, >=, and > are supported
+
+    r:<pattern>, r:<pattern>=<pattern>
+        cells with matching parameters. also with <, <=, >= and >.
+
+    n:<pattern>
+        all objects with a name matching the given pattern
+        (i.e. 'n:' is optional as it is the default matching rule)
+
+    @<name>
+        push the selection saved prior with 'select -set <name> ...'
+
+The following actions can be performed on the top sets on the stack:
+
+    %
+        push a copy of the current selection to the stack
+
+    %%
+        replace the stack with a union of all elements on it
+
+    %n
+        replace top set with its invert
+
+    %u
+        replace the two top sets on the stack with their union
+
+    %i
+        replace the two top sets on the stack with their intersection
+
+    %d
+        pop the top set from the stack and subtract it from the new top
+
+    %D
+        like %d but swap the roles of two top sets on the stack
+
+    %c
+        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.
+        (i.e. select all cells connected to selected wires and select all
+        wires connected to selected cells) The rules specify which cell
+        ports to use for this. the syntax for a rule is a '-' for exclusion
+        and a '+' for inclusion, followed by an optional comma separated
+        list of cell types followed by an optional comma separated list of
+        cell ports in square brackets. a rule can also be just a cell or wire
+        name that limits the expansion (is included but does not go beyond).
+        select at most <num2> objects. a warning message is printed when this
+        limit is reached. When '*' is used instead of <num1> then the process
+        is repeated until no further object are selected.
+
+    %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]]
+    %co[<num1>|*][.<num2>][:<rule>[:<rule>..]]
+        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 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:
+
+    select */t:SWITCH %x:+[GATE] */t:SWITCH %d
+\end{lstlisting}
+
+\section{setattr -- set/unset attributes on objects}
+\label{cmd:setattr}
+\begin{lstlisting}[numbers=left,frame=single]
+    setattr [ -mod ] [ -set name value | -unset name ]... [selection]
+
+Set/unset the given attributes on the selected objects. String values must be
+passed in double quotes (").
+
+When called with -mod, this command will set and unset attributes on modules
+instead of objects within modules.
+\end{lstlisting}
+
+\section{setparam -- set/unset parameters on objects}
+\label{cmd:setparam}
+\begin{lstlisting}[numbers=left,frame=single]
+    setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection]
+
+Set/unset the given parameters on the selected cells. String values must be
+passed in double quotes (").
+
+The -type option can be used to change the cell type of the selected cells.
+\end{lstlisting}
+
+\section{setundef -- replace undef values with defined constants}
+\label{cmd:setundef}
+\begin{lstlisting}[numbers=left,frame=single]
+    setundef [options] [selection]
+
+This command replaces undef (x) constants with defined (0/1) constants.
+
+    -undriven
+        also set undriven nets to constant values
+
+    -expose
+        also expose undriven nets as inputs (use with -undriven)
+
+    -zero
+        replace with bits cleared (0)
+
+    -one
+        replace with bits set (1)
+
+    -undef
+        replace with undef (x) bits, may be used with -undriven
+
+    -anyseq
+        replace with $anyseq drivers (for formal)
+
+    -anyconst
+        replace with $anyconst drivers (for formal)
+
+    -random <seed>
+        replace with random bits using the specified integer als seed
+        value for the random number generator.
+
+    -init
+        also create/update init values for flip-flops
+\end{lstlisting}
+
+\section{share -- perform sat-based resource sharing}
+\label{cmd:share}
+\begin{lstlisting}[numbers=left,frame=single]
+    share [options] [selection]
+
+This pass merges shareable resources into a single resource. A SAT solver
+is used to determine if two resources are share-able.
+
+  -force
+    Per default the selection of cells that is considered for sharing is
+    narrowed using a list of cell types. With this option all selected
+    cells are considered for resource sharing.
+
+    IMPORTANT NOTE: If the -all option is used then no cells with internal
+    state must be selected!
+
+  -aggressive
+    Per default some heuristics are used to reduce the number of cells
+    considered for resource sharing to only large resources. This options
+    turns this heuristics off, resulting in much more cells being considered
+    for resource sharing.
+
+  -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 opportunities
+    for resource sharing.
+
+  -limit N
+    Only perform the first N merges, then stop. This is useful for debugging.
+\end{lstlisting}
+
+\section{shell -- enter interactive command mode}
+\label{cmd:shell}
+\begin{lstlisting}[numbers=left,frame=single]
+    shell
+
+This command enters the interactive command mode. This can be useful
+in a script to interrupt the script at a certain point and allow for
+interactive inspection or manual synthesis of the design at this point.
+
+The command prompt of the interactive shell indicates the current
+selection (see 'help select'):
+
+    yosys>
+        the entire design is selected
+
+    yosys*>
+        only part of the design is selected
+
+    yosys [modname]>
+        the entire module 'modname' is selected using 'select -module modname'
+
+    yosys [modname]*>
+        only part of current module 'modname' is selected
+
+When in interactive shell, some errors (e.g. invalid command arguments)
+do not terminate yosys but return to the command prompt.
+
+This command is the default action if nothing else has been specified
+on the command line.
+
+Press Ctrl-D or type 'exit' to leave the interactive shell.
+\end{lstlisting}
+
+\section{show -- generate schematics using graphviz}
+\label{cmd:show}
+\begin{lstlisting}[numbers=left,frame=single]
+    show [options] [selection]
+
+Create a graphviz DOT file for the selected part of the design and compile it
+to a graphics file (usually SVG or PostScript).
+
+    -viewer <viewer>
+        Run the specified command with the graphics file as parameter.
+        On Windows, this pauses yosys until the viewer exits.
+
+    -format <format>
+        Generate a graphics file in the specified format. Use 'dot' to just
+        generate a .dot file, or other <format> strings such as 'svg' or 'ps'
+        to generate files in other formats (this calls the 'dot' command).
+
+    -lib <verilog_or_ilang_file>
+        Use the specified library file for determining whether cell ports are
+        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.*
+
+    -color <color> <object>
+        assign the specified color to the specified object. The object can be
+        a single selection wildcard expressions or a saved set of objects in
+        the @<name> syntax (see "help select" for details).
+
+    -label <text> <object>
+        assign the specified label text to the specified object. The object can
+        be a single selection wildcard expressions or a saved set of objects in
+        the @<name> syntax (see "help select" for details).
+
+    -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 ambiguous. A seed of zero deactivates the coloring.
+
+    -colorattr <attribute_name>
+        Use the specified attribute to assign colors. A unique color is
+        assigned to each unique value of this attribute.
+
+    -width
+        annotate busses with a label indicating the width of the bus.
+
+    -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
+        stretch the graph so all inputs are on the left side and all outputs
+        (including inout ports) are on the right side.
+
+    -pause
+        wait for the use to press enter to before returning
+
+    -enum
+        enumerate objects with internal ($-prefixed) names
+
+    -long
+        do not abbreviate objects with internal ($-prefixed) names
+
+    -notitle
+        do not add the module name as graph title to the dot file
+
+When no <format> is specified, 'dot' is used. When no <format> and <viewer> is
+specified, 'xdot' is used to display the schematic (POSIX systems only).
+
+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 each time
+the 'show' command is executed.
+\end{lstlisting}
+
+\section{shregmap -- map shift registers}
+\label{cmd:shregmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    shregmap [options] [selection]
+
+This pass converts chains of $_DFF_[NP]_ gates to target specific shift register
+primitives. The generated shift register will be of type $__SHREG_DFF_[NP]_ and
+will use the same interface as the original $_DFF_*_ cells. The cell parameter
+'DEPTH' will contain the depth of the shift register. Use a target-specific
+'techmap' map file to convert those cells to the actual target cells.
+
+    -minlen N
+        minimum length of shift register (default = 2)
+        (this is the length after -keep_before and -keep_after)
+
+    -maxlen N
+        maximum length of shift register (default = no limit)
+        larger chains will be mapped to multiple shift register instances
+
+    -keep_before N
+        number of DFFs to keep before the shift register (default = 0)
+
+    -keep_after N
+        number of DFFs to keep after the shift register (default = 0)
+
+    -clkpol pos|neg|any
+        limit match to only positive or negative edge clocks. (default = any)
+
+    -enpol pos|neg|none|any_or_none|any
+        limit match to FFs with the specified enable polarity. (default = none)
+
+    -match <cell_type>[:<d_port_name>:<q_port_name>]
+        match the specified cells instead of $_DFF_N_ and $_DFF_P_. If
+        ':<d_port_name>:<q_port_name>' is omitted then 'D' and 'Q' is used
+        by default. E.g. the option '-clkpol pos' is just an alias for
+        '-match $_DFF_P_', which is an alias for '-match $_DFF_P_:D:Q'.
+
+    -params
+        instead of encoding the clock and enable polarity in the cell name by
+        deriving from the original cell name, simply name all generated cells
+        $__SHREG_ and use CLKPOL and ENPOL parameters. An ENPOL value of 2 is
+        used to denote cells without enable input. The ENPOL parameter is
+        omitted when '-enpol none' (or no -enpol option) is passed.
+
+    -zinit
+        assume the shift register is automatically zero-initialized, so it
+        becomes legal to merge zero initialized FFs into the shift register.
+
+    -init
+        map initialized registers to the shift reg, add an INIT parameter to
+        generated cells with the initialization value. (first bit to shift out
+        in LSB position)
+
+    -tech greenpak4
+        map to greenpak4 shift registers.
+\end{lstlisting}
+
+\section{sim -- simulate the circuit}
+\label{cmd:sim}
+\begin{lstlisting}[numbers=left,frame=single]
+    sim [options] [top-level]
+
+This command simulates the circuit using the given top-level module.
+
+    -vcd <filename>
+        write the simulation results to the given VCD file
+
+    -clock <portname>
+        name of top-level clock input
+
+    -clockn <portname>
+        name of top-level clock input (inverse polarity)
+
+    -reset <portname>
+        name of top-level reset input (active high)
+
+    -resetn <portname>
+        name of top-level inverted reset input (active low)
+
+    -rstlen <integer>
+        number of cycles reset should stay active (default: 1)
+
+    -zinit
+        zero-initialize all uninitialized regs and memories
+
+    -n <integer>
+        number of cycles to simulate (default: 20)
+
+    -a
+        include all nets in VCD output, not just those with public names
+
+    -w
+        writeback mode: use final simulation state as new init state
+
+    -d
+        enable debug output
+\end{lstlisting}
+
+\section{simplemap -- mapping simple coarse-grain cells}
+\label{cmd:simplemap}
+\begin{lstlisting}[numbers=left,frame=single]
+    simplemap [selection]
+
+This pass maps a small selection of simple coarse-grain cells to yosys gate
+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, $tribuf
+  $sr, $ff, $dff, $dffsr, $adff, $dlatch
+\end{lstlisting}
+
+\section{splice -- create explicit splicing cells}
+\label{cmd:splice}
+\begin{lstlisting}[numbers=left,frame=single]
+    splice [options] [selection]
+
+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 dedicated hardware is needed to splice signals.
+
+    -sel_by_cell
+        only select the cell ports to rewire by the cell. if the selection
+        contains a cell, than all cell inputs are rewired, if necessary.
+
+    -sel_by_wire
+        only select the cell ports to rewire by the wire. if the selection
+        contains a wire, than all cell ports driven by this wire are wired,
+        if necessary.
+
+    -sel_any_bit
+        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.
+
+    -port <name>
+        only rewire cell ports with the specified name. can be used multiple
+        times. implies -no_output.
+
+    -no_port <name>
+        do not rewire cell ports with the specified name. can be used multiple
+        times. can not be combined with -port <name>.
+
+By default selected output wires and all cell ports of selected cells driven
+by selected wires are rewired.
+\end{lstlisting}
+
+\section{splitnets -- split up multi-bit nets}
+\label{cmd:splitnets}
+\begin{lstlisting}[numbers=left,frame=single]
+    splitnets [options] [selection]
+
+This command splits multi-bit nets into single-bit nets.
+
+    -format char1[char2[char3]]
+        the first char is inserted between the net name and the bit index, the
+        second char is appended to the netname. e.g. -format () creates net
+        names like 'mysignal(42)'. the 3rd character is the range separation
+        character when creating multi-bit wires. the default is '[]:'.
+
+    -ports
+        also split module ports. per default only internal signals are split.
+
+    -driver
+        don't blindly split nets in individual bits. instead look at the driver
+        and split nets so that no driver drives only part of a net.
+\end{lstlisting}
+
+\section{stat -- print some statistics}
+\label{cmd:stat}
+\begin{lstlisting}[numbers=left,frame=single]
+    stat [options] [selection]
+
+Print some statistics (number of objects) on the selected portion of the
+design.
+
+    -top <module>
+        print design hierarchy with this module as top. if the design is fully
+        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.
+\end{lstlisting}
+
+\section{submod -- moving part of a module to a new submodule}
+\label{cmd:submod}
+\begin{lstlisting}[numbers=left,frame=single]
+    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
+cell that replaces the group of cells with the same attribute value.
+
+This pass can be used to create a design hierarchy in flat design. This can
+be useful for analyzing or reverse-engineering a design.
+
+This pass only operates on completely selected modules with no processes
+or memories.
+
 
-    -nomem2reg
-        under certain conditions memories are converted to registers
-        early during simplification to ensure correct handling of
-        complex corner cases. this option disables this behavior.
+    submod -name <name> [-copy] [selection]
 
-        this can also be achieved by setting the 'nomem2reg'
-        attribute on the respective module or register.
+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.
 
-    -mem2reg
-        always convert memories to registers. this can also be
-        achieved by setting the 'mem2reg' attribute on the respective
-        module or register.
+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}
 
-    -ppdump
-        dump verilog code after pre-processor
+\section{synth -- generic synthesis script}
+\label{cmd:synth}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth [options]
 
-    -nopp
-        do not run the pre-processor
+This command runs the default synthesis script. This command does not operate
+on partly selected designs.
 
-    -lib
-        only create empty blackbox modules
+    -top <module>
+        use the specified module as top module (default='top')
 
-    -noopt
-        don't perform basic optimizations (such as const folding) in the
-        high-level front-end.
+    -auto-top
+        automatically determine the top of the design hierarchy
 
-    -Dname[=definition]
-        define the preprocessor symbol 'name' and set its optional value
-        'definition'
+    -flatten
+        flatten the design before synthesis. this will pass '-auto-top' to
+        'hierarchy' if no top module is specified.
 
-    -Idir
-        add 'dir' to the directories which are used when searching include
-        files
+    -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
+
+    -noshare
+        do not run SAT-based resource sharing
+
+    -run <from_label>[:<to_label>]
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        hierarchy -check [-top <top> | -auto-top]
+
+    coarse:
+        proc
+        flatten    (if -flatten)
+        opt_expr
+        opt_clean
+        check
+        opt
+        wreduce
+        alumacc
+        share
+        opt
+        fsm
+        opt -fast
+        memory -nomap
+        opt_clean
+
+    fine:
+        opt -fast -full
+        memory_map
+        opt -full
+        techmap
+        opt -fast
+        abc -fast
+        opt -fast
+
+    check:
+        hierarchy -check
+        stat
+        check
 \end{lstlisting}
 
-\section{rename -- rename object in the design}
-\label{cmd:rename}
+\section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.}
+\label{cmd:synth_achronix}
 \begin{lstlisting}[numbers=left,frame=single]
-    rename old_name new_name
+    synth_achronix [options]
 
-Rename the specified object. Note that selection patterns are not supported
-by this command.
+This command runs synthesis for Achronix Speedster eFPGAs. This work is still experimental.
 
+    -top <module>
+        use the specified module as top module (default='top')
 
-    rename -enumerate [selection]
+    -vout <file>
+        write the design to the specified Verilog netlist file. writing of an
+        output file is omitted if this parameter is not specified.
 
-Assign short auto-generated names to all selected wires and cells with private
-names.
+    -run <from_label>:<to_label>
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+    -noflatten
+        do not flatten design before synthesis
+
+    -retime
+        run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        read_verilog -sv -lib +/achronix/speedster22i/cells_sim.v
+        hierarchy -check -top <top>
+
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
+        deminout
+
+    coarse:
+        synth -run coarse
+
+    fine:
+        opt -fast -mux_undef -undriven -fine -full
+        memory_map
+        opt -undriven -fine
+        dffsr2dff
+        dff2dffe -direct-match $_DFF_*
+        opt -fine
+        techmap -map +/techmap.v
+        opt -full
+        clean -purge
+        setundef -undriven -zero
+        abc -markgroups -dff    (only if -retime)
+
+    map_luts:
+        abc -lut 4
+        clean
+
+    map_cells:
+        iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I
+        techmap -map +/achronix/speedster22i/cells_map.v
+        clean -purge
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    vout:
+        write_verilog -nodec -attr2comment -defparam -renameprefix syn_ <file-name>
 \end{lstlisting}
 
-\section{sat -- solve a SAT problem in the circuit}
-\label{cmd:sat}
+\section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs}
+\label{cmd:synth_coolrunner2}
 \begin{lstlisting}[numbers=left,frame=single]
-    sat [options] [selection]
+    synth_coolrunner2 [options]
 
-This command solves a SAT problem defined over the currently selected circuit
-and additional constraints passed as parameters.
+This command runs synthesis for Coolrunner-II CPLDs. This work is experimental.
+It is intended to be used with https://github.com/azonenberg/openfpga as the
+place-and-route.
 
-    -all
-        show all solutions to the problem (this can grow exponentially, use
-        -max <N> instead to get <N> solutions)
+    -top <module>
+        use the specified module as top module (default='top')
 
-    -max <N>
-        like -all, but limit number of solutions to <N>
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    -set <signal> <value>
-        set the specified signal to the specified value.
+    -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.
 
-    -show <signal>
-        show the model for the specified signal. if no -show option is
-        passed then a set of signals to be shown is automatically selected.
+    -noflatten
+        do not flatten design before synthesis
 
-    -ignore_div_by_zero
-        ignore all solutions that involve a division by zero
+    -retime
+        run 'abc' with -dff option
 
-The following options can be used to set up a sequential problem:
 
-    -seq <N>
-        set up a sequential problem with <N> time steps. The steps will
-        be numbered from 1 to N.
+The following commands are executed by this synthesis command:
 
-    -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.
+    begin:
+        read_verilog -lib +/coolrunner2/cells_sim.v
+        hierarchy -check -top <top>
 
-The following additional options can be used to set up a proof. If also -seq
-is passed, a temporal induction proof is performed.
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
 
-    -prove <signal> <value>
-        Attempt to proof that <signal> is always <value>. In a temporal
-        induction proof it is proven that the condition holds forever after
-        the number of time steps passed using -seq.
+    coarse:
+        synth -run coarse
 
-    -maxsteps <N>
-        Set a maximum length for the induction.
+    fine:
+        opt -fast -full
+        techmap
+        techmap -map +/coolrunner2/cells_latch.v
+        dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib
 
-    -timeout <N>
-        Maximum number of seconds a single SAT instance may take.
+    map_tff:
+        abc -g AND,XOR
+        clean
+        extract -map +/coolrunner2/tff_extract.v
 
-    -verify
-        Return an error and stop the synthesis script if the proof fails.
+    map_pla:
+        abc -sop -I 40 -P 56
+        clean
 
-    -verify-no-timeout
-        Like -verify but do not return an error for timeouts.
+    map_cells:
+        dfflibmap -liberty +/coolrunner2/xc2_dff.lib
+        dffinit -ff FDCP Q INIT
+        dffinit -ff FDCP_N Q INIT
+        dffinit -ff FTCP Q INIT
+        dffinit -ff FTCP_N Q INIT
+        dffinit -ff LDCP Q INIT
+        dffinit -ff LDCP_N Q INIT
+        coolrunner2_sop
+        iopadmap -bits -inpad IBUF O:I -outpad IOBUFE I:IO -inoutpad IOBUFE O:IO -toutpad IOBUFE E:I:IO -tinoutpad IOBUFE E:O:I:IO
+        attrmvcp -attr src -attr LOC t:IOBUFE n:*
+        attrmvcp -attr src -attr LOC -driven t:IBUF n:*
+        splitnets
+        clean
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    json:
+        write_json <file-name>
 \end{lstlisting}
 
-\section{scatter -- add additional intermediate nets}
-\label{cmd:scatter}
+\section{synth\_easic -- synthesis for eASIC platform}
+\label{cmd:synth_easic}
 \begin{lstlisting}[numbers=left,frame=single]
-    scatter [selection]
+    synth_easic [options]
 
-This command adds additional intermediate nets on all cell ports. This is used
-for testing the correct use of the SigMap helper in passes. If you don't know
-what this means: don't worry -- you only need this pass when testing your own
-extensions to Yosys.
+This command runs synthesis for eASIC platform.
 
-Use the opt_clean command to get rid of the additional nets.
+    -top <module>
+        use the specified module as top module
+
+    -vlog <file>
+        write the design to the specified structural Verilog file. writing of
+        an output file is omitted if this parameter is not specified.
+
+    -etools <path>
+        set path to the eTools installation. (default=/opt/eTools)
+
+    -run <from_label>:<to_label>
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+    -noflatten
+        do not flatten design before synthesis
+
+    -retime
+        run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        read_liberty -lib <etools_phys_clk_lib>
+        read_liberty -lib <etools_logic_lut_lib>
+        hierarchy -check -top <top>
+
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+
+    coarse:
+        synth -run coarse
+
+    fine:
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+        techmap
+        opt -fast
+        abc -dff     (only if -retime)
+        opt_clean    (only if -retime)
+
+    map:
+        dfflibmap -liberty <etools_phys_clk_lib>
+        abc -liberty <etools_logic_lut_lib>
+        opt_clean
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    vlog:
+        write_verilog -noexpr -attr2comment <file-name>
 \end{lstlisting}
 
-\section{scc -- detect strongly connected components (logic loops)}
-\label{cmd:scc}
+\section{synth\_ecp5 -- synthesis for ECP5 FPGAs}
+\label{cmd:synth_ecp5}
 \begin{lstlisting}[numbers=left,frame=single]
-    scc [options] [selection]
+    synth_ecp5 [options]
 
-This command identifies strongly connected components (aka logic loops) in the
-design.
+This command runs synthesis for ECP5 FPGAs.
 
-    -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.
+    -top <module>
+        use the specified module as top module
 
-    -all_cell_types
-        Usually this command only considers internal non-memory cells. With
-        this option set, all cells are considered. For unkown cells all ports
-        are assumed to be bidirectional 'inout' ports.
+    -blif <file>
+        write the design to the specified BLIF file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    -set_attr <name> <value>
-    -set_cell_attr <name> <value>
-    -set_wire_attr <name> <value>
-        set the specified attribute on all cells and/or wires that are part of
-        a logic loop. the special token {} in the value is replaced with a
-        unique identifier for the logic loop.
+    -edif <file>
+        write the design to the specified EDIF file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    -select
-        replace the current selection with a selection of all cells and wires
-        that are part of a found logic loop
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
+        is omitted if this parameter is not specified.
+
+    -run <from_label>:<to_label>
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+    -noflatten
+        do not flatten design before synthesis
+
+    -retime
+        run 'abc' with -dff option
+
+    -noccu2
+        do not use CCU2 cells in output netlist
+
+    -nodffe
+        do not use flipflops with CE in output netlist
+
+    -nobram
+        do not use BRAM cells in output netlist
+
+    -nodram
+        do not use distributed RAM cells in output netlist
+
+    -nomux
+        do not use PFU muxes to implement LUTs larger than LUT4s
+
+    -abc2
+        run two passes of 'abc' for slightly improved logic density
+
+    -vpr
+        generate an output netlist (and BLIF file) suitable for VPR
+        (this feature is experimental and incomplete)
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        read_verilog -lib +/ecp5/cells_sim.v
+        hierarchy -check -top <top>
+
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
+        deminout
+
+    coarse:
+        synth -run coarse
+
+    bram:    (skip if -nobram)
+
+    dram:    (skip if -nodram)
+        memory_bram -rules +/ecp5/dram.txt
+        techmap -map +/ecp5/drams_map.v
+
+    fine:
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+        techmap -map +/techmap.v -map +/ecp5/arith_map.v
+        abc -dff    (only if -retime)
+
+    map_ffs:
+        dffsr2dff
+        dff2dffs
+        opt_clean
+        dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
+        techmap -D NO_LUT -map +/ecp5/cells_map.v
+        opt_expr -mux_undef
+        simplemap
+
+    map_luts:
+        abc          (only if -abc2)
+        abc -lut 4:7
+        clean
+
+    map_cells:
+        techmap -map +/ecp5/cells_map.v    (with -D NO_LUT in vpr mode)
+        clean
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    blif:
+        opt_clean -purge                                     (vpr mode)
+        write_blif -attr -cname -conn -param <file-name>     (vpr mode)
+        write_blif -gates -attr -param <file-name>           (non-vpr mode)
+
+    edif:
+        write_edif <file-name>
+
+    json:
+        write_json <file-name>
 \end{lstlisting}
 
-\section{script -- execute commands from script file}
-\label{cmd:script}
-\begin{lstlisting}[numbers=left,frame=single]
-    script <filename>
+\section{synth\_gowin -- synthesis for Gowin FPGAs}
+\label{cmd:synth_gowin}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_gowin [options]
+
+This command runs synthesis for Gowin FPGAs. This work is experimental.
+
+    -top <module>
+        use the specified module as top module (default='top')
+
+    -vout <file>
+        write the design to the specified Verilog netlist file. writing of an
+        output file is omitted if this parameter is not specified.
+
+    -run <from_label>:<to_label>
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+    -retime
+        run 'abc' with -dff option
 
-This command executes the yosys commands in the specified file.
-\end{lstlisting}
 
-\section{select -- modify and view the list of selected objects}
-\label{cmd:select}
-\begin{lstlisting}[numbers=left,frame=single]
-    select [ -add | -del | -set <name> ] <selection>
-    select [ -list | -write <filename> | -count | -clear ]
-    select -module <modname>
+The following commands are executed by this synthesis command:
 
-Most commands use the list of currently selected objects to determine which part
-of the design to operate on. This command can be used to modify and view this
-list of selected objects.
+    begin:
+        read_verilog -lib +/gowin/cells_sim.v
+        hierarchy -check -top <top>
 
-Note that many commands support an optional [selection] argument that can be
-used to override the global selection for the command. The syntax of this
-optional argument is identical to the syntax of the <selection> argument
-described here.
+    flatten:
+        proc
+        flatten
+        tribuf -logic
+        deminout
 
-    -add, -del
-        add or remove the given objects to the current selection.
-        without this options the current selection is replaced.
+    coarse:
+        synth -run coarse
 
-    -set <name>
-        do not modify the current selection. instead save the new selection
-        under the given name (see @<name> below).
+    fine:
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+        techmap
+        clean -purge
+        splitnets -ports
+        setundef -undriven -zero
+        abc -dff    (only if -retime)
 
-    -list
-        list all objects in the current selection
+    map_luts:
+        abc -lut 4
+        clean
 
-    -write <filename>
-        like -list but write the output to the specified file
+    map_cells:
+        techmap -map +/gowin/cells_map.v
+        hilomap -hicell VCC V -locell GND G
+        iopadmap -inpad IBUF O:I -outpad OBUF I:O
+        clean -purge
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    vout:
+        write_verilog -nodec -attr2comment -defparam -renameprefix gen <file-name>
+\end{lstlisting}
 
-    -count
-        count all objects in the current selection
+\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs}
+\label{cmd:synth_greenpak4}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_greenpak4 [options]
 
-    -clear
-        clear the current selection. this effectively selects the
-        whole design.
+This command runs synthesis for GreenPAK4 FPGAs. This work is experimental.
+It is intended to be used with https://github.com/azonenberg/openfpga as the
+place-and-route.
 
-    -module <modname>
-        limit the current scope to the specified module.
-        the difference between this and simply selecting the module
-        is that all object names are interpreted relative to this
-        module after this command until the selection is cleared again.
+    -top <module>
+        use the specified module as top module (default='top')
 
-When this command is called without an argument, the current selection
-is displayed in a compact form (i.e. only the module name when a whole module
-is selected).
+    -part <part>
+        synthesize for the specified part. Valid values are SLG46140V,
+        SLG46620V, and SLG46621V (default).
 
-The <selection> argument itself is a series of commands for a simple stack
-machine. Each element on the stack represents a set of selected objects.
-After this commands have been executed, the union of all remaining sets
-on the stack is computed and used as selection for the command.
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
+        is omitted if this parameter is not specified.
 
-Pushing (selecting) object when not in -module mode:
+    -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.
 
-    <mod_pattern>
-        select the specified module(s)
+    -noflatten
+        do not flatten design before synthesis
 
-    <mod_pattern>/<obj_pattern>
-        select the specified object(s) from the module(s)
+    -retime
+        run 'abc' with -dff option
 
-Pushing (selecting) object when in -module mode:
 
-    <obj_pattern>
-        select the specified object(s) from the current module
+The following commands are executed by this synthesis command:
 
-A <mod_pattern> can be a module name or wildcard expression (*, ?, [..])
-matching module names.
+    begin:
+        read_verilog -lib +/greenpak4/cells_sim.v
+        hierarchy -check -top <top>
 
-An <obj_pattern> can be an object name, wildcard expression, or one of
-the following:
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
 
-    w:<pattern>
-        all wires with a name matching the given wildcard pattern
+    coarse:
+        synth -run coarse
 
-    m:<pattern>
-        all memories with a name matching the given pattern
+    fine:
+        extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14
+        clean
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+        techmap
+        techmap -map +/greenpak4/cells_latch.v
+        dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib
+        opt -fast
+        abc -dff    (only if -retime)
 
-    c:<pattern>
-        all cells with a name matching the given pattern
+    map_luts:
+        nlutmap -assert -luts 0,6,8,2     (for -part SLG46140V)
+        nlutmap -assert -luts 2,8,16,2    (for -part SLG46620V)
+        nlutmap -assert -luts 2,8,16,2    (for -part SLG46621V)
+        clean
 
-    t:<pattern>
-        all cells with a type matching the given pattern
+    map_cells:
+        shregmap -tech greenpak4
+        dfflibmap -liberty +/greenpak4/gp_dff.lib
+        dffinit -ff GP_DFF Q INIT
+        dffinit -ff GP_DFFR Q INIT
+        dffinit -ff GP_DFFS Q INIT
+        dffinit -ff GP_DFFSR Q INIT
+        iopadmap -bits -inpad GP_IBUF OUT:IN -outpad GP_OBUF IN:OUT -inoutpad GP_OBUF OUT:IN -toutpad GP_OBUFT OE:IN:OUT -tinoutpad GP_IOBUF OE:OUT:IN:IO
+        attrmvcp -attr src -attr LOC t:GP_OBUF t:GP_OBUFT t:GP_IOBUF n:*
+        attrmvcp -attr src -attr LOC -driven t:GP_IBUF n:*
+        techmap -map +/greenpak4/cells_map.v
+        greenpak4_dffinv
+        clean
 
-    p:<pattern>
-        all processes with a name matching the given pattern
+    check:
+        hierarchy -check
+        stat
+        check -noinit
 
-    a:<pattern>
-        all objects with an attribute name matching the given pattern
+    json:
+        write_json <file-name>
+\end{lstlisting}
 
-    a:<pattern>=<pattern>
-        all objects with a matching attribute name-value-pair
+\section{synth\_ice40 -- synthesis for iCE40 FPGAs}
+\label{cmd:synth_ice40}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_ice40 [options]
 
-    n:<pattern>
-        all objects with a name matching the given pattern
-        (i.e. 'n:' is optional as it is the default matching rule)
+This command runs synthesis for iCE40 FPGAs.
 
-    @<name>
-        push the selection saved prior with 'select -set <name> ...'
+    -top <module>
+        use the specified module as top module
 
-The following actions can be performed on the top sets on the stack:
+    -blif <file>
+        write the design to the specified BLIF file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    %
-        push a copy of the current selection to the stack
+    -edif <file>
+        write the design to the specified EDIF file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    %%
-        replace the stack with a union of all elements on it
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
+        is omitted if this parameter is not specified.
 
-    %n
-        replace top set with its invert
+    -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.
 
-    %u
-        replace the two top sets on the stack with their union
+    -noflatten
+        do not flatten design before synthesis
 
-    %i
-        replace the two top sets on the stack with their intersection
+    -retime
+        run 'abc' with -dff option
 
-    %d
-        pop the top set from the stack and subtract it from the new top
+    -nocarry
+        do not use SB_CARRY cells in output netlist
 
-    %x[<num1>|*][.<num2>][:<rule>[:<rule>..]]
-        expand top set <num1> num times according to the specified rules.
-        (i.e. select all cells connected to selected wires and select all
-        wires connected to selected cells) The rules specify which cell
-        ports to use for this. the syntax for a rule is a '-' for exclusion
-        and a '+' for inclusion, followed by an optional comma seperated
-        list of cell types followed by an optional comma separated list of
-        cell ports in square brackets. a rule can also be just a cell or wire
-        name that limits the expansion (is included but does not go beyond).
-        select at most <num2> objects. a warning message is printed when this
-        limit is reached. When '*' is used instead of <num1> then the process
-        is repeated until no further object are selected.
+    -nodffe
+        do not use SB_DFFE* cells in output netlist
 
-    %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]]
-    %co[<num1>|*][.<num2>][:<rule>[:<rule>..]]
-        simmilar to %x, but only select input (%ci) or output cones (%co)
+    -nobram
+        do not use SB_RAM40_4K* cells in output netlist
 
-Example: the following command selects all wires that are connected to a
-'GATE' input of a 'SWITCH' cell:
+    -abc2
+        run two passes of 'abc' for slightly improved logic density
 
-    select */t:SWITCH %x:+[GATE] */t:SWITCH %d
-\end{lstlisting}
+    -vpr
+        generate an output netlist (and BLIF file) suitable for VPR
+        (this feature is experimental and incomplete)
 
-\section{shell -- enter interactive command mode}
-\label{cmd:shell}
-\begin{lstlisting}[numbers=left,frame=single]
-    shell
 
-This command enters the interactive command mode. This can be useful
-in a script to interrupt the script at a certain point and allow for
-interactive inspection or manual synthesis of the design at this point.
+The following commands are executed by this synthesis command:
 
-The command prompt of the interactive shell indicates the current
-selection (see 'help select'):
+    begin:
+        read_verilog -lib +/ice40/cells_sim.v
+        hierarchy -check -top <top>
 
-    yosys>
-        the entire design is selected
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
+        deminout
 
-    yosys*>
-        only part of the design is selected
+    coarse:
+        synth -run coarse
 
-    yosys [modname]>
-        the entire module 'modname' is selected using 'select -module modname'
+    bram:    (skip if -nobram)
+        memory_bram -rules +/ice40/brams.txt
+        techmap -map +/ice40/brams_map.v
 
-    yosys [modname]*>
-        only part of current module 'modname' is selected
+    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 -D NO_LUT -map +/ice40/cells_map.v
+        opt_expr -mux_undef
+        simplemap
+        ice40_ffinit
+        ice40_ffssr
+        ice40_opt -full
 
-When in interactive shell, some errors (e.g. invalid command arguments)
-do not terminate yosys but return to the command prompt.
+    map_luts:
+        abc          (only if -abc2)
+        ice40_opt    (only if -abc2)
+        techmap -map +/ice40/latches_map.v
+        abc -lut 4
+        clean
 
-This command is the default action if nothing else has been specified
-on the command line.
+    map_cells:
+        techmap -map +/ice40/cells_map.v    (with -D NO_LUT in vpr mode)
+        clean
 
-Press Ctrl-D or type 'exit' to leave the interactive shell.
-\end{lstlisting}
+    check:
+        hierarchy -check
+        stat
+        check -noinit
 
-\section{show -- generate schematics using graphviz}
-\label{cmd:show}
-\begin{lstlisting}[numbers=left,frame=single]
-    show [options] [selection]
+    blif:
+        opt_clean -purge                                     (vpr mode)
+        write_blif -attr -cname -conn -param <file-name>     (vpr mode)
+        write_blif -gates -attr -param <file-name>           (non-vpr mode)
 
-Create a graphviz DOT file for the selected part of the design and compile it
-to a graphics file (usually SVG or PostScript).
+    edif:
+        write_edif <file-name>
 
-    -viewer <viewer>
-        Run the specified command with the graphics file as parameter.
+    json:
+        write_json <file-name>
+\end{lstlisting}
 
-    -format <format>
-        Generate a graphics file in the specified format.
-        Usually <format> is 'svg' or 'ps'.
+\section{synth\_intel -- synthesis for Intel (Altera) FPGAs.}
+\label{cmd:synth_intel}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_intel [options]
 
-    -lib <verilog_or_ilang_file>
-        Use the specified library file for determining whether cell ports are
-        inputs or outputs. This option can be used multiple times to specify
-        more than one library.
+This command runs synthesis for Intel FPGAs.
 
-    -prefix <prefix>
-        generate <prefix>.* instead of ~/.yosys_show.*
+    -family < max10 | a10gx | cyclone10 | cyclonev | cycloneiv | cycloneive>
+        generate the synthesis netlist for the specified family.
+        MAX10 is the default target if not family argument specified.
+        For Cyclone GX devices, use cycloneiv argument; For Cyclone E, use cycloneive.
+        Cyclone V and Arria 10 GX devices are experimental, use it with a10gx argument.
 
-    -color <color> <wire>
-        assign the specified color to the specified wire. The object can be
-        a single selection wildcard expressions or a saved set of objects in
-        the @<name> syntax (see "help select" for details).
+    -top <module>
+        use the specified module as top module (default='top')
 
-    -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.
+    -vqm <file>
+        write the design to the specified Verilog Quartus Mapping File. Writing of an
+        output file is omitted if this parameter is not specified.
 
-    -width
-        annotate busses with a label indicating the width of the bus.
+    -vpr <file>
+        write BLIF files for VPR flow experiments. The synthesized BLIF output file is not
+        compatible with the Quartus flow. Writing of an
+        output file is omitted if this parameter is not specified.
 
-    -stretch
-        stretch the graph so all inputs are on the left side and all outputs
-        (including inout ports) are on the right side.
+    -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.
 
-When no <format> is specified, SVG is used. When no <format> and <viewer> is
-specified, 'yosys-svgviewer' is used to display the schematic.
+    -noiopads
+        do not use altsyncram cells in output netlist
 
-The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
-unless another prefix is specified using -prefix <prefix>.
-\end{lstlisting}
+    -nobram
+        do not use altsyncram cells in output netlist
 
-\section{splitnets -- split up multi-bit nets}
-\label{cmd:splitnets}
-\begin{lstlisting}[numbers=left,frame=single]
-    splitnets [options] [selection]
+    -noflatten
+        do not flatten design before synthesis
 
-This command splits multi-bit nets into single-bit nets.
+    -retime
+        run 'abc' with -dff option
 
-    -format char1[char2]
-        the first char is inserted between the net name and the bit index, the
-        second char is appended to the netname. e.g. -format () creates net
-        names like 'mysignal(42)'. the default is '[]'.
+The following commands are executed by this synthesis command:
 
-    -ports
-        also split module ports. per default only internal signals are split.
-\end{lstlisting}
+    begin:
 
-\section{submod -- moving part of a module to a new submodule}
-\label{cmd:submod}
-\begin{lstlisting}[numbers=left,frame=single]
-    submod [selection]
+    family:
+        read_verilog -sv -lib +/intel/max10/cells_sim.v
+        read_verilog -sv -lib +/intel/common/m9k_bb.v
+        read_verilog -sv -lib +/intel/common/altpll_bb.v
+        hierarchy -check -top <top>
 
-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
-cell that replaces the group of cells with the same attribute value.
+    flatten:    (unless -noflatten)
+        proc
+        flatten
+        tribuf -logic
+        deminout
 
-This pass can be used to create a design hierarchy in flat design. This can
-be useful for analyzing or reverse-engineering a design.
+    coarse:
+        synth -run coarse
 
-This pass only operates on completely selected modules with no processes
-or memories.
+    bram:    (skip if -nobram)
+        memory_bram -rules +/intel/common/brams.txt
+        techmap -map +/intel/common/brams_map.v
 
+    fine:
+        opt -fast -mux_undef -undriven -fine -full
+        memory_map
+        opt -undriven -fine
+        dffsr2dff
+        dff2dffe -direct-match $_DFF_*
+        opt -fine
+        techmap -map +/techmap.v
+        opt -full
+        clean -purge
+        setundef -undriven -zero
+        abc -markgroups -dff    (only if -retime)
 
-    submod -name <name> [selection]
+    map_luts:
+        abc -lut 4
+        clean
 
-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.
+    map_cells:
+        iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I    (unless -noiopads)
+        techmap -map +/intel/max10/cells_map.v
+        dffinit -highlow -ff dffeas q power_up
+        clean -purge
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    vqm:
+        write_verilog -attr2comment -defparam -nohex -decimal -renameprefix syn_ <file-name>
+
+    vpr:
+        opt_clean -purge
+        write_blif <file-name>
 \end{lstlisting}
 
 \section{synth\_xilinx -- synthesis for Xilinx FPGAs}
@@ -1160,61 +4229,87 @@ is used as the value of the 'submod' attribute above.
     synth_xilinx [options]
 
 This command runs synthesis for Xilinx FPGAs. This command does not operate on
-partly selected designs.
+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')
-
-    -arch <arch>
-        select architecture. the following architectures are supported:
-            spartan6 (default), artix7, kintex7, virtex7, zynq7000
-            (this parameter is not used by the command at the moment)
+        use the specified module as top module
 
     -edif <file>
         write the design to the specified edif file. writing of an output file
         is omitted if this parameter is not specified.
 
+    -blif <file>
+        write the design to the specified BLIF file. writing of an output file
+        is omitted if this parameter is not specified.
+
+    -vpr
+        generate an output netlist (and BLIF file) suitable for VPR
+        (this feature is experimental and incomplete)
+
     -run <from_label>:<to_label>
         only run the commands between the labels (see below). an empty
         from label is synonymous to 'begin', and empty to label is
         synonymous to the end of the command list.
 
+    -flatten
+        flatten design before synthesis
+
+    -retime
+        run 'abc' with -dff option
+
 
 The following commands are executed by this synthesis command:
 
     begin:
+        read_verilog -lib +/xilinx/cells_sim.v
+        read_verilog -lib +/xilinx/cells_xtra.v
+        read_verilog -lib +/xilinx/brams_bb.v
         hierarchy -check -top <top>
 
-    coarse:
+    flatten:     (only if -flatten)
         proc
-        opt
-        memory
-        clean
-        fsm
-        opt
+        flatten
+
+    coarse:
+        synth -run coarse
+
+    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:
-        techmap
-        opt
+        opt -fast -full
+        memory_map
+        dffsr2dff
+        dff2dffe
+        opt -full
+        techmap -map +/techmap.v -map +/xilinx/arith_map.v
+        opt -fast
 
     map_luts:
-        abc -lut 6
+        abc -luts 2:2,3,6:5,10,20 [-dff]
         clean
 
     map_cells:
-        techmap -map <share_dir>/xilinx/cells.v
+        techmap -map +/xilinx/cells_map.v (with -D NO_LUT in vpr mode)
+        dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT
         clean
 
-    clkbuf:
-        select -set xilinx_clocks <top>/t:FDRE %x:+FDRE[C] <top>/t:FDRE %d
-        iopadmap -inpad BUFGP O:I @xilinx_clocks
+    check:
+        hierarchy -check
+        stat
+        check -noinit
 
-    iobuf:
-        select -set xilinx_nonclocks <top>/w:* <top>/t:BUFGP %x:+BUFGP[I] %d
-        iopadmap -outpad OBUF I:O -inpad IBUF O:I @xilinx_nonclocks
+    edif:     (only if -edif)
+        write_edif <file-name>
 
-    edif:
-        write_edif -top <top> synth.edif
+    blif:     (only if -blif)
+        write_blif <file-name>
 \end{lstlisting}
 
 \section{tcl -- execute a TCL script file}
@@ -1226,18 +4321,18 @@ This command executes the tcl commands in the specified file.
 Use 'yosys cmd' to run the yosys command 'cmd' from tcl.
 
 The tcl command 'yosys -import' can be used to import all yosys
-commands directly as tcl commands to the tcl shell. The yosys
-command 'proc' is wrapped using the tcl command 'procs' in order
-to avoid a name collision with the tcl builting command 'proc'.
+commands directly as tcl commands to the tcl shell. Yosys commands
+'proc' and 'rename' are wrapped to tcl commands 'procs' and 'renames'
+in order to avoid a name collision with the built in commands.
 \end{lstlisting}
 
-\section{techmap -- simple technology mapper}
+\section{techmap -- generic technology mapper}
 \label{cmd:techmap}
 \begin{lstlisting}[numbers=left,frame=single]
     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
@@ -1246,12 +4341,51 @@ file.
         transforms the internal RTL cells to the internal gate
         library.
 
+    -map %<design-name>
+        like -map above, but with an in-memory design instead of a file.
+
+    -extern
+        load the cell implementations as separate modules into the design
+        instead of inlining them.
+
+    -max_iter <number>
+        only run the specified number of iterations.
+
+    -recursive
+        instead of the iterative breadth-first algorithm use a recursive
+        depth-first algorithm. both methods should yield equivalent results,
+        but may differ in performance.
+
+    -autoproc
+        Automatically call "proc" on implementations that contain processes.
+
+    -assert
+        this option will cause techmap to exit with an error if it can't map
+        a selected cell. only cell types that end on an underscore are accepted
+        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
+        '-nooverwrite' option set.
+
 When a module in the map file has the 'techmap_celltype' attribute set, it will
-match cells with a type that match the text value of this attribute.
+match cells with a type that match the text value of this attribute. Otherwise
+the module name will be used to match the cell.
+
+When a module in the map file has the 'techmap_simplemap' attribute set, techmap
+will use 'simplemap' (see 'help simplemap') to map cells matching the module.
+
+When a module in the map file has the 'techmap_maccmap' attribute set, techmap
+will use 'maccmap' (see 'help maccmap') to map cells matching the module.
+
+When a module in the map file has the 'techmap_wrap' attribute set, techmap
+will create a wrapper for the cell and then run the command string that the
+attribute is set to on the wrapper module.
 
 All wires in the modules from the map file matching the pattern _TECHMAP_*
 or *._TECHMAP_* are special wires that are used to pass instructions from
-the mapping module to the techmap command. At the moment the following spoecial
+the mapping module to the techmap command. At the moment the following special
 wires are supported:
 
     _TECHMAP_FAIL_
@@ -1273,23 +4407,96 @@ wires are supported:
         wire to start out as non-constant and evaluate to a constant value
         during processing of other _TECHMAP_DO_* commands.
 
+        A _TECHMAP_DO_* command may start with the special token 'CONSTMAP; '.
+        in this case techmap will create a copy for each distinct configuration
+        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
+        optimized specializations of techmap modules without using the special
+        parameters described below.
+
+        A _TECHMAP_DO_* command may start with the special token 'RECURSION; '.
+        then techmap will recursively replace the cells in the module with their
+        implementation. This is not affected by the -max_iter option.
+
+        It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '.
+
+In addition to this special wires, techmap also supports special parameters in
+modules in the map file:
+
+    _TECHMAP_CELLTYPE_
+        When a parameter with this name exists, it will be set to the type name
+        of the cell that matches the module.
+
+    _TECHMAP_CONSTMSK_<port-name>_
+    _TECHMAP_CONSTVAL_<port-name>_
+        When this pair of parameters is available in a module for a port, then
+        former has a 1-bit for each constant input bit and the latter has the
+        value for this bit. The unused bits of the latter are set to undef (x).
+
+    _TECHMAP_BITS_CONNMAP_
+    _TECHMAP_CONNMAP_<port-name>_
+        For an N-bit port, the _TECHMAP_CONNMAP_<port-name>_ parameter, if it
+        exists, will be set to an N*_TECHMAP_BITS_CONNMAP_ bit vector containing
+        N words (of _TECHMAP_BITS_CONNMAP_ bits each) that assign each single
+        bit driver a unique id. The values 0-3 are reserved for 0, 1, x, and z.
+        This can be used to detect shorted inputs.
+
 When a module in the map file has a parameter where the according cell in the
 design has a port, the module from the map file is only used if the port in
 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
+and attributes 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}
+\label{cmd:tee}
+\begin{lstlisting}[numbers=left,frame=single]
+    tee [-q] [-o logfile|-a logfile] cmd
+
+Execute the specified command, optionally writing the commands output to the
+specified logfile(s).
+
+    -q
+        Do not print output to the normal destination (console and/or log file)
+
+    -o logfile
+        Write output to this file, truncate if exists.
+
+    -a logfile
+        Write output to this file, append if exists.
+
+    +INT, -INT
+        Add/subract INT from the -v setting for this command.
+\end{lstlisting}
+
+\section{test\_abcloop -- automatically test handling of loops in abc command}
+\label{cmd:test_abcloop}
+\begin{lstlisting}[numbers=left,frame=single]
+    test_abcloop [options]
+
+Test handling of logic loops in ABC.
+
+    -n {integer}
+        create this number of circuits and test them (default = 100).
+
+    -s {positive_integer}
+        use this value as rng seed value (default = unix time).
 \end{lstlisting}
 
-\section{write\_autotest -- generate simple test benches}
-\label{cmd:write_autotest}
+\section{test\_autotb -- generate simple test benches}
+\label{cmd:test_autotb}
 \begin{lstlisting}[numbers=left,frame=single]
-    write_autotest [filename]
+    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.
 
@@ -1303,6 +4510,326 @@ be forced to be interpreted as clock signal by setting the attribute
 The attribute 'gentb_constant' can be used to force a signal to a constant
 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 should run (default = 1000)
+\end{lstlisting}
+
+\section{test\_cell -- automatically test the implementation of a cell type}
+\label{cmd:test_cell}
+\begin{lstlisting}[numbers=left,frame=single]
+    test_cell [options] {cell-types}
+
+Tests the internal implementation of the given cell type (for example '$add')
+by comparing SAT solver, EVAL and TECHMAP implementations of the cell types..
+
+Run with 'all' instead of a cell type to run the test on all supported
+cell types. Use for example 'all /$add' for all cell types except $add.
+
+    -n {integer}
+        create this number of cell instances and test them (default = 100).
+
+    -s {positive_integer}
+        use this value as rng seed value (default = unix time).
+
+    -f {ilang_file}
+        don't generate circuits. instead load the specified ilang file.
+
+    -w {filename_prefix}
+        don't test anything. just generate the circuits and write them
+        to ilang files with the specified prefix
+
+    -map {filename}
+        pass this option to techmap.
+
+    -simlib
+        use "techmap -D SIMLIB_NOCHECKS -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
+
+    -script {script_file}
+        instead of calling "techmap", call "script {script_file}".
+
+    -const
+        set some input bits to random constant values
+
+    -nosat
+        do not check SAT model or run SAT equivalence checking
+
+    -noeval
+        do not check const-eval models
+
+    -edges
+        test cell edges db creator against sat-based implementation
+
+    -v
+        print additional debug information to the console
+
+    -vlog {filename}
+        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]
+    trace cmd
+
+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{uniquify -- create unique copies of modules}
+\label{cmd:uniquify}
+\begin{lstlisting}[numbers=left,frame=single]
+    uniquify [selection]
+
+By default, a module that is instantiated by several other modules is only
+kept once in the design. This preserves the original modularity of the design
+and reduces the overall size of the design in memory. But it prevents certain
+optimizations and other operations on the design. This pass creates unique
+modules for all selected cells. The created modules are marked with the
+'unique' attribute.
+
+This commands only operates on modules that by themself have the 'unique'
+attribute set (the 'top' module is unique implicitly).
+\end{lstlisting}
+
+\section{verific -- load Verilog and VHDL designs using Verific}
+\label{cmd:verific}
+\begin{lstlisting}[numbers=left,frame=single]
+    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..
+
+Load the specified Verilog/SystemVerilog files into Verific.
+
+All files specified in one call to this command are one compilation unit.
+Files passed to different calls to this command are treated as belonging to
+different compilation units.
+
+Additional -D<macro>[=<value>] options may be added after the option indicating
+the language version (and before file names) to set additional verilog defines.
+The macros SYNTHESIS and VERIFIC are defined implicitly.
+
+
+    verific -formal <verilog-file>..
+
+Like -sv, but define FORMAL instead of SYNTHESIS.
+
+
+    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..
+
+Load the specified VHDL files into Verific.
+
+
+    verific -work <libname> {-sv|-vhdl|...} <hdl-file>
+
+Load the specified Verilog/SystemVerilog/VHDL file into the specified library.
+(default library when -work is not present: "work")
+
+
+    verific -vlog-incdir <directory>..
+
+Add Verilog include directories.
+
+
+    verific -vlog-libdir <directory>..
+
+Add Verilog library directories. Verific will search in this directories to
+find undefined modules.
+
+
+    verific -vlog-define <macro>[=<value>]..
+
+Add Verilog defines.
+
+
+    verific -vlog-undef <macro>..
+
+Remove Verilog defines previously set with -vlog-define.
+
+
+    verific -set-error <msg_id>..
+    verific -set-warning <msg_id>..
+    verific -set-info <msg_id>..
+    verific -set-ignore <msg_id>..
+
+Set message severity. <msg_id> is the string in square brackets when a message
+is printed, such as VERI-1209.
+
+
+    verific -import [options] <top-module>..
+
+Elaborate the design for the specified top modules, import to Yosys and
+reset the internal state of Verific.
+
+Import options:
+
+  -all
+    Elaborate all modules, not just the hierarchy below the given top
+    modules. With this option the list of modules to import is optional.
+
+  -gates
+    Create a gate-level netlist.
+
+  -flatten
+    Flatten the design in Verific before importing.
+
+  -extnets
+    Resolve references to external nets by adding module ports as needed.
+
+  -autocover
+    Generate automatic cover statements for all asserts
+
+  -v, -vv
+    Verbose log messages. (-vv is even more verbose than -v.)
+
+The following additional import options are useful for debugging the Verific
+bindings (for Yosys and/or Verific developers):
+
+  -k
+    Keep going after an unsupported verific primitive is found. The
+    unsupported primitive is added as blockbox module to the design.
+    This will also add all SVA related cells to the design parallel to
+    the checker logic inferred by it.
+
+  -V
+    Import Verific netlist as-is without translating to Yosys cell types. 
+
+  -nosva
+    Ignore SVA properties, do not infer checker logic.
+
+  -L <int>
+    Maximum number of ctrl bits for SVA checker FSMs (default=16).
+
+  -n
+    Keep all Verific names on instances and nets. By default only
+    user-declared names are preserved.
+
+  -d <dump_file>
+    Dump the Verific netlist as a verilog file.
+
+Visit http://verific.com/ for more information on Verific.
+\end{lstlisting}
+
+\section{verilog\_defaults -- set default options for read\_verilog}
+\label{cmd:verilog_defaults}
+\begin{lstlisting}[numbers=left,frame=single]
+    verilog_defaults -add [options]
+
+Add the specified options to the list of default options to read_verilog.
+
+
+    verilog_defaults -clear
+
+Clear the list of Verilog default options.
+
+
+    verilog_defaults -push
+    verilog_defaults -pop
+
+Push or pop the list of default options to a stack. Note that -push does
+not imply -clear.
+\end{lstlisting}
+
+\section{verilog\_defines -- define and undefine verilog defines}
+\label{cmd:verilog_defines}
+\begin{lstlisting}[numbers=left,frame=single]
+    verilog_defines [options]
+
+Define and undefine verilog preprocessor macros.
+
+    -Dname[=definition]
+        define the preprocessor symbol 'name' and set its optional value
+        'definition'
+
+    -Uname[=definition]
+        undefine the preprocessor symbol 'name'
+\end{lstlisting}
+
+\section{wreduce -- reduce the word size of operations if possible}
+\label{cmd:wreduce}
+\begin{lstlisting}[numbers=left,frame=single]
+    wreduce [options] [selection]
+
+This command reduces the word size of operations. For example it will replace
+the 32 bit adders in the following code with adders of more appropriate widths:
+
+    module test(input [3:0] a, b, c, output [7:0] y);
+        assign y = a + b + c + 1;
+    endmodule
+
+Options:
+
+    -memx
+        Do not change the width of memory address ports. Use this options in
+        flows that use the 'memory_memx' pass.
+\end{lstlisting}
+
+\section{write\_aiger -- write design to AIGER file}
+\label{cmd:write_aiger}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_aiger [options] [filename]
+
+Write the current design to an AIGER file. The design must be flattened and
+must not contain any cell types except $_AND_, $_NOT_, simple FF types,
+$assert and $assume cells, and $initstate cells.
+
+$assert and $assume cells are converted to AIGER bad state properties and
+invariant constraints.
+
+    -ascii
+        write ASCII version of AGIER format
+
+    -zinit
+        convert FFs to zero-initialized FFs, adding additional inputs for
+        uninitialized FFs.
+
+    -miter
+        design outputs are AIGER bad state properties
+
+    -symbols
+        include a symbol table in the generated AIGER file
+
+    -map <filename>
+        write an extra file with port and latch symbols
+
+    -vmap <filename>
+        like -map, but more verbose
 \end{lstlisting}
 
 \section{write\_blif -- write design to BLIF file}
@@ -1318,24 +4845,74 @@ Write the current design to an BLIF file.
     -buf <cell-type> <in-port> <out-port>
         use cells of type <cell-type> with the specified port names for buffers
 
+    -unbuf <cell-type> <in-port> <out-port>
+        replace buffer cells with the specified name and port names with
+        a .names statement that models a buffer
+
     -true <cell-type> <out-port>
     -false <cell-type> <out-port>
-        use the specified cell types to drive nets that are constant 1 or 0
-
-The following options can be usefull when the generated file is not going to be
+    -undef <cell-type> <out-port>
+        use the specified cell types to drive nets that are constant 1, 0, or
+        undefined. when '-' is used as <cell-type>, then <out-port> specifies
+        the wire name to be used for the constant signal and no cell driving
+        that wire is generated. when '+' is used as <cell-type>, then <out-port>
+        specifies the wire name to be used for the constant signal and a .names
+        statement is generated to drive the wire.
+
+    -noalias
+        if a net name is aliasing another net name, then by default a net
+        without fanout is created that is driven by the other net. This option
+        suppresses the generation of this nets without fanout.
+
+The following options can be useful when the generated file is not going to be
 read by a BLIF parser but a custom tool. It is recommended to not name the output
 file *.blif when any of this options is used.
 
-    -subckt
+    -icells
         do not translate Yosys's internal gates to generic BLIF logic
-        functions. Instead create .subckt lines for all cells.
+        functions. Instead create .subckt or .gate lines for all cells.
+
+    -gates
+        print .gate instead of .subckt lines for all cells that are not
+        instantiations of other modules from this design.
 
     -conn
         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 cell parameters
+
+    -cname
+        use the non-standard .cname statement to write cell names
+
+    -iname, -iattr
+        enable -cname and -attr functionality for .names statements
+        (the .cname and .attr statements will be included in the BLIF
+        output after the truth table for the .names statement)
+
+    -blackbox
+        write blackbox cells with .blackbox statement.
+
     -impltf
-        do not write definitions for the $true and $false wires.
+        do not write definitions for the $true, $false and $undef wires.
+\end{lstlisting}
+
+\section{write\_btor -- write design to BTOR file}
+\label{cmd:write_btor}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_btor [options] [filename]
+
+Write a BTOR description of the current design.
+
+  -v
+    Add comments and indentation to BTOR output file
+
+  -s
+    Output only a single bad property for all asserts
 \end{lstlisting}
 
 \section{write\_edif -- write design to EDIF netlist file}
@@ -1348,12 +4925,47 @@ Write the current design to an EDIF netlist file.
     -top top_module
         set the specified module as design top module
 
+    -nogndvcc
+        do not create "GND" and "VCC" cells. (this will produce an error
+        if the design contains constant nets. use "hilomap" to map to custom
+        constant drivers first)
+
+    -pvector {par|bra|ang}
+        sets the delimiting character for module port rename clauses to
+        parentheses, square brackets, or angle brackets.
+
 Unfortunately there are different "flavors" of the EDIF file format. This
 command generates EDIF files for the Xilinx place&route tools. It might be
 necessary to make small modifications to this command when a different tool
 is targeted.
 \end{lstlisting}
 
+\section{write\_file -- write a text to a file}
+\label{cmd:write_file}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_file [options] output_file [input_file]
+
+Write the text from the input file to the output file.
+
+    -a
+        Append to output file (instead of overwriting)
+
+
+Inside a script the input file can also can a here-document:
+
+    write_file hello.txt <<EOT
+    Hello World!
+    EOT
+\end{lstlisting}
+
+\section{write\_firrtl -- write design to a FIRRTL file}
+\label{cmd:write_firrtl}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_firrtl [options] [filename]
+
+Write a FIRRTL netlist of the current design.
+\end{lstlisting}
+
 \section{write\_ilang -- write design to ilang file}
 \label{cmd:write_ilang}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1390,6 +5002,403 @@ 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.
+
+Numeric parameter and attribute values up to 32 bits are written as decimal
+values. Numbers larger than that are written as string holding the binary
+representation of the value.
+
+For example the following Verilog code:
+
+    module test(input x, y);
+      (* 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\_simplec -- convert design to simple C code}
+\label{cmd:write_simplec}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_simplec [options] [filename]
+
+Write simple C code for simulating the design. The C code writen can be used to
+simulate the design in a C environment, but the purpose of this command is to
+generate code that works well with C-based formal verification.
+
+    -verbose
+        this will print the recursive walk used to export the modules.
+
+    -i8, -i16, -i32, -i64
+        set the maximum integer bit width to use in the generated code.
+
+THIS COMMAND IS UNDER CONSTRUCTION
+\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 will
+define and declare functions operating on that state.
+
+The following SMT2 functions are generated for a module with name '<mod>'.
+Some declarations/definitions are printed with a special comment. A prover
+using the SMT2 files can use those comments to collect all relevant metadata
+about the design.
+
+    ; yosys-smt2-module <mod>
+    (declare-sort |<mod>_s| 0)
+        The sort representing a state of module <mod>.
+
+    (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))
+        This function must be asserted for each state to establish the
+        design hierarchy.
+
+    ; yosys-smt2-input <wirename> <width>
+    ; yosys-smt2-output <wirename> <width>
+    ; yosys-smt2-register <wirename> <width>
+    ; yosys-smt2-wire <wirename> <width>
+    (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))
+    (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)
+        For each port, register, and wire with the 'keep' attribute set an
+        accessor function is generated. Single-bit wires are returned as Bool,
+        multi-bit wires as BitVec.
+
+    ; yosys-smt2-cell <submod> <instancename>
+    (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)
+        There is a function like that for each hierarchical instance. It
+        returns the sort that represents the state of the sub-module that
+        implements the instance.
+
+    (declare-fun |<mod>_is| (|<mod>_s|) Bool)
+        This function must be asserted 'true' for initial states, and 'false'
+        otherwise.
+
+    (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))
+        This function must be asserted 'true' for initial states. For
+        non-initial states it must be left unconstrained.
+
+    (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))
+        This function evaluates to 'true' if the states 'state' and
+        'next_state' form a valid state transition.
+
+    (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))
+        This function evaluates to 'true' if all assertions hold in the state.
+
+    (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))
+        This function evaluates to 'true' if all assumptions hold in the state.
+
+    ; yosys-smt2-assert <id> <filename:linenum>
+    (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))
+        Each $assert cell is converted into one of this functions. The function
+        evaluates to 'true' if the assert statement holds in the state.
+
+    ; yosys-smt2-assume <id> <filename:linenum>
+    (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))
+        Each $assume cell is converted into one of this functions. The function
+        evaluates to 'true' if the assume statement holds in the state.
+
+    ; yosys-smt2-cover <id> <filename:linenum>
+    (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))
+        Each $cover cell is converted into one of this functions. The function
+        evaluates to 'true' if the cover statement is activated in the state.
+
+Options:
+
+    -verbose
+        this will print the recursive walk used to export the modules.
+
+    -stbv
+        Use a BitVec sort to represent a state instead of an uninterpreted
+        sort. As a side-effect this will prevent use of arrays to model
+        memories.
+
+    -stdt
+        Use SMT-LIB 2.6 style datatypes to represent a state instead of an
+        uninterpreted sort.
+
+    -nobv
+        disable support for BitVec (FixedSizeBitVectors theory). without this
+        option multi-bit wires are represented using the BitVec sort and
+        support for coarse grain cells (incl. arithmetic) is enabled.
+
+    -nomem
+        disable support for memories (via ArraysEx theory). this option is
+        implied by -nobv. 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.
+
+    -wires
+        create '<mod>_n' functions for all public wires. by default only ports,
+        registers, and wires with the 'keep' attribute are exported.
+
+    -tpl <template_file>
+        use the given template file. the line containing only the token '%%'
+        is replaced with the regular output of this command.
+
+[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David
+R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf
+
+---------------------------------------------------------------------------
+
+Example:
+
+Consider the following module (test.v). We want to prove that the output can
+never transition from a non-zero value to a zero value.
+
+        module test(input clk, output reg [3:0] y);
+          always @(posedge clk)
+            y <= (y << 1) | ^y;
+        endmodule
+
+For this proof we create the following template (test.tpl).
+
+        ; we need QF_UFBV for this poof
+        (set-logic QF_UFBV)
+
+        ; insert the auto-generated code here
+        %%
+
+        ; declare two state variables s1 and s2
+        (declare-fun s1 () test_s)
+        (declare-fun s2 () test_s)
+
+        ; state s2 is the successor of state s1
+        (assert (test_t s1 s2))
+
+        ; we are looking for a model with y non-zero in s1
+        (assert (distinct (|test_n y| s1) #b0000))
+
+        ; we are looking for a model with y zero in s2
+        (assert (= (|test_n y| s2) #b0000))
+
+        ; is there such a model?
+        (check-sat)
+
+The following yosys script will create a 'test.smt2' file for our proof:
+
+        read_verilog test.v
+        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]
@@ -1398,7 +5407,7 @@ http://www.clifford.at/intersynth/
 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
@@ -1410,22 +5419,48 @@ Write the current design to an SPICE netlist file.
     -nc_prefix
         prefix for not-connected nets (default: _NC)
 
+    -inames
+        include names of internal ($-prefixed) nets in outputs
+        (default is to use net numbers instead)
+
     -top top_module
         set the specified module as design top module
 \end{lstlisting}
 
-\section{write\_verilog -- write design to verilog file}
+\section{write\_table -- write design as connectivity table}
+\label{cmd:write_table}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_table [options] [filename]
+
+Write the current design as connectivity table. The output is a tab-separated
+ASCII table with the following columns:
+
+  module name
+  cell name
+  cell type
+  cell port
+  direction
+  signal
+
+module inputs and outputs are output using cell type and port '-' and with
+'pi' (primary input) or 'po' (primary output) or 'pio' as direction.
+\end{lstlisting}
+
+\section{write\_verilog -- write design to Verilog file}
 \label{cmd:write_verilog}
 \begin{lstlisting}[numbers=left,frame=single]
     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
         instead of a backslash prefix) are changed to short names in the
         format '_<number>_'.
 
+    -renameprefix <prefix>
+        insert this prefix in front of auto-generated instance names
+
     -noattr
         with this option no attributes are included in the output
 
@@ -1433,9 +5468,32 @@ 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.
 
+    -nodec
+        32-bit constant values are by default dumped as decimal numbers,
+        not bit pattern. This option deactivates this feature and instead
+        will write out all constants in binary.
+
+    -decimal
+        dump 32-bit constants in decimal and without size and radix
+
+    -nohex
+        constant values that are compatible with hex output are usually
+        dumped as hex values. This option deactivates this feature and
+        instead will write out all constants in binary.
+
+    -nostr
+        Parameters and attributes that are specified as strings in the
+        original input will be output as strings by this back-end. This
+        deactivates this feature and instead will write string constants
+        as binary numbers.
+
+    -defparam
+        Use 'defparam' statements instead of the Verilog-2001 syntax for
+        cell parameters.
+
     -blackboxes
         usually modules with the 'blackbox' attribute are ignored. with
         this option set only the modules with the 'blackbox' attribute
@@ -1444,5 +5502,25 @@ Write the current design to a verilog file.
     -selected
         only write selected modules. modules must be selected entirely or
         not at all.
+
+    -v
+        verbose output (print new names of all renamed wires and cells)
+
+Note that RTLIL processes can't always be mapped directly to Verilog
+always blocks. This frontend should only be used to export an RTLIL
+netlist, i.e. after the "proc" pass has been used to convert all
+processes to logic networks and registers. A warning is generated when
+this command is called on a design with RTLIL processes.
+\end{lstlisting}
+
+\section{zinit -- add inverters so all FF are zero-initialized}
+\label{cmd:zinit}
+\begin{lstlisting}[numbers=left,frame=single]
+    zinit [options] [selection]
+
+Add inverters as needed to make all FFs zero-initialized.
+
+    -all
+        also add zero initialization to uninitialized FFs
 \end{lstlisting}