diff options
Diffstat (limited to 'manual/command-reference-manual.tex')
| -rw-r--r-- | manual/command-reference-manual.tex | 161 |
1 files changed, 157 insertions, 4 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 2d5f55749..e3055c0bc 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -671,6 +671,14 @@ Convert modules into blackbox modules (remove contents and set the blackbox module attribute). \end{lstlisting} +\section{bmuxmap -- transform \$bmux cells to trees of \$mux cells} +\label{cmd:bmuxmap} +\begin{lstlisting}[numbers=left,frame=single] + bmuxmap [selection] + +This pass transforms $bmux cells to trees of $mux cells. +\end{lstlisting} + \section{bugpoint -- minimize testcases} \label{cmd:bugpoint} \begin{lstlisting}[numbers=left,frame=single] @@ -1133,6 +1141,14 @@ selected wires, thus 'deleting' module ports. "Demote" inout ports to input or output ports, if possible. \end{lstlisting} +\section{demuxmap -- transform \$demux cells to \$eq + \$mux cells} +\label{cmd:demuxmap} +\begin{lstlisting}[numbers=left,frame=single] + demuxmap [selection] + +This pass transforms $demux cells to a bunch of equality comparisons. +\end{lstlisting} + \section{design -- save, restore and reset current design} \label{cmd:design} \begin{lstlisting}[numbers=left,frame=single] @@ -2206,6 +2222,89 @@ one-hot encoding and binary encoding is supported. .map <old_bitpattern> <new_bitpattern> \end{lstlisting} +\section{glift -- create GLIFT models and optimization problems} +\label{cmd:glift} +\begin{lstlisting}[numbers=left,frame=single] + glift <command> [options] [selection] + +Augments the current or specified module with gate-level information flow tracking +(GLIFT) logic using the "constructive mapping" approach. Also can set up QBF-SAT +optimization problems in order to optimize GLIFT models or trade off precision and +complexity. + + +Commands: + + -create-precise-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with precise taint tracking logic. + For example, precise taint tracking logic for an AND gate is: + + y_t = a & b_t | b & a_t | a_t & b_t + + + -create-imprecise-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with imprecise "All OR" taint tracking + logic: + + y_t = a_t | b_t + + + -create-instrumented-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with 4 varying-precision versions of taint + tracking logic. Which version of taint tracking logic is used for a given gate is + determined by a MUX selected by an $anyconst cell. By default, unless the + `-no-cost-model` option is provided, an additional wire named `__glift_weight` with + the `keep` and `minimize` attributes is added to the module along with pmuxes and + adders to calculate a rough estimate of the number of logic gates in the GLIFT model + given an assignment for the $anyconst cells. The four versions of taint tracking logic + for an AND gate are: + y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`) + y_t = a_t | a & b_t + y_t = b_t | b & a_t + y_t = a_t | b_t (like `-create-imprecise-model`) + + +Options: + + -taint-constants + Constant values in the design are labeled as tainted. + (default: label constants as un-tainted) + + -keep-outputs + Do not remove module outputs. Taint tracking outputs will appear in the module ports + alongside the orignal outputs. + (default: original module outputs are removed) + + -simple-cost-model + Do not model logic area. Instead model the number of non-zero assignments to $anyconsts. + Taint tracking logic versions vary in their size, but all reduced-precision versions are + significantly smaller than the fully-precise version. A non-zero $anyconst assignment means + that reduced-precision taint tracking logic was chosen for some gate. + Only applicable in combination with `-create-instrumented-model`. + (default: use a complex model and give that wire the "keep" and "minimize" attributes) + + -no-cost-model + Do not model taint tracking logic area and do not create a `__glift_weight` wire. + Only applicable in combination with `-create-instrumented-model`. + (default: model area and give that wire the "keep" and "minimize" attributes) + + -instrument-more + Allow choice from more versions of (even simpler) taint tracking logic. A total + of 8 versions of taint tracking logic will be added per gate, including the 4 + versions from `-create-instrumented-model` and these additional versions: + + y_t = a_t + y_t = b_t + y_t = 1 + y_t = 0 + + Only applicable in combination with `-create-instrumented-model`. + (default: do not add more versions of taint tracking logic. +\end{lstlisting} + \section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches} \label{cmd:greenpak4_dffinv} \begin{lstlisting}[numbers=left,frame=single] @@ -2420,7 +2519,7 @@ the resulting cells to more sophisticated PAD cells. -inpad <celltype> <in_port>[:<ext_port>] 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 + signal is passed through the pad cell, using the 2nd portname as the port facing the module port. -outpad <celltype> <out_port>[:<ext_port>] @@ -4815,6 +4914,16 @@ This command simulates the circuit using the given top-level module. -vcd <filename> write the simulation results to the given VCD file + -fst <filename> + write the simulation results to the given FST file + + -aiw <filename> + write the simulation results to an AIGER witness file + (requires a *.aim file via -map) + + -x + ignore constant x outputs in simulation file. + -clock <portname> name of top-level clock input @@ -4837,14 +4946,44 @@ This command simulates the circuit using the given top-level module. include the specified timescale declaration in the vcd -n <integer> - number of cycles to simulate (default: 20) + number of clock cycles to simulate (default: 20) -a - include all nets in VCD output, not just those with public names + use all nets in VCD/FST operations, not just those with public names -w writeback mode: use final simulation state as new init state + -r + read simulation results file (file formats supported: FST) + + -map <filename> + read file with port and latch symbols, needed for AIGER witness input + + -scope + scope of simulation top model + + -at <time> + sets start and stop time + + -start <time> + start co-simulation in arbitary time (default 0) + + -stop <time> + stop co-simulation in arbitary time (default END) + + -sim + simulation with stimulus from FST (default) + + -sim-cmp + co-simulation expect exact match + + -sim-gold + co-simulation, x in simulation can match any value in FST + + -sim-gate + co-simulation, x in FST can match any value in simulation + -d enable debug output \end{lstlisting} @@ -5197,6 +5336,9 @@ This command runs synthesis for Anlogic FPGAs. -nolutram do not use EG_LOGIC_DRAM16X4 cells in output netlist + -nobram + do not use EG_PHY_BRAM or EG_PHY_BRAM32K cells in output netlist + The following commands are executed by this synthesis command: @@ -5213,6 +5355,12 @@ The following commands are executed by this synthesis command: coarse: synth -run coarse + map_bram: (skip if -nobram) + memory_bram -rules +/anlogic/brams.txt + techmap -map +/anlogic/brams_map.v + setundef -zero -params t:EG_PHY_BRAM + setundef -zero -params t:EG_PHY_BRAM32K + map_lutram: (skip if -nolutram) memory_bram -rules +/anlogic/lutrams.txt techmap -map +/anlogic/lutrams_map.v @@ -6781,6 +6929,7 @@ The following commands are executed by this synthesis command: write_blif -attr -param -auto-top verilog: + write_verilog -noattr -nohex <file-name> \end{lstlisting} \section{synth\_sf2 -- synthesis for SmartFusion2 and IGLOO2 FPGAs} @@ -7495,9 +7644,11 @@ Like -sv, but define FORMAL instead of SYNTHESIS. Load the specified VHDL files into Verific. - verific {-f|-F} <command-file> + verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal] <command-file> Load and execute the specified command file. +Override verilog parsing mode can be set. +The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly. Command file parser supports following commands: +define - defines macro @@ -8193,6 +8344,8 @@ Inside a script the input file can also can a here-document: Write a FIRRTL netlist of the current design. The following commands are executed by this command: pmuxtree + bmuxmap + demuxmap \end{lstlisting} \section{write\_ilang -- (deprecated) alias of write\_rtlil} |