Update documentation

manual/command-reference-manual.tex

@@ -2222,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]
@@ -4834,6 +4917,13 @@ This command simulates the circuit using the given top-level module.
     -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
 
@@ -4867,6 +4957,9 @@ This command simulates the circuit using the given top-level module.
     -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
 
@@ -7551,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