Update manual

manual/command-reference-manual.tex

@@ -764,12 +764,14 @@ 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 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'.
@@ -2166,6 +2168,13 @@ Options:
     -fm_set_fsm_file file
     -encfile file
         passed through to fsm_recode pass
+
+This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'
+before this pass to prepare the design.
+
+The Verific frontend may merge multiplexers in a way that interferes with FSM
+detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before
+reading the source, and 'bmuxmap' after 'proc' for best results.
 \end{lstlisting}
 
 \section{fsm\_detect -- finding FSMs in design}
@@ -2181,6 +2190,13 @@ 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".
+
+This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'
+before this pass to prepare the design for fsm_detect.
+
+The Verific frontend may merge multiplexers in a way that interferes with FSM
+detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before
+reading the source, and 'bmuxmap' after 'proc' for best results.
 \end{lstlisting}
 
 \section{fsm\_expand -- expand FSM cells by merging logic into it}
@@ -4435,6 +4451,9 @@ and additional constraints passed as parameters.
     -set-def-inputs
         add -set-def constraints for all module inputs
 
+    -set-def-formal
+        add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells
+
     -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.
@@ -5233,7 +5252,7 @@ This command simulates the circuit using the given top-level module.
     -r
         read simulation results file
             File formats supported: FST, VCD, AIW and WIT
-		 VCD support requires vcd2fst external tool to be present
+            VCD support requires vcd2fst external tool to be present
 
     -map <filename>
         read file with port and latch symbols, needed for AIGER witness input
@@ -6099,6 +6118,165 @@ The following commands are executed by this synthesis command:
         write_json <file-name>
 \end{lstlisting}
 
+\section{synth\_fabulous -- FABulous synthesis script}
+\label{cmd:synth_fabulous}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_fabulous [options]
+
+This command runs synthesis for FPGA fabrics generated with FABulous. 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
+
+    -blif <file>
+        write the design to the specified BLIF file. writing of an output file
+        is omitted if this parameter is not specified.
+
+    -edif <file>
+        write the design to the specified EDIF file. writing of an output file
+        is omitted if this parameter is not specified.
+
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
+        is omitted if this parameter is not specified.
+
+    -lut <k>
+        perform synthesis for a k-LUT architecture (default 4).
+
+    -vpr
+        perform synthesis for the FABulous VPR flow (using slightly different techmapping).
+
+    -plib <primitive_library.v>
+        use the specified Verilog file as a primitive library.
+
+    -extra-plib <primitive_library.v>
+        use the specified Verilog file for extra primitives (can be specified multiple
+        times).
+
+    -extra-map <techamp.v>
+        use the specified Verilog file for extra techmap rules (can be specified multiple
+        times).
+
+    -encfile <file>
+        passed to 'fsm_recode' via 'fsm'
+
+    -nofsm
+        do not run FSM optimization
+
+    -noalumacc
+        do not run 'alumacc' pass. i.e. keep arithmetic operators in
+        their direct form ($add, $sub, etc.).
+
+    -noregfile
+        do not map register files
+
+    -iopad
+        enable automatic insertion of IO buffers (otherwise a wrapper
+        with manually inserted and constrained IO should be used.)
+
+    -complex-dff
+        enable support for FFs with enable and synchronous SR (must also be
+        supported by the target fabric.)
+
+    -noflatten
+        do not flatten design after elaboration
+
+    -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.
+
+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+
+
+The following commands are executed by this synthesis command:
+        read_verilog  -lib +/fabulous/prims.v
+        read_verilog -lib <extra_plib.v>    (for each -extra-plib)
+
+    begin:
+        hierarchy -check
+        proc
+
+    flatten:    (unless -noflatten)
+        flatten
+        tribuf -logic
+        deminout
+
+    coarse:
+        tribuf -logic
+        deminout
+        opt_expr
+        opt_clean
+        check
+        opt -nodffe -nosdff
+        fsm          (unless -nofsm)
+        opt
+        wreduce
+        peepopt
+        opt_clean
+        techmap -map +/cmp2lut.v -map +/cmp2lcu.v     (if -lut)
+        alumacc      (unless -noalumacc)
+        share        (unless -noshare)
+        opt
+        memory -nomap
+        opt_clean
+
+    map_ram:
+        memory_libmap -lib +/fabulous/ram_regfile.txt
+        techmap -map +/fabulous/regfile_map.v
+
+    map_ffram:
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+
+    map_gates:
+        opt -full
+        techmap -map +/techmap.v
+        opt -fast
+
+    map_iopad:    (if -iopad)
+
+    map_ffs:
+        dfflegalize -cell $_DFF_P_ 0 -cell $_DLATCH_?_ x    without -complex-dff
+        techmap -map +/fabulous/latches_map.v
+        techmap -map +/fabulous/ff_map.v
+        techmap -map <extra_map.v>...    (for each -extra-map)
+        clean
+
+    map_luts:
+        abc -lut 4 -dress
+        clean
+
+    map_cells:
+        techmap -D LUT_K=4 -map +/fabulous/cells_map.v
+        clean
+
+    check:
+        hierarchy -check
+        stat
+
+    blif:
+        opt_clean -purge
+        write_blif -attr -cname -conn -param <file-name>
+
+    json:
+        write_json <file-name>
+\end{lstlisting}
+
 \section{synth\_gatemate -- synthesis for Cologne Chip GateMate FPGAs}
 \label{cmd:synth_gatemate}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -7550,8 +7728,8 @@ If any arguments are specified, these arguments are provided to the script via
 the standard $argc and $argv variables.
 
 Note, tcl will not recieve the output of any yosys command. If the output
-of the tcl commands are needed, use the yosys command 'tee' to redirect yosys's
+of the tcl commands are needed, use the yosys command 'tee -s result.string'
-output to a temporary file.
+to redirect yosys's output to the 'result.string' scratchpad value.
 \end{lstlisting}
 
 \section{techmap -- generic technology mapper}
@@ -7736,6 +7914,9 @@ specified logfile(s).
     -a logfile
         Write output to this file, append if exists.
 
+    -s scratchpad
+        Write output to this scratchpad value, truncate if it exists.
+
     +INT, -INT
         Add/subtract INT from the -v setting for this command.
 \end{lstlisting}
@@ -8047,12 +8228,14 @@ Remove Verilog defines previously set with -vlog-define.
 
 Set message severity. <msg_id> is the string in square brackets when a message
 is printed, such as VERI-1209.
+Also errors, warnings, infos and comments could be used to set new severity for
+all messages of certain type.
 
 
-    verific -import [options] <top-module>..
+    verific -import [options] <top>..
 
-Elaborate the design for the specified top modules, import to Yosys and
+Elaborate the design for the specified top modules or configurations, import to
-reset the internal state of Verific.
+Yosys and reset the internal state of Verific.
 
 Import options: