diff options
author | Miodrag Milanovic <mmicko@gmail.com> | 2022-03-04 10:56:33 +0100 |
---|---|---|
committer | Miodrag Milanovic <mmicko@gmail.com> | 2022-03-04 10:56:33 +0100 |
commit | a7090e9711339b56f98ee25d78286203a0545acb (patch) | |
tree | 423ee00bac4372824ec800f1b8c6b15859dc9d50 | |
parent | 9581b9adac1578ddad5df27daeb8edf6d2f5d9b2 (diff) | |
download | yosys-a7090e9711339b56f98ee25d78286203a0545acb.tar.gz yosys-a7090e9711339b56f98ee25d78286203a0545acb.tar.bz2 yosys-a7090e9711339b56f98ee25d78286203a0545acb.zip |
Update documentation
-rw-r--r-- | manual/command-reference-manual.tex | 97 |
1 files changed, 96 insertions, 1 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 1aa0facb5..e3055c0bc 100644 --- a/manual/command-reference-manual.tex +++ b/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 |