mirror of https://github.com/YosysHQ/yosys.git
7632 lines
246 KiB
TeX
7632 lines
246 KiB
TeX
% Generated using the yosys 'help -write-tex-command-reference-manual' command.
|
|
|
|
\section{abc -- use ABC for technology mapping}
|
|
\label{cmd:abc}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
abc [options] [selection]
|
|
|
|
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 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).
|
|
|
|
-constr <file>
|
|
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,
|
|
NMUX, 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
|
|
cmos: NAND NOR AOI3 OAI3 AOI4 OAI4 NMUX MUX XOR XNOR
|
|
gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT
|
|
aig: AND NAND OR NOR ANDNOT ORNOT
|
|
|
|
The alias 'all' represent the full set of all gate types.
|
|
|
|
Prefix a gate type with a '-' to remove it from the list. For example
|
|
the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent.
|
|
|
|
The default is 'all,-NMUX,-AOI3,-OAI3,-AOI4,-OAI4'.
|
|
|
|
-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.
|
|
|
|
-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.
|
|
|
|
-dress
|
|
run the 'dress' command after all other ABC commands. This aims to
|
|
preserve naming by an equivalence check between the original and post-ABC
|
|
netlists (experimental).
|
|
|
|
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 then 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}
|
|
|
|
\section{abc9 -- use ABC9 for technology mapping}
|
|
\label{cmd:abc9}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
abc9 [options] [selection]
|
|
|
|
This script pass performs a sequence of commands to facilitate the use of the ABC
|
|
tool [1] for technology mapping of the current design to a target FPGA
|
|
architecture. Only fully-selected modules are supported.
|
|
|
|
-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.
|
|
|
|
-exe <command>
|
|
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:
|
|
&scorr; &sweep; &dc2; &dch -f; &ps; &if {C} {W} {D} {R} -v; &mfs
|
|
|
|
-fast
|
|
use different default scripts that are slightly faster (at the cost
|
|
of output quality):
|
|
&if {C} {W} {D} {R} -v
|
|
|
|
-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
|
|
(indicating best possible delay).
|
|
|
|
-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.
|
|
|
|
-lut <file>
|
|
pass this file with lut library to ABC.
|
|
|
|
-luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,..
|
|
generate netlist using luts. Use the specified costs for luts with 1,
|
|
2, 3, .. inputs.
|
|
|
|
-maxlut <width>
|
|
when auto-generating the lut library, discard all luts equal to or
|
|
greater than this size (applicable when neither -lut nor -luts is
|
|
specified).
|
|
|
|
-dff
|
|
also pass $_ABC9_FF_ cells through to ABC. modules with many clock
|
|
domains are marked as such and automatically partitioned by ABC.
|
|
|
|
-nocleanup
|
|
when this option is used, the temporary files created by this pass
|
|
are not removed. this is useful for debugging.
|
|
|
|
-showtmp
|
|
print the temp dir name in log. usually this is suppressed so that the
|
|
command output is identical across runs.
|
|
|
|
-box <file>
|
|
pass this file with box library to ABC.
|
|
|
|
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 an XAIGER file with `write_xaiger' and then 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/
|
|
|
|
|
|
pre:
|
|
abc9_ops -check
|
|
scc -set_attr abc9_scc_id {}
|
|
abc9_ops -mark_scc -prep_delays -prep_xaiger [-dff] (option for -dff)
|
|
abc9_ops -prep_lut <maxlut> (skip if -lut or -luts)
|
|
abc9_ops -prep_box [-dff] (skip if -box)
|
|
select -set abc9_holes A:abc9_holes
|
|
flatten -wb @abc9_holes
|
|
techmap @abc9_holes
|
|
abc9_ops -prep_dff (only if -dff)
|
|
opt -purge @abc9_holes
|
|
aigmap
|
|
wbflip @abc9_holes
|
|
|
|
map:
|
|
foreach module in selection
|
|
abc9_ops -write_lut <abc-temp-dir>/input.lut (skip if '-lut' or '-luts')
|
|
abc9_ops -write_box <abc-temp-dir>/input.box
|
|
write_xaiger -map <abc-temp-dir>/input.sym <abc-temp-dir>/input.xaig
|
|
abc9_exe [options] -cwd <abc-temp-dir> [-lut <abc-temp-dir>/input.lut] -box <abc-temp-dir>/input.box
|
|
read_aiger -xaiger -wideports -module_name <module-name>$abc9 -map <abc-temp-dir>/input.sym <abc-temp-dir>/output.aig
|
|
abc9_ops -reintegrate
|
|
\end{lstlisting}
|
|
|
|
\section{abc9\_exe -- use ABC9 for technology mapping}
|
|
\label{cmd:abc9_exe}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
abc9_exe [options]
|
|
|
|
|
|
This pass uses the ABC tool [1] for technology mapping of the top module
|
|
(according to the (* top *) attribute or if only one module is currently selected)
|
|
to a target FPGA architecture.
|
|
|
|
-exe <command>
|
|
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:
|
|
&scorr; &sweep; &dc2; &dch -f; &ps; &if {C} {W} {D} {R} -v; &mfs
|
|
|
|
-fast
|
|
use different default scripts that are slightly faster (at the cost
|
|
of output quality):
|
|
&if {C} {W} {D} {R} -v
|
|
|
|
-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
|
|
(indicating best possible delay).
|
|
|
|
-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.
|
|
|
|
-lut <file>
|
|
pass this file with lut library to ABC.
|
|
|
|
-luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,..
|
|
generate netlist using luts. Use the specified costs for luts with 1,
|
|
2, 3, .. inputs.
|
|
|
|
-showtmp
|
|
print the temp dir name in log. usually this is suppressed so that the
|
|
command output is identical across runs.
|
|
|
|
-box <file>
|
|
pass this file with box library to ABC.
|
|
|
|
-cwd <dir>
|
|
use this as the current working directory, inside which the 'input.xaig'
|
|
file is expected. temporary files will be created in this directory, and
|
|
the mapped result will be written to 'output.aig'.
|
|
|
|
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 then 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}
|
|
|
|
\section{abc9\_ops -- helper functions for ABC9}
|
|
\label{cmd:abc9_ops}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
abc9_ops [options] [selection]
|
|
|
|
This pass contains a set of supporting operations for use during ABC technology
|
|
mapping, and is expected to be called in conjunction with other operations from
|
|
the `abc9' script pass. Only fully-selected modules are supported.
|
|
|
|
-check
|
|
check that the design is valid, e.g. (* abc9_box_id *) values are unique,
|
|
(* abc9_carry *) is only given for one input/output port, etc.
|
|
|
|
-prep_delays
|
|
insert `$__ABC9_DELAY' blackbox cells into the design to account for
|
|
certain required times.
|
|
|
|
-mark_scc
|
|
for an arbitrarily chosen cell in each unique SCC of each selected module
|
|
(tagged with an (* abc9_scc_id = <int> *) attribute), temporarily mark all
|
|
wires driven by this cell's outputs with a (* keep *) attribute in order
|
|
to break the SCC. this temporary attribute will be removed on -reintegrate.
|
|
|
|
-prep_xaiger
|
|
prepare the design for XAIGER output. this includes computing the
|
|
topological ordering of ABC9 boxes, as well as preparing the
|
|
'<module-name>$holes' module that contains the logic behaviour of ABC9
|
|
whiteboxes.
|
|
|
|
-dff
|
|
consider flop cells (those instantiating modules marked with (* abc9_flop *))
|
|
during -prep_{delays,xaiger,box}.
|
|
|
|
-prep_dff
|
|
compute the clock domain and initial value of each flop in the design.
|
|
process the '$holes' module to support clock-enable functionality.
|
|
|
|
-prep_lut <maxlut>
|
|
pre-compute the lut library by analysing all modules marked with
|
|
(* abc9_lut=<area> *).
|
|
|
|
-write_lut <dst>
|
|
write the pre-computed lut library to <dst>.
|
|
|
|
-prep_box
|
|
pre-compute the box library by analysing all modules marked with
|
|
(* abc9_box *).
|
|
|
|
-write_box <dst>
|
|
write the pre-computed box library to <dst>.
|
|
|
|
-reintegrate
|
|
for each selected module, re-intergrate the module '<module-name>$abc9'
|
|
by first recovering ABC9 boxes, and then stitching in the remaining primary
|
|
inputs and outputs.
|
|
\end{lstlisting}
|
|
|
|
\section{add -- add objects to the design}
|
|
\label{cmd:add}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
add <command> [selection]
|
|
|
|
This command adds objects to the design. It operates on all fully selected
|
|
modules. So e.g. 'add -wire foo' will add a wire foo to all selected modules.
|
|
|
|
|
|
add {-wire|-input|-inout|-output} <name> <width> [selection]
|
|
|
|
Add a wire (input, inout, output port) with the given name and width. The
|
|
command will fail if the object exists already and has different properties
|
|
than the object to be created.
|
|
|
|
|
|
add -global_input <name> <width> [selection]
|
|
|
|
Like 'add -input', but also connect the signal between instances of the
|
|
selected modules.
|
|
|
|
|
|
add {-assert|-assume|-live|-fair|-cover} <name1> [-if <name2>]
|
|
|
|
Add an $assert, $assume, etc. cell connected to a wire named name1, with its
|
|
enable signal optionally connected to a wire named name2 (default: 1'b1).
|
|
|
|
|
|
add -mod <name[s]>
|
|
|
|
Add module[s] with the specified name[s].
|
|
\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
|
|
|
|
-select
|
|
Overwrite replaced cells in the current selection with new $_AND_,
|
|
$_NOT_, and $_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{anlogic\_eqn -- Anlogic: Calculate equations for luts}
|
|
\label{cmd:anlogic_eqn}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
anlogic_eqn [selection]
|
|
|
|
Calculate equations for luts since bitstream generator depends on it.
|
|
\end{lstlisting}
|
|
|
|
\section{anlogic\_fixcarry -- Anlogic: fix carry chain}
|
|
\label{cmd:anlogic_fixcarry}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
anlogic_fixcarry [options] [selection]
|
|
|
|
Add Anlogic adders to fix carry chain if needed.
|
|
\end{lstlisting}
|
|
|
|
\section{assertpmux -- adds asserts for parallel muxes}
|
|
\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 by the mux tree it drives. this option will deactivate this
|
|
additional constraint 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, $dffsr, and $dlatch 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 maps 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{autoname -- automatically assign names to objects}
|
|
\label{cmd:autoname}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
autoname [selection]
|
|
|
|
Assign auto-generated public names to objects with private names (the ones
|
|
with $-prefix).
|
|
\end{lstlisting}
|
|
|
|
\section{blackbox -- convert modules into blackbox modules}
|
|
\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{bugpoint -- minimize testcases}
|
|
\label{cmd:bugpoint}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
bugpoint [options]
|
|
|
|
This command minimizes testcases that crash Yosys. It removes an arbitrary part
|
|
of the design and recursively invokes Yosys with a given script, repeating these
|
|
steps while it can find a smaller design that still causes a crash. Once this
|
|
command finishes, it replaces the current design with the smallest testcase it
|
|
was able to produce.
|
|
|
|
It is possible to specify the kinds of design part that will be removed. If none
|
|
are specified, all parts of design will be removed.
|
|
|
|
-yosys <filename>
|
|
use this Yosys binary. if not specified, `yosys` is used.
|
|
|
|
-script <filename>
|
|
use this script to crash Yosys. required.
|
|
|
|
-grep <string>
|
|
only consider crashes that place this string in the log file.
|
|
|
|
-fast
|
|
run `proc_clean; clean -purge` after each minimization step. converges
|
|
faster, but produces larger testcases, and may fail to produce any
|
|
testcase at all if the crash is related to dangling wires.
|
|
|
|
-clean
|
|
run `proc_clean; clean -purge` before checking testcase and after
|
|
finishing. produces smaller and more useful testcases, but may fail to
|
|
produce any testcase at all if the crash is related to dangling wires.
|
|
|
|
-modules
|
|
try to remove modules.
|
|
|
|
-ports
|
|
try to remove module ports.
|
|
|
|
-cells
|
|
try to remove cells.
|
|
|
|
-connections
|
|
try to reconnect ports to 'x.
|
|
|
|
-assigns
|
|
try to remove process assigns from cases.
|
|
|
|
-updates
|
|
try to remove process updates from syncs.
|
|
|
|
-runner "<prefix>"
|
|
child process wrapping command, e.g., "timeout 30", or valgrind.
|
|
\end{lstlisting}
|
|
|
|
\section{cd -- a shortcut for 'select -module <name>'}
|
|
\label{cmd:cd}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
cd <modname>
|
|
|
|
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 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{check -- check for obvious problems in the design}
|
|
\label{cmd:check}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
check [options] [selection]
|
|
|
|
This pass identifies the following problems in the current design:
|
|
|
|
- combinatorial loops
|
|
|
|
- two or more conflicting drivers for one wire
|
|
|
|
- used wires that do not have a driver
|
|
|
|
Options:
|
|
|
|
-noinit
|
|
Also check for wires which have the 'init' attribute set.
|
|
|
|
-initdrv
|
|
Also check for wires that have the 'init' attribute set and are not
|
|
driven by an FF cell type.
|
|
|
|
-mapped
|
|
Also check for internal cells that have not been mapped to cells of the
|
|
target architecture.
|
|
|
|
-allow-tbuf
|
|
Modify the -mapped behavior to still allow $_TBUF_ cells.
|
|
|
|
-assert
|
|
Produce a runtime error if any problems are found in the current design.
|
|
\end{lstlisting}
|
|
|
|
\section{chformal -- change formal constraints of the design}
|
|
\label{cmd:chformal}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
chformal [types] [mode] [options] [selection]
|
|
|
|
Make changes to the formal constraints of the design. The [types] options
|
|
the type of constraint to operate on. If none of the following options are 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
|
|
|
|
Exactly one of the following modes must be specified:
|
|
|
|
-remove
|
|
remove the cells and thus constraints from the design
|
|
|
|
-early
|
|
bypass FFs that only delay the activation of a constraint
|
|
|
|
-delay <N>
|
|
delay activation of the constraint by <N> clock cycles
|
|
|
|
-skip <N>
|
|
ignore activation of the constraint in the first <N> clock cycles
|
|
|
|
-assert2assume
|
|
-assume2assert
|
|
-live2fair
|
|
-fair2live
|
|
change the roles of cells as indicated. these options can be combined
|
|
\end{lstlisting}
|
|
|
|
\section{chparam -- re-evaluate modules with new parameters}
|
|
\label{cmd:chparam}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
chparam [ -set name value ]... [selection]
|
|
|
|
Re-evaluate the selected modules with new parameters. String values must be
|
|
passed in double quotes (").
|
|
|
|
|
|
chparam -list [selection]
|
|
|
|
List the available parameters of the selected modules.
|
|
\end{lstlisting}
|
|
|
|
\section{chtype -- change type of cells in the design}
|
|
\label{cmd:chtype}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
chtype [options] [selection]
|
|
|
|
Change the types of cells in the design.
|
|
|
|
-set <type>
|
|
set the cell type to the given type
|
|
|
|
-map <old_type> <new_type>
|
|
change cells types that match <old_type> to <new_type>
|
|
\end{lstlisting}
|
|
|
|
\section{clean -- remove unused cells and wires}
|
|
\label{cmd:clean}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
clean [options] [selection]
|
|
|
|
This is identical to 'opt_clean', but less verbose.
|
|
|
|
When commands are separated using the ';;' token, this command will be executed
|
|
between the commands.
|
|
|
|
When commands are separated using the ';;;' token, this command will be executed
|
|
in -purge mode between the commands.
|
|
\end{lstlisting}
|
|
|
|
\section{clk2fflogic -- convert clocked FFs to generic \$ff cells}
|
|
\label{cmd:clk2fflogic}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
clk2fflogic [options] [selection]
|
|
|
|
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}
|
|
|
|
\section{clkbufmap -- insert global buffers on clock networks}
|
|
\label{cmd:clkbufmap}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
clkbufmap [options] [selection]
|
|
|
|
Inserts global buffers between nets connected to clock inputs and their drivers.
|
|
|
|
In the absence of any selection, all wires without the 'clkbuf_inhibit'
|
|
attribute will be considered for global buffer insertion.
|
|
Alternatively, to consider all wires without the 'buffer_type' attribute set to
|
|
'none' or 'bufr' one would specify:
|
|
'w:* a:buffer_type=none a:buffer_type=bufr %u %d'
|
|
as the selection.
|
|
|
|
-buf <celltype> <portname_out>:<portname_in>
|
|
Specifies the cell type to use for the global buffers
|
|
and its port names. The first port will be connected to
|
|
the clock network sinks, and the second will be connected
|
|
to the actual clock source. This option is required.
|
|
|
|
-inpad <celltype> <portname_out>:<portname_in>
|
|
If specified, a PAD cell of the given type is inserted on
|
|
clock nets that are also top module's inputs (in addition
|
|
to the global buffer).
|
|
\end{lstlisting}
|
|
|
|
\section{connect -- create or remove connections}
|
|
\label{cmd:connect}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr>
|
|
|
|
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.
|
|
|
|
|
|
connect [-nomap] -unset <expr>
|
|
|
|
Unconnect all existing drivers for the specified expression.
|
|
|
|
|
|
connect [-nomap] -port <cell> <port> <expr>
|
|
|
|
Connect the specified cell port to the specified cell port.
|
|
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
This command does not operate on module with processes.
|
|
\end{lstlisting}
|
|
|
|
\section{connect\_rpc -- connect to RPC frontend}
|
|
\label{cmd:connect_rpc}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
connect_rpc -exec <command> [args...]
|
|
connect_rpc -path <path>
|
|
|
|
Load modules using an out-of-process frontend.
|
|
|
|
-exec <command> [args...]
|
|
run <command> with arguments [args...]. send requests on stdin, read
|
|
responses from stdout.
|
|
|
|
-path <path>
|
|
connect to Unix domain socket at <path>. (Unix)
|
|
connect to bidirectional byte-type named pipe at <path>. (Windows)
|
|
|
|
A simple JSON-based, newline-delimited protocol is used for communicating with
|
|
the frontend. Yosys requests data from the frontend by sending exactly 1 line
|
|
of JSON. Frontend responds with data or error message by replying with exactly
|
|
1 line of JSON as well.
|
|
|
|
-> {"method": "modules"}
|
|
<- {"modules": ["<module-name>", ...]}
|
|
<- {"error": "<error-message>"}
|
|
request for the list of modules that can be derived by this frontend.
|
|
the 'hierarchy' command will call back into this frontend if a cell
|
|
with type <module-name> is instantiated in the design.
|
|
|
|
-> {"method": "derive", "module": "<module-name">, "parameters": {
|
|
"<param-name>": {"type": "[unsigned|signed|string|real]",
|
|
"value": "<param-value>"}, ...}}
|
|
<- {"frontend": "[ilang|verilog|...]","source": "<source>"}}
|
|
<- {"error": "<error-message>"}
|
|
request for the module <module-name> to be derived for a specific set of
|
|
parameters. <param-name> starts with \ for named parameters, and with $
|
|
for unnamed parameters, which are numbered starting at 1.<param-value>
|
|
for integer parameters is always specified as a binary string of unlimited
|
|
precision. the <source> returned by the frontend is hygienically parsed
|
|
by a built-in Yosys <frontend>, allowing the RPC frontend to return any
|
|
convenient representation of the module. the derived module is cached,
|
|
so the response should be the same whenever the same set of parameters
|
|
is provided.
|
|
\end{lstlisting}
|
|
|
|
\section{connwrappers -- match width of input-output port pairs}
|
|
\label{cmd:connwrappers}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
connwrappers [options] [selection]
|
|
|
|
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.
|
|
|
|
-signed <cell_type> <port_name> <width_param>
|
|
-unsigned <cell_type> <port_name> <width_param>
|
|
consider the specified signed/unsigned wrapper output
|
|
|
|
-port <cell_type> <port_name> <width_param> <sign_param>
|
|
use the specified parameter to decide if signed or unsigned
|
|
|
|
The options -signed, -unsigned, and -port can be specified multiple times.
|
|
\end{lstlisting}
|
|
|
|
\section{coolrunner2\_fixup -- insert necessary buffer cells for CoolRunner-II architecture}
|
|
\label{cmd:coolrunner2_fixup}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
coolrunner2_fixup [options] [selection]
|
|
|
|
Insert necessary buffer cells for CoolRunner-II architecture.
|
|
\end{lstlisting}
|
|
|
|
\section{coolrunner2\_sop -- break \$sop cells into ANDTERM/ORTERM cells}
|
|
\label{cmd:coolrunner2_sop}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
coolrunner2_sop [options] [selection]
|
|
|
|
Break $sop cells into ANDTERM/ORTERM cells.
|
|
\end{lstlisting}
|
|
|
|
\section{copy -- copy modules in the design}
|
|
\label{cmd:copy}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
copy old_name new_name
|
|
|
|
Copy the specified module. Note that selection patterns are not supported
|
|
by this command.
|
|
\end{lstlisting}
|
|
|
|
\section{cover -- print code coverage counters}
|
|
\label{cmd:cover}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
cover [options] [pattern]
|
|
|
|
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.
|
|
|
|
-q
|
|
Do not print output to the normal destination (console and/or log file)
|
|
|
|
-o file
|
|
Write output to this file, truncate if exists.
|
|
|
|
-a file
|
|
Write output to this file, append if exists.
|
|
|
|
-d dir
|
|
Write output to a newly created file in the specified directory.
|
|
|
|
When one or more pattern (shell wildcards) are specified, then only counters
|
|
matching at least one pattern are printed.
|
|
|
|
|
|
It is also possible to instruct Yosys to print the coverage counters on program
|
|
exit to a file using environment variables:
|
|
|
|
YOSYS_COVER_DIR="{dir-name}" yosys {args}
|
|
|
|
This will create a file (with an auto-generated name) in this
|
|
directory and write the coverage counters to it.
|
|
|
|
YOSYS_COVER_FILE="{file-name}" yosys {args}
|
|
|
|
This will append the coverage counters to the specified file.
|
|
|
|
|
|
Hint: Use the following AWK command to consolidate Yosys coverage files:
|
|
|
|
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
|
|
|
|
|
|
Coverage counters are only available in Yosys for Linux.
|
|
\end{lstlisting}
|
|
|
|
\section{cutpoint -- adds formal cut points to the design}
|
|
\label{cmd:cutpoint}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
cutpoint [options] [selection]
|
|
|
|
This command adds formal cut points to the design.
|
|
|
|
-undef
|
|
set cupoint nets to undef (x). the default behavior is to create a
|
|
$anyseq cell and drive the cutpoint net from that
|
|
\end{lstlisting}
|
|
|
|
\section{debug -- run command with debug log messages enabled}
|
|
\label{cmd:debug}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
debug cmd
|
|
|
|
Execute the specified command with debug log messages enabled
|
|
\end{lstlisting}
|
|
|
|
\section{delete -- delete objects in the design}
|
|
\label{cmd:delete}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
delete [selection]
|
|
|
|
Deletes the selected objects. This will also remove entire modules, if the
|
|
whole module is selected.
|
|
|
|
|
|
delete {-input|-output|-port} [selection]
|
|
|
|
Does not delete any object but removes the input and/or output flag on the
|
|
selected wires, thus 'deleting' module ports.
|
|
\end{lstlisting}
|
|
|
|
\section{deminout -- demote inout ports to input or output}
|
|
\label{cmd:deminout}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
deminout [options] [selection]
|
|
|
|
"Demote" inout ports to input or output ports, if possible.
|
|
\end{lstlisting}
|
|
|
|
\section{design -- save, restore and reset current design}
|
|
\label{cmd:design}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
design -reset
|
|
|
|
Clear the current design.
|
|
|
|
|
|
design -save <name>
|
|
|
|
Save the current design under the given name.
|
|
|
|
|
|
design -stash <name>
|
|
|
|
Save the current design under the given name and then clear the current design.
|
|
|
|
|
|
design -push
|
|
|
|
Push the current design to the stack and then clear the current design.
|
|
|
|
|
|
design -push-copy
|
|
|
|
Push the current design to the stack without clearing the current design.
|
|
|
|
|
|
design -pop
|
|
|
|
Reset the current design and pop the last design from the stack.
|
|
|
|
|
|
design -load <name>
|
|
|
|
Reset the current design and load the design previously saved under the given
|
|
name.
|
|
|
|
|
|
design -copy-from <name> [-as <new_mod_name>] <selection>
|
|
|
|
Copy modules from the specified design into the current one. The selection is
|
|
evaluated in the other design.
|
|
|
|
|
|
design -copy-to <name> [-as <new_mod_name>] [selection]
|
|
|
|
Copy modules from the current design into the specified one.
|
|
|
|
|
|
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{determine\_init -- Determine the init value of cells}
|
|
\label{cmd:determine_init}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
determine_init [selection]
|
|
|
|
Determine the init value of cells that doesn't allow unknown init value.
|
|
\end{lstlisting}
|
|
|
|
\section{dff2dffe -- transform \$dff cells to \$dffe cells}
|
|
\label{cmd:dff2dffe}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
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 ignored in unmap mode.
|
|
|
|
-unmap-mince N
|
|
Same as -unmap but only unmap $dffe where the clock enable port
|
|
signal is used by less $dffe than the specified number
|
|
|
|
-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}
|
|
|
|
\section{dff2dffs -- process sync set/reset with SR over CE priority}
|
|
\label{cmd:dff2dffs}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
dff2dffs [options] [selection]
|
|
|
|
Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before
|
|
dff2dffe for SR over CE priority.
|
|
|
|
-match-init
|
|
Disallow merging synchronous set/reset that has polarity opposite of the
|
|
output wire's init attribute (if any).
|
|
\end{lstlisting}
|
|
|
|
\section{dffinit -- set INIT param on FF cells}
|
|
\label{cmd:dffinit}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
dffinit [options] [selection]
|
|
|
|
This pass sets an FF cell parameter to the the initial value of the net it
|
|
drives. (This is primarily used in FPGA flows.)
|
|
|
|
-ff <cell_name> <output_port> <init_param>
|
|
operate on the specified cell type. this option can be used
|
|
multiple times.
|
|
|
|
-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.)
|
|
|
|
-strinit <string for high> <string for low>
|
|
use string values in the command line to represent a single-bit
|
|
initial value of 1 or 0. (multi-bit values are not supported in this
|
|
mode.)
|
|
|
|
-noreinit
|
|
fail if the FF cell has already a defined initial value set in other
|
|
passes and the initial value of the net it drives is not equal to
|
|
the already defined initial value.
|
|
\end{lstlisting}
|
|
|
|
\section{dfflibmap -- technology mapping of flip-flops}
|
|
\label{cmd:dfflibmap}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
dfflibmap [-prepare] -liberty <file> [selection]
|
|
|
|
Map internal flip-flop cells to the flip-flop cells in the technology
|
|
library specified in the given liberty file.
|
|
|
|
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.
|
|
|
|
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{dump -- print parts of the design in ilang format}
|
|
\label{cmd:dump}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
dump [options] [selection]
|
|
|
|
Write the selected parts of the design to the console or specified file in
|
|
ilang format.
|
|
|
|
-m
|
|
also dump the module headers, even if only parts of a single
|
|
module is selected
|
|
|
|
-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{echo -- turning echoing back of commands on and off}
|
|
\label{cmd:echo}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
echo on
|
|
|
|
Print all commands to log before executing them.
|
|
|
|
|
|
echo off
|
|
|
|
Do not print all commands to log before executing them. (default)
|
|
\end{lstlisting}
|
|
|
|
\section{ecp5\_ffinit -- ECP5: handle FF init values}
|
|
\label{cmd:ecp5_ffinit}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
ecp5_ffinit [options] [selection]
|
|
|
|
Remove init values for FF output signals when equal to reset value.
|
|
If reset is not used, set the reset value to the init value, otherwise
|
|
unmap out the reset (if not an async reset).
|
|
\end{lstlisting}
|
|
|
|
\section{ecp5\_gsr -- ECP5: handle GSR}
|
|
\label{cmd:ecp5_gsr}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
ecp5_gsr [options] [selection]
|
|
|
|
Trim active low async resets connected to GSR and resolve GSR parameter,
|
|
if a GSR or SGSR primitive is used in the design.
|
|
|
|
If any cell has the GSR parameter set to "AUTO", this will be resolved
|
|
to "ENABLED" if a GSR primitive is present and the (* nogsr *) attribute
|
|
is not set, otherwise it will be resolved to "DISABLED".
|
|
\end{lstlisting}
|
|
|
|
\section{edgetypes -- list all types of edges in selection}
|
|
\label{cmd:edgetypes}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
edgetypes [options] [selection]
|
|
|
|
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{efinix\_fixcarry -- Efinix: fix carry chain}
|
|
\label{cmd:efinix_fixcarry}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
efinix_fixcarry [options] [selection]
|
|
|
|
Add Efinix adders to fix carry chain if needed.
|
|
\end{lstlisting}
|
|
|
|
\section{efinix\_gbuf -- Efinix: insert global clock buffers}
|
|
\label{cmd:efinix_gbuf}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
efinix_gbuf [options] [selection]
|
|
|
|
Add Efinix global clock buffers to top module as needed.
|
|
\end{lstlisting}
|
|
|
|
\section{equiv\_add -- add a \$equiv cell}
|
|
\label{cmd:equiv_add}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_add [-try] gold_sig gate_sig
|
|
|
|
This command adds an $equiv cell for the specified signals.
|
|
|
|
|
|
equiv_add [-try] -cell gold_cell gate_cell
|
|
|
|
This command adds $equiv cells for the ports of the specified cells.
|
|
\end{lstlisting}
|
|
|
|
\section{equiv\_induct -- proving \$equiv cells using temporal induction}
|
|
\label{cmd:equiv_induct}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_induct [options] [selection]
|
|
|
|
Uses a version of temporal induction to prove $equiv cells.
|
|
|
|
Only selected $equiv cells are proven and only selected cells are used to
|
|
perform the proof.
|
|
|
|
-undef
|
|
enable modelling of undef states
|
|
|
|
-seq <N>
|
|
the max. number of time steps to be considered (default = 4)
|
|
|
|
This command is very effective in proving complex sequential circuits, when
|
|
the internal state of the circuit quickly propagates to $equiv cells.
|
|
|
|
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).
|
|
|
|
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{equiv\_make -- prepare a circuit for equivalence checking}
|
|
\label{cmd:equiv_make}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_make [options] gold_module gate_module equiv_module
|
|
|
|
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.
|
|
|
|
-inames
|
|
Also match cells and wires with $... names.
|
|
|
|
-blacklist <file>
|
|
Do not match cells or signals that match the names in the file.
|
|
|
|
-encfile <file>
|
|
Match FSM encodings using the description from the file.
|
|
See 'help fsm_recode' for details.
|
|
|
|
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{equiv\_mark -- mark equivalence checking regions}
|
|
\label{cmd:equiv_mark}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_mark [options] [selection]
|
|
|
|
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{equiv\_miter -- extract miter from equiv circuit}
|
|
\label{cmd:equiv_miter}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_miter [options] miter_module [selection]
|
|
|
|
This creates a miter module for further analysis of the selected $equiv cells.
|
|
|
|
-trigger
|
|
Create a trigger output
|
|
|
|
-cmp
|
|
Create cmp_* outputs for individual unproven $equiv cells
|
|
|
|
-assert
|
|
Create a $assert cell for each unproven $equiv cell
|
|
|
|
-undef
|
|
Create compare logic that handles undefs correctly
|
|
\end{lstlisting}
|
|
|
|
\section{equiv\_opt -- prove equivalence for optimized circuit}
|
|
\label{cmd:equiv_opt}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_opt [options] [command]
|
|
|
|
This command uses temporal induction to check circuit equivalence before and
|
|
after an optimization pass.
|
|
|
|
-run <from_label>:<to_label>
|
|
only run the commands between the labels (see below). an empty
|
|
from label is synonymous to the start of the command list, and empty to
|
|
label is synonymous to the end of the command list.
|
|
|
|
-map <filename>
|
|
expand the modules in this file before proving equivalence. this is
|
|
useful for handling architecture-specific primitives.
|
|
|
|
-blacklist <file>
|
|
Do not match cells or signals that match the names in the file
|
|
(passed to equiv_make).
|
|
|
|
-assert
|
|
produce an error if the circuits are not equivalent.
|
|
|
|
-multiclock
|
|
run clk2fflogic before equivalence checking.
|
|
|
|
-async2sync
|
|
run async2sync before equivalence checking.
|
|
|
|
-undef
|
|
enable modelling of undef states during equiv_induct.
|
|
|
|
The following commands are executed by this verification command:
|
|
|
|
run_pass:
|
|
hierarchy -auto-top
|
|
design -save preopt
|
|
[command]
|
|
design -stash postopt
|
|
|
|
prepare:
|
|
design -copy-from preopt -as gold A:top
|
|
design -copy-from postopt -as gate A:top
|
|
|
|
techmap: (only with -map)
|
|
techmap -wb -D EQUIV -autoproc -map <filename> ...
|
|
|
|
prove:
|
|
clk2fflogic (only with -multiclock)
|
|
async2sync (only with -async2sync)
|
|
equiv_make -blacklist <filename> ... gold gate equiv
|
|
equiv_induct [-undef] equiv
|
|
equiv_status [-assert] equiv
|
|
|
|
restore:
|
|
design -load preopt
|
|
\end{lstlisting}
|
|
|
|
\section{equiv\_purge -- purge equivalence checking module}
|
|
\label{cmd:equiv_purge}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_purge [options] [selection]
|
|
|
|
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{equiv\_remove -- remove \$equiv cells}
|
|
\label{cmd:equiv_remove}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_remove [options] [selection]
|
|
|
|
This command removes the selected $equiv cells. If neither -gold nor -gate is
|
|
used then only proven cells are removed.
|
|
|
|
-gold
|
|
keep gold circuit
|
|
|
|
-gate
|
|
keep gate circuit
|
|
\end{lstlisting}
|
|
|
|
\section{equiv\_simple -- try proving simple \$equiv instances}
|
|
\label{cmd:equiv_simple}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
equiv_simple [options] [selection]
|
|
|
|
This command tries to prove $equiv cells using a simple direct SAT approach.
|
|
|
|
-v
|
|
verbose output
|
|
|
|
-undef
|
|
enable modelling of undef states
|
|
|
|
-short
|
|
create shorter input cones that stop at shared nodes. This yields
|
|
simpler SAT problems but sometimes fails to prove equivalence.
|
|
|
|
-nogroup
|
|
disabling grouping of $equiv cells by output wire
|
|
|
|
-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{exec -- execute commands in the operating system shell}
|
|
\label{cmd:exec}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
exec [options] -- [command]
|
|
|
|
Execute a command in the operating system shell. All supplied arguments are
|
|
concatenated and passed as a command to popen(3). Whitespace is not guaranteed
|
|
to be preserved, even if quoted. stdin and stderr are not connected, while stdout is
|
|
logged unless the "-q" option is specified.
|
|
|
|
|
|
-q
|
|
Suppress stdout and stderr from subprocess
|
|
|
|
-expect-return <int>
|
|
Generate an error if popen() does not return specified value.
|
|
May only be specified once; the final specified value is controlling
|
|
if specified multiple times.
|
|
|
|
-expect-stdout <regex>
|
|
Generate an error if the specified regex does not match any line
|
|
in subprocess's stdout. May be specified multiple times.
|
|
|
|
-not-expect-stdout <regex>
|
|
Generate an error if the specified regex matches any line
|
|
in subprocess's stdout. May be specified multiple times.
|
|
|
|
|
|
Example: exec -q -expect-return 0 -- echo "bananapie" | grep "nana"
|
|
\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 (default 64)
|
|
|
|
-minwidth N
|
|
Only extract counters at least N bits wide (default 2)
|
|
|
|
-allow_arst yes|no
|
|
Allow counters to have async reset (default yes)
|
|
|
|
-dir up|down|both
|
|
Look for up-counters, down-counters, or both (default down)
|
|
|
|
-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{extractinv -- extract explicit inverter cells for invertible cell pins}
|
|
\label{cmd:extractinv}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
extractinv [options] [selection]
|
|
|
|
Searches the design for all cells with invertible pins controlled by a cell
|
|
parameter (eg. IS_CLK_INVERTED on many Xilinx cells) and removes the parameter.
|
|
If the parameter was set to 1, inserts an explicit inverter cell in front of
|
|
the pin instead. Normally used for output to ISE, which does not support the
|
|
inversion parameters.
|
|
|
|
To mark a cell port as invertible, use (* invertible_pin = "param_name" *)
|
|
on the wire in the blackbox module. The parameter value should have
|
|
the same width as the port, and will be effectively XORed with it.
|
|
|
|
-inv <celltype> <portname_out>:<portname_in>
|
|
Specifies the cell type to use for the inverters and its port names.
|
|
This option is required.
|
|
\end{lstlisting}
|
|
|
|
\section{flatten -- flatten design}
|
|
\label{cmd:flatten}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
flatten [options] [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.
|
|
|
|
-wb
|
|
Ignore the 'whitebox' attribute on cell implementations.
|
|
\end{lstlisting}
|
|
|
|
\section{flowmap -- pack LUTs with FlowMap}
|
|
\label{cmd:flowmap}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
flowmap [options] [selection]
|
|
|
|
This pass uses the FlowMap technology mapping algorithm to pack logic gates
|
|
into k-LUTs with optimal depth. It allows mapping any circuit elements that can
|
|
be evaluated with the `eval` pass, including cells with multiple output ports
|
|
and multi-bit input and output ports.
|
|
|
|
-maxlut k
|
|
perform technology mapping for a k-LUT architecture. if not specified,
|
|
defaults to 3.
|
|
|
|
-minlut n
|
|
only produce n-input or larger LUTs. if not specified, defaults to 1.
|
|
|
|
-cells <cell>[,<cell>,...]
|
|
map specified cells. if not specified, maps $_NOT_, $_AND_, $_OR_,
|
|
$_XOR_ and $_MUX_, which are the outputs of the `simplemap` pass.
|
|
|
|
-relax
|
|
perform depth relaxation and area minimization.
|
|
|
|
-r-alpha n, -r-beta n, -r-gamma n
|
|
parameters of depth relaxation heuristic potential function.
|
|
if not specified, alpha=8, beta=2, gamma=1.
|
|
|
|
-optarea n
|
|
optimize for area by trading off at most n logic levels for fewer LUTs.
|
|
n may be zero, to optimize for area without increasing depth.
|
|
implies -relax.
|
|
|
|
-debug
|
|
dump intermediate graphs.
|
|
|
|
-debug-relax
|
|
explain decisions performed during depth relaxation.
|
|
\end{lstlisting}
|
|
|
|
\section{fmcombine -- combine two instances of a cell into one}
|
|
\label{cmd:fmcombine}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
fmcombine [options] module_name gold_cell gate_cell
|
|
|
|
This pass takes two cells, which are instances of the same module, and replaces
|
|
them with one instance of a special 'combined' module, that effectively
|
|
contains two copies of the original module, plus some formal properties.
|
|
|
|
This is useful for formal test benches that check what differences in behavior
|
|
a slight difference in input causes in a module.
|
|
|
|
-initeq
|
|
Insert assumptions that initially all FFs in both circuits have the
|
|
same initial values.
|
|
|
|
-anyeq
|
|
Do not duplicate $anyseq/$anyconst cells.
|
|
|
|
-fwd
|
|
Insert forward hint assumptions into the combined module.
|
|
|
|
-bwd
|
|
Insert backward hint assumptions into the combined module.
|
|
(Backward hints are logically equivalend to fordward hits, but
|
|
some solvers are faster with bwd hints, or even both -bwd and -fwd.)
|
|
|
|
-nop
|
|
Don't insert hint assumptions into the combined module.
|
|
(This should not provide any speedup over the original design, but
|
|
strangely sometimes it does.)
|
|
|
|
If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.
|
|
\end{lstlisting}
|
|
|
|
\section{fminit -- set init values/sequences for formal}
|
|
\label{cmd:fminit}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
fminit [options] <selection>
|
|
|
|
This pass creates init constraints (for example for reset sequences) in a formal
|
|
model.
|
|
|
|
-seq <signal> <sequence>
|
|
Set sequence using comma-separated list of values, use 'z for
|
|
unconstrained bits. The last value is used for the remainder of the
|
|
trace.
|
|
|
|
-set <signal> <value>
|
|
Add constant value constraint
|
|
|
|
-posedge <signal>
|
|
-negedge <signal>
|
|
Set clock for init sequences
|
|
\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. It also resolves assignments to wired logic data types (wand/wor),
|
|
resolves positional module parameters, unroll array instances, and more.
|
|
|
|
-check
|
|
also check the design hierarchy. this generates an error when
|
|
an unknown module is used as cell type.
|
|
|
|
-simcheck
|
|
like -check, but also throw 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.
|
|
|
|
-nodefaults
|
|
do not resolve input port default values
|
|
|
|
-nokeep_asserts
|
|
per default this pass sets the "keep" attribute on all modules
|
|
that directly or indirectly contain one or more formal properties.
|
|
This option disables this behavior.
|
|
|
|
-top <module>
|
|
use the specified top module to build the 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.
|
|
|
|
-chparam name value
|
|
elaborate the top module using this parameter value. Modules on which
|
|
this parameter does not exist may cause a warning message to be output.
|
|
This option can be specified multiple times to override multiple
|
|
parameters. String values must be passed in double quotes (").
|
|
|
|
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\_braminit -- iCE40: perform SB\_RAM40\_4K initialization from file}
|
|
\label{cmd:ice40_braminit}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
ice40_braminit
|
|
|
|
This command processes all SB_RAM40_4K blocks with a non-empty INIT_FILE
|
|
parameter and converts it into the required INIT_x attributes
|
|
\end{lstlisting}
|
|
|
|
\section{ice40\_dsp -- iCE40: map multipliers}
|
|
\label{cmd:ice40_dsp}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
ice40_dsp [options] [selection]
|
|
|
|
Map multipliers ($mul/SB_MAC16) and multiply-accumulate ($mul/SB_MAC16 + $add)
|
|
cells into iCE40 DSP resources.
|
|
Currently, only the 16x16 multiply mode is supported and not the 2 x 8x8 mode.
|
|
|
|
Pack input registers (A, B, {C,D}; with optional hold), pipeline registers
|
|
({F,J,K,G}, H), output registers (O -- full 32-bits or lower 16-bits only; with
|
|
optional hold), and post-adder into into the SB_MAC16 resource.
|
|
|
|
Multiply-accumulate operations using the post-adder with feedback on the {C,D}
|
|
input will be folded into the DSP. In this scenario only, resetting the
|
|
the accumulator to an arbitrary value can be inferred to use the {C,D} input.
|
|
\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>
|
|
\end{lstlisting}
|
|
|
|
\section{ice40\_wrapcarry -- iCE40: wrap carries}
|
|
\label{cmd:ice40_wrapcarry}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
ice40_wrapcarry [selection]
|
|
|
|
Wrap manually instantiated SB_CARRY cells, along with their associated SB_LUT4s,
|
|
into an internal $__ICE40_CARRY_WRAPPER cell for preservation across technology
|
|
mapping.
|
|
|
|
Attributes on both cells will have their names prefixed with 'SB_CARRY.' or
|
|
'SB_LUT4.' and attached to the wrapping cell.
|
|
A (* keep *) attribute on either cell will be logically OR-ed together.
|
|
|
|
-unwrap
|
|
unwrap $__ICE40_CARRY_WRAPPER cells back into SB_CARRYs and SB_LUT4s,
|
|
including restoring their attributes.
|
|
\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.
|
|
|
|
-ignore <celltype> <portname>[:<portname>]*
|
|
Skips mapping inputs/outputs that are already connected to given
|
|
ports of the given cell. Can be used multiple times. This is in
|
|
addition to the cells specified as mapping targets.
|
|
|
|
-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
|
|
|
|
-compat-int
|
|
emit 32-bit or smaller fully-defined parameter values directly
|
|
as JSON numbers (for compatibility with old parsers)
|
|
|
|
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{logger -- set logger properties}
|
|
\label{cmd:logger}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
logger [options]
|
|
|
|
This command sets global logger properties, also available using command line
|
|
options.
|
|
|
|
-[no]time
|
|
enable/disable display of timestamp in log output.
|
|
|
|
-[no]stderr
|
|
enable/disable logging errors to stderr.
|
|
|
|
-warn regex
|
|
print a warning for all log messages matching the regex.
|
|
|
|
-nowarn regex
|
|
if a warning message matches the regex, it is printed as regular
|
|
message instead.
|
|
|
|
-werror regex
|
|
if a warning message matches the regex, it is printed as error
|
|
message instead and the tool terminates with a nonzero return code.
|
|
|
|
-[no]debug
|
|
globally enable/disable debug log messages.
|
|
|
|
-experimental <feature>
|
|
do not print warnings for the specified experimental feature
|
|
|
|
-expect <type> <regex> <expected_count>
|
|
expect log,warning or error to appear. In case of error return code is 0.
|
|
|
|
-expect-no-warnings
|
|
gives error in case there is at least one warning that is not expected.
|
|
\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:
|
|
|
|
opt_mem
|
|
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 configuration options, a set of block ram description
|
|
and a sequence of match rules.
|
|
|
|
The option 'attr_icase' configures how attribute values are matched. The value 0
|
|
means case-sensitive, 1 means case-insensitive.
|
|
|
|
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)
|
|
|
|
A match containing the command 'attribute' followed by a list of space
|
|
separated 'name[=string_value]' values requires that the memory contains any
|
|
one of the given attribute name and string values (where specified), or name
|
|
and integer 1 value (if no string_value given, since Verilog will interpret
|
|
'(* attr *)' as '(* attr=1 *)').
|
|
A name prefixed with '!' indicates that the attribute must not exist.
|
|
|
|
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 [options] [selection]
|
|
|
|
This pass converts multiport memory cells as generated by the memory_collect
|
|
pass to word-wide DFFs and address decoders.
|
|
|
|
-attr !<name>
|
|
do not map memories that have attribute <name> set.
|
|
|
|
-attr <name>[=<value>]
|
|
for memories that have attribute <name> set, only map them if its value
|
|
is a string <value> (if specified), or an integer 1 (otherwise). if this
|
|
option is specified multiple times, map the memory if the attribute is
|
|
to any of the values.
|
|
|
|
-iattr
|
|
for -attr, ignore case of <value>.
|
|
\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 -wb; 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 -wb; opt_expr -keepdc -undriven;;' on the miter circuit.
|
|
\end{lstlisting}
|
|
|
|
\section{mutate -- generate or apply design mutations}
|
|
\label{cmd:mutate}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
mutate -list N [options] [selection]
|
|
|
|
Create a list of N mutations using an even sampling.
|
|
|
|
-o filename
|
|
Write list to this file instead of console output
|
|
|
|
-s filename
|
|
Write a list of all src tags found in the design to the specified file
|
|
|
|
-seed N
|
|
RNG seed for selecting mutations
|
|
|
|
-none
|
|
Include a "none" mutation in the output
|
|
|
|
-ctrl name width value
|
|
Add -ctrl options to the output. Use 'value' for first mutation, then
|
|
simply count up from there.
|
|
|
|
-mode name
|
|
-module name
|
|
-cell name
|
|
-port name
|
|
-portbit int
|
|
-ctrlbit int
|
|
-wire name
|
|
-wirebit int
|
|
-src string
|
|
Filter list of mutation candidates to those matching
|
|
the given parameters.
|
|
|
|
-cfg option int
|
|
Set a configuration option. Options available:
|
|
weight_pq_w weight_pq_b weight_pq_c weight_pq_s
|
|
weight_pq_mw weight_pq_mb weight_pq_mc weight_pq_ms
|
|
weight_cover pick_cover_prcnt
|
|
|
|
|
|
mutate -mode MODE [options]
|
|
|
|
Apply the given mutation.
|
|
|
|
-ctrl name width value
|
|
Add a control signal with the given name and width. The mutation is
|
|
activated if the control signal equals the given value.
|
|
|
|
-module name
|
|
-cell name
|
|
-port name
|
|
-portbit int
|
|
-ctrlbit int
|
|
Mutation parameters, as generated by 'mutate -list N'.
|
|
|
|
-wire name
|
|
-wirebit int
|
|
-src string
|
|
Ignored. (They are generated by -list for documentation purposes.)
|
|
\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[=cost], -mux8[=cost], -mux16[=cost]
|
|
Cover $_MUX_ trees using the specified types of MUXes (with optional
|
|
integer costs). If none of these options are given, the effect is the
|
|
same as if all of them are.
|
|
Default costs: $_MUX4_ = 220, $_MUX8_ = 460,
|
|
$_MUX16_ = 940
|
|
|
|
-mux2=cost
|
|
Use the specified cost for $_MUX_ cells when making covering decisions.
|
|
Default cost: $_MUX_ = 100
|
|
|
|
-dmux=cost
|
|
Use the specified cost for $_MUX_ cells used in decoders.
|
|
Default cost: 90
|
|
|
|
-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.
|
|
|
|
-nopartial
|
|
Do not consider mappings that use $_MUX<N>_ to select from less
|
|
than <N> different signals.
|
|
\end{lstlisting}
|
|
|
|
\section{muxpack -- \$mux/\$pmux cascades to \$pmux}
|
|
\label{cmd:muxpack}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
muxpack [selection]
|
|
|
|
This pass converts cascaded chains of $pmux cells (e.g. those create from case
|
|
constructs) and $mux cells (e.g. those created by if-else constructs) into
|
|
$pmux cells.
|
|
|
|
This optimisation is conservative --- it will only pack $mux or $pmux cells
|
|
whose select lines are driven by '$eq' cells with other such cells if it can be
|
|
certain that their select inputs are mutually exclusive.
|
|
\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{onehot -- optimize \$eq cells for onehot signals}
|
|
\label{cmd:onehot}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
onehot [options] [selection]
|
|
|
|
This pass optimizes $eq cells that compare one-hot signals against constants
|
|
|
|
-v, -vv
|
|
verbose output
|
|
\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_share (-full only)
|
|
opt_rmdff [-keepdc] [-sat]
|
|
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] [-sat]
|
|
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 rewriting.
|
|
|
|
-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\_lut -- optimize LUT cells}
|
|
\label{cmd:opt_lut}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
opt_lut [options] [selection]
|
|
|
|
This pass combines cascaded $lut cells with unused inputs.
|
|
|
|
-dlogic <type>:<cell-port>=<LUT-input>[:<cell-port>=<LUT-input>...]
|
|
preserve connections to dedicated logic cell <type> that has ports
|
|
<cell-port> connected to LUT inputs <LUT-input>. this includes
|
|
the case where both LUT and dedicated logic input are connected to
|
|
the same constant.
|
|
|
|
-limit N
|
|
only perform the first N combines, then stop. useful for debugging.
|
|
\end{lstlisting}
|
|
|
|
\section{opt\_lut\_ins -- discard unused LUT inputs}
|
|
\label{cmd:opt_lut_ins}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
opt_lut_ins [options] [selection]
|
|
|
|
This pass removes unused inputs from LUT cells (that is, inputs that can not
|
|
influence the output signal given this LUT's value). While such LUTs cannot
|
|
be directly emitted by ABC, they can be a result of various post-ABC
|
|
transformations, such as mapping wide LUTs (not all sub-LUTs will use the
|
|
full set of inputs) or optimizations such as xilinx_dffopt.
|
|
|
|
-tech <technology>
|
|
Instead of generic $lut cells, operate on LUT cells specific
|
|
to the given technology. Valid values are: xilinx, ecp5, gowin.
|
|
\end{lstlisting}
|
|
|
|
\section{opt\_mem -- optimize memories}
|
|
\label{cmd:opt_mem}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
opt_mem [options] [selection]
|
|
|
|
This pass performs various optimizations on memories in the design.
|
|
\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] [-sat] [selection]
|
|
|
|
This pass identifies flip-flops with constant inputs and replaces them with
|
|
a constant driver.
|
|
|
|
-sat
|
|
additionally invoke SAT solver to detect and remove flip-flops (with
|
|
non-constant inputs) that can also be replaced with a constant driver
|
|
\end{lstlisting}
|
|
|
|
\section{opt\_share -- merge mutually exclusive cells of the same type that share an input signal}
|
|
\label{cmd:opt_share}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
opt_share [selection]
|
|
|
|
This pass identifies mutually exclusive cells of the same type that:
|
|
(a) share an input signal,
|
|
(b) drive the same $mux, $_MUX_, or $pmux multiplexing cell,
|
|
|
|
allowing the cell to be merged and the multiplexer to be moved from
|
|
multiplexing its output to multiplexing the non-shared input signals.
|
|
\end{lstlisting}
|
|
|
|
\section{paramap -- renaming cell parameters}
|
|
\label{cmd:paramap}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
paramap [options] [selection]
|
|
|
|
This command renames cell parameters and/or maps 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.
|
|
|
|
For example, mapping Diamond-style ECP5 "init" attributes to Yosys-style:
|
|
|
|
paramap -tocase INIT t:LUT4
|
|
\end{lstlisting}
|
|
|
|
\section{peepopt -- collection of peephole optimizers}
|
|
\label{cmd:peepopt}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
peepopt [options] [selection]
|
|
|
|
This pass applies a collection of peephole optimizers to the current design.
|
|
\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{pmux2shiftx -- transform \$pmux cells to \$shiftx cells}
|
|
\label{cmd:pmux2shiftx}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
pmux2shiftx [options] [selection]
|
|
|
|
This pass transforms $pmux cells to $shiftx cells.
|
|
|
|
-v, -vv
|
|
verbose output
|
|
|
|
-min_density <percentage>
|
|
specifies the minimum density for the shifter
|
|
default: 50
|
|
|
|
-min_choices <int>
|
|
specified the minimum number of choices for a control signal
|
|
default: 3
|
|
|
|
-onehot ignore|pmux|shiftx
|
|
select strategy for one-hot encoded control signals
|
|
default: pmux
|
|
|
|
-norange
|
|
disable $sub inference for "range decoders"
|
|
\end{lstlisting}
|
|
|
|
\section{pmuxtree -- transform \$pmux cells to trees of \$mux cells}
|
|
\label{cmd:pmuxtree}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
pmuxtree [selection]
|
|
|
|
This pass transforms $pmux cells to trees of $mux cells.
|
|
\end{lstlisting}
|
|
|
|
\section{portlist -- list (top-level) ports}
|
|
\label{cmd:portlist}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
portlist [options] [selection]
|
|
|
|
This command lists all module ports found in the selected modules.
|
|
|
|
If no selection is provided then it lists the ports on the top module.
|
|
|
|
-m
|
|
print verilog blackbox module definitions instead of port lists
|
|
\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 -keepdc [-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_prune
|
|
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 [options] [selection]
|
|
|
|
-quiet
|
|
do not print any messages.
|
|
|
|
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\_prune -- remove redundant assignments}
|
|
\label{cmd:proc_prune}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
proc_prune [selection]
|
|
|
|
This pass identifies assignments in processes that are always overwritten by
|
|
a later assignment to the same signal and removes them.
|
|
\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.
|
|
|
|
|
|
read -verific
|
|
read -noverific
|
|
|
|
Subsequent calls to 'read' will either use or not use Verific. Calling 'read'
|
|
with -verific will result in an error on Yosys binaries that are built without
|
|
Verific support. The default is to use Verific if it is available.
|
|
\end{lstlisting}
|
|
|
|
\section{read\_aiger -- read AIGER file}
|
|
\label{cmd:read_aiger}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
read_aiger [options] [filename]
|
|
|
|
Load module from an AIGER file into the current design.
|
|
|
|
-module_name <module_name>
|
|
name of module to be created (default: <filename>)
|
|
|
|
-clk_name <wire_name>
|
|
if specified, AIGER latches to be transformed into $_DFF_P_ cells
|
|
clocked by wire of this name. otherwise, $_FF_ cells will be used
|
|
|
|
-map <filename>
|
|
read file with port and latch symbols
|
|
|
|
-wideports
|
|
merge ports that match the pattern 'name[int]' into a single
|
|
multi-bit port 'name'
|
|
|
|
-xaiger
|
|
read XAIGER extensions
|
|
\end{lstlisting}
|
|
|
|
\section{read\_blif -- read BLIF file}
|
|
\label{cmd:read_blif}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
read_blif [options] [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.)
|
|
|
|
-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
|
|
|
|
-lib
|
|
only create empty blackbox modules
|
|
\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
|
|
|
|
-noassert
|
|
ignore assert() statements
|
|
|
|
-noassume
|
|
ignore assume() statements
|
|
|
|
-norestrict
|
|
ignore restrict() statements
|
|
|
|
-assume-asserts
|
|
treat all assert() statements like assume() statements
|
|
|
|
-assert-assumes
|
|
treat all assume() statements like assert() statements
|
|
|
|
-debug
|
|
alias for -dump_ast1 -dump_ast2 -dump_vlog1 -dump_vlog2 -yydebug
|
|
|
|
-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_vlog1
|
|
dump ast as Verilog code (before simplification)
|
|
|
|
-dump_vlog2
|
|
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.
|
|
|
|
-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
|
|
|
|
-noblackbox
|
|
do not automatically add a (* blackbox *) attribute to an
|
|
empty module.
|
|
|
|
-lib
|
|
only create empty blackbox modules. This implies -DBLACKBOX.
|
|
modules with the (* whitebox *) attribute will be preserved.
|
|
(* lib_whitebox *) will be treated like (* whitebox *).
|
|
|
|
-nowb
|
|
delete (* whitebox *) and (* lib_whitebox *) attributes from
|
|
all modules.
|
|
|
|
-specify
|
|
parse and import specify blocks
|
|
|
|
-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
|
|
|
|
-pwires
|
|
add a wire for each module parameter
|
|
|
|
-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 -output old_name new_name
|
|
|
|
Like above, but also make the wire an output. This will fail if the object is
|
|
not a wire.
|
|
|
|
|
|
rename -src [selection]
|
|
|
|
Assign names auto-generated from the src attribute to all selected wires and
|
|
cells with private names.
|
|
|
|
|
|
rename -wire [selection]
|
|
|
|
Assign auto-generated names based on the wires they drive to all selected
|
|
cells with private names. Ignores cells driving privatly named wires.
|
|
|
|
|
|
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{scratchpad -- get/set values in the scratchpad}
|
|
\label{cmd:scratchpad}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
scratchpad [options]
|
|
|
|
This pass allows to read and modify values from the scratchpad of the current
|
|
design. Options:
|
|
|
|
-get <identifier>
|
|
print the value saved in the scratchpad under the given identifier.
|
|
|
|
-set <identifier> <value>
|
|
save the given value in the scratchpad under the given identifier.
|
|
|
|
-unset <identifier>
|
|
remove the entry for the given identifier from the scratchpad.
|
|
|
|
-copy <identifier_from> <identifier_to>
|
|
copy the value of the first identifier to the second identifier.
|
|
|
|
-assert <identifier> <value>
|
|
assert that the entry for the given identifier is set to the given value.
|
|
|
|
-assert-set <identifier>
|
|
assert that the entry for the given identifier exists.
|
|
|
|
-assert-unset <identifier>
|
|
assert that the entry for the given identifier does not exist.
|
|
|
|
The identifier may not contain whitespace. By convention, it is usually prefixed
|
|
by the name of the pass that uses it, e.g. 'opt.did_something'. If the value
|
|
contains whitespace, it must be enclosed in double quotes.
|
|
\end{lstlisting}
|
|
|
|
\section{script -- execute commands from file or wire}
|
|
\label{cmd:script}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
script <filename> [<from_label>:<to_label>]
|
|
script -scriptwire [selection]
|
|
|
|
This command executes the yosys commands in the specified file (default
|
|
behaviour), or commands embedded in the constant text value connected to the
|
|
selected wires.
|
|
|
|
In the default (file) case, the 2nd argument can be used to only execute the
|
|
section of the file between the specified labels. An empty from label is
|
|
synonymous with the beginning of the file and an empty to label is synonymous
|
|
with 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.
|
|
|
|
In "-scriptwire" mode, the commands on the selected wire(s) will be executed
|
|
in the scope of (and thus, relative to) the wires' owning module(s). This
|
|
'-module' mode can be exited by using the 'cd' command.
|
|
\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 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
|
|
|
|
N:<pattern>
|
|
all modules with a name matching the given pattern
|
|
(i.e. 'N:' is optional as it is the default matching rule)
|
|
|
|
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 as seed
|
|
value for the random number generator.
|
|
|
|
-init
|
|
also create/update init values for flip-flops
|
|
|
|
-params
|
|
replace undef in cell parameters
|
|
\end{lstlisting}
|
|
|
|
\section{sf2\_iobs -- SF2: insert IO buffers}
|
|
\label{cmd:sf2_iobs}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
sf2_iobs [options] [selection]
|
|
|
|
Add SF2 I/O buffers and global buffers to top module as needed.
|
|
|
|
-clkbuf
|
|
Insert PAD->global_net clock buffers
|
|
\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 buses 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
|
|
|
|
-nobg
|
|
don't run viewer in the background, IE wait for the viewer tool to
|
|
exit before returning
|
|
|
|
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
|
|
|
|
-tech <technology>
|
|
print area estemate for the specified technology. Currently supported
|
|
values for <technology>: xilinx, cmos
|
|
|
|
-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 [options] [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.
|
|
|
|
-copy
|
|
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.
|
|
|
|
-name <name>
|
|
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 instead.
|
|
|
|
-hidden
|
|
instead of creating submodule ports with public names, create ports with
|
|
private names so that a subsequent 'flatten; clean' call will restore the
|
|
original module with original public names.
|
|
\end{lstlisting}
|
|
|
|
\section{supercover -- add hi/lo cover cells for each wire bit}
|
|
\label{cmd:supercover}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
supercover [options] [selection]
|
|
|
|
This command adds two cover cells for each bit of each selected wire, one
|
|
checking for a hi signal level and one checking for lo level.
|
|
\end{lstlisting}
|
|
|
|
\section{synth -- generic synthesis script}
|
|
\label{cmd:synth}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth [options]
|
|
|
|
This command runs the default synthesis script. 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.
|
|
|
|
-encfile <file>
|
|
passed to 'fsm_recode' via 'fsm'
|
|
|
|
-lut <k>
|
|
perform synthesis for a k-LUT architecture.
|
|
|
|
-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.
|
|
|
|
-abc9
|
|
use new ABC9 flow (EXPERIMENTAL)
|
|
|
|
-flowmap
|
|
use FlowMap LUT techmapping instead of ABC
|
|
|
|
|
|
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
|
|
peepopt
|
|
opt_clean
|
|
techmap -map +/cmp2lut.v -map +/cmp2lcu.v (if -lut)
|
|
alumacc (unless -noalumacc)
|
|
share (unless -noshare)
|
|
opt
|
|
fsm (unless -nofsm)
|
|
opt -fast
|
|
memory -nomap
|
|
opt_clean
|
|
|
|
fine:
|
|
opt -fast -full
|
|
memory_map
|
|
opt -full
|
|
techmap
|
|
techmap -map +/gate2lut.v (if -noabc and -lut)
|
|
clean; opt_lut (if -noabc and -lut)
|
|
flowmap -maxlut K (if -flowmap and -lut)
|
|
opt -fast
|
|
abc -fast (unless -noabc, unless -lut)
|
|
abc -fast -lut k (unless -noabc, if -lut)
|
|
opt -fast (unless -noabc)
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.}
|
|
\label{cmd:synth_achronix}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_achronix [options]
|
|
|
|
This command runs synthesis for Achronix Speedster eFPGAs. This work is still 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.
|
|
|
|
-noflatten
|
|
do not flatten design before synthesis
|
|
|
|
-retime
|
|
run 'abc' with '-dff -D 1' options
|
|
|
|
|
|
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
|
|
dff2dffe -direct-match $_DFF_*
|
|
opt -fine
|
|
techmap -map +/techmap.v
|
|
opt -full
|
|
clean -purge
|
|
setundef -undriven -zero
|
|
abc -markgroups -dff -D 1 (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{synth\_anlogic -- synthesis for Anlogic FPGAs}
|
|
\label{cmd:synth_anlogic}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_anlogic [options]
|
|
|
|
This command runs synthesis for Anlogic FPGAs.
|
|
|
|
-top <module>
|
|
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.
|
|
|
|
-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 -D 1' options
|
|
|
|
-nolutram
|
|
do not use EG_LOGIC_DRAM16X4 cells in output netlist
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/anlogic/cells_sim.v +/anlogic/eagle_bb.v
|
|
hierarchy -check -top <top>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
|
|
map_lutram: (skip if -nolutram)
|
|
memory_bram -rules +/anlogic/lutrams.txt
|
|
techmap -map +/anlogic/lutrams_map.v
|
|
setundef -zero -params t:EG_LOGIC_DRAM16X4
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map
|
|
opt -undriven -fine
|
|
|
|
map_gates:
|
|
techmap -map +/techmap.v -map +/anlogic/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
|
|
map_ffs:
|
|
techmap -D NO_LUT -map +/anlogic/cells_map.v
|
|
dffinit -strinit SET RESET -ff AL_MAP_SEQ q REGSET -noreinit
|
|
opt_expr -mux_undef
|
|
simplemap
|
|
|
|
map_luts:
|
|
abc -lut 4:6
|
|
clean
|
|
|
|
map_cells:
|
|
techmap -map +/anlogic/cells_map.v
|
|
clean
|
|
|
|
map_anlogic:
|
|
anlogic_fixcarry
|
|
anlogic_eqn
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
edif:
|
|
write_edif <file-name>
|
|
|
|
json:
|
|
write_json <file-name>
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs}
|
|
\label{cmd:synth_coolrunner2}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_coolrunner2 [options]
|
|
|
|
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.
|
|
|
|
-top <module>
|
|
use the specified module as top module (default='top')
|
|
|
|
-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 -D 1' options
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/coolrunner2/cells_sim.v
|
|
hierarchy -check -top <top>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
|
|
fine:
|
|
extract_counter -dir up -allow_arst no
|
|
techmap -map +/coolrunner2/cells_counter_map.v
|
|
clean
|
|
opt -fast -full
|
|
techmap -map +/techmap.v -map +/coolrunner2/cells_latch.v
|
|
opt -fast
|
|
dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib
|
|
|
|
map_tff:
|
|
abc -g AND,XOR
|
|
clean
|
|
extract -map +/coolrunner2/tff_extract.v
|
|
|
|
map_pla:
|
|
abc -sop -I 40 -P 56
|
|
clean
|
|
|
|
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
|
|
clean
|
|
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:*
|
|
coolrunner2_fixup
|
|
splitnets
|
|
clean
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
json:
|
|
write_json <file-name>
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_easic -- synthesis for eASIC platform}
|
|
\label{cmd:synth_easic}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_easic [options]
|
|
|
|
This command runs synthesis for eASIC platform.
|
|
|
|
-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 -D 1' options
|
|
|
|
|
|
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 -D 1 (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{synth\_ecp5 -- synthesis for ECP5 FPGAs}
|
|
\label{cmd:synth_ecp5}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_ecp5 [options]
|
|
|
|
This command runs synthesis for ECP5 FPGAs.
|
|
|
|
-top <module>
|
|
use the specified module as top module
|
|
|
|
-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.
|
|
|
|
-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 -D 1' options
|
|
|
|
-noccu2
|
|
do not use CCU2 cells in output netlist
|
|
|
|
-nodffe
|
|
do not use flipflops with CE in output netlist
|
|
|
|
-nobram
|
|
do not use block RAM cells in output netlist
|
|
|
|
-nolutram
|
|
do not use LUT RAM cells in output netlist
|
|
|
|
-nowidelut
|
|
do not use PFU muxes to implement LUTs larger than LUT4s
|
|
|
|
-asyncprld
|
|
use async PRLD mode to implement DLATCH and DFFSR (EXPERIMENTAL)
|
|
|
|
-abc2
|
|
run two passes of 'abc' for slightly improved logic density
|
|
|
|
-abc9
|
|
use new ABC9 flow (EXPERIMENTAL)
|
|
|
|
-vpr
|
|
generate an output netlist (and BLIF file) suitable for VPR
|
|
(this feature is experimental and incomplete)
|
|
|
|
-nodsp
|
|
do not map multipliers to MULT18X18D
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib -specify +/ecp5/cells_sim.v +/ecp5/cells_bb.v
|
|
hierarchy -check -top <top>
|
|
|
|
coarse:
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
opt_expr
|
|
opt_clean
|
|
check
|
|
opt
|
|
wreduce
|
|
peepopt
|
|
opt_clean
|
|
share
|
|
techmap -map +/cmp2lut.v -D LUT_WIDTH=4
|
|
opt_expr
|
|
opt_clean
|
|
techmap -map +/mul2dsp.v -map +/ecp5/dsp_map.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_NAME=$__MUL18X18 (unless -nodsp)
|
|
chtype -set $mul t:$__soft_mul (unless -nodsp)
|
|
alumacc
|
|
opt
|
|
fsm
|
|
opt -fast
|
|
memory -nomap
|
|
opt_clean
|
|
|
|
map_bram: (skip if -nobram)
|
|
memory_bram -rules +/ecp5/brams.txt
|
|
techmap -map +/ecp5/brams_map.v
|
|
|
|
map_lutram: (skip if -nolutram)
|
|
memory_bram -rules +/ecp5/lutrams.txt
|
|
techmap -map +/ecp5/lutrams_map.v
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
|
|
opt -undriven -fine
|
|
|
|
map_gates:
|
|
techmap -map +/techmap.v -map +/ecp5/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
|
|
map_ffs:
|
|
dff2dffs
|
|
opt_clean
|
|
dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
|
|
techmap -D NO_LUT [-D ASYNC_PRLD] -map +/ecp5/cells_map.v
|
|
opt_expr -undriven -mux_undef
|
|
simplemap
|
|
ecp5_ffinit
|
|
ecp5_gsr
|
|
attrmvcp -copy -attr syn_useioff
|
|
opt_clean
|
|
|
|
map_luts:
|
|
abc (only if -abc2)
|
|
techmap -map +/ecp5/latches_map.v
|
|
abc -lut 4:7 -dress
|
|
clean
|
|
|
|
map_cells:
|
|
techmap -map +/ecp5/cells_map.v (with -D NO_LUT in vpr mode)
|
|
opt_lut_ins -tech ecp5
|
|
clean
|
|
|
|
check:
|
|
autoname
|
|
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{synth\_efinix -- synthesis for Efinix FPGAs}
|
|
\label{cmd:synth_efinix}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_efinix [options]
|
|
|
|
This command runs synthesis for Efinix FPGAs.
|
|
|
|
-top <module>
|
|
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.
|
|
|
|
-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 -D 1' options
|
|
|
|
-nobram
|
|
do not use EFX_RAM_5K cells in output netlist
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/efinix/cells_sim.v
|
|
hierarchy -check -top <top>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
memory_bram -rules +/efinix/brams.txt
|
|
techmap -map +/efinix/brams_map.v
|
|
setundef -zero -params t:EFX_RAM_5K
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map
|
|
opt -undriven -fine
|
|
|
|
map_gates:
|
|
techmap -map +/techmap.v -map +/efinix/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
|
|
map_ffs:
|
|
techmap -D NO_LUT -map +/efinix/cells_map.v
|
|
dffinit -strinit SET RESET -ff AL_MAP_SEQ q REGSET -noreinit
|
|
opt_expr -mux_undef
|
|
simplemap
|
|
|
|
map_luts:
|
|
abc -lut 4
|
|
clean
|
|
|
|
map_cells:
|
|
techmap -map +/efinix/cells_map.v
|
|
clean
|
|
|
|
map_gbuf:
|
|
efinix_gbuf
|
|
efinix_fixcarry
|
|
clean
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
edif:
|
|
write_edif <file-name>
|
|
|
|
json:
|
|
write_json <file-name>
|
|
\end{lstlisting}
|
|
|
|
\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.
|
|
|
|
-nodffe
|
|
do not use flipflops with CE in output netlist
|
|
|
|
-nobram
|
|
do not use BRAM cells in output netlist
|
|
|
|
-nolutram
|
|
do not use distributed RAM cells in output netlist
|
|
|
|
-noflatten
|
|
do not flatten design before synthesis
|
|
|
|
-retime
|
|
run 'abc' with '-dff -D 1' options
|
|
|
|
-nowidelut
|
|
do not use muxes to implement LUTs larger than LUT4s
|
|
|
|
-noiopads
|
|
do not emit IOB at top level ports
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/gowin/cells_sim.v
|
|
hierarchy -check -top <top>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
|
|
map_bram: (skip if -nobram)
|
|
memory_bram -rules +/gowin/brams.txt
|
|
techmap -map +/gowin/brams_map.v
|
|
|
|
map_lutram: (skip if -nolutram)
|
|
memory_bram -rules +/gowin/lutrams.txt
|
|
techmap -map +/gowin/lutrams_map.v
|
|
determine_init
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map
|
|
opt -undriven -fine
|
|
|
|
map_gates:
|
|
techmap -map +/techmap.v -map +/gowin/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
splitnets
|
|
|
|
map_ffs:
|
|
dff2dffs -match-init
|
|
opt_clean
|
|
dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
|
|
techmap -map +/gowin/cells_map.v
|
|
opt_expr -mux_undef
|
|
simplemap
|
|
|
|
map_luts:
|
|
abc -lut 4:8
|
|
clean
|
|
|
|
map_cells:
|
|
techmap -map +/gowin/cells_map.v
|
|
opt_lut_ins -tech gowin
|
|
setundef -undriven -params -zero
|
|
hilomap -singleton -hicell VCC V -locell GND G
|
|
iopadmap -bits -inpad IBUF O:I -outpad OBUF I:O -toutpad TBUF OEN:I:O -tinoutpad IOBUF OEN:O:I:IO (unless -noiopads)
|
|
clean
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
vout:
|
|
write_verilog -decimal -attr2comment -defparam -renameprefix gen <file-name>
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs}
|
|
\label{cmd:synth_greenpak4}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_greenpak4 [options]
|
|
|
|
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.
|
|
|
|
-top <module>
|
|
use the specified module as top module (default='top')
|
|
|
|
-part <part>
|
|
synthesize for the specified part. Valid values are SLG46140V,
|
|
SLG46620V, and SLG46621V (default).
|
|
|
|
-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 -D 1' options
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/greenpak4/cells_sim.v
|
|
hierarchy -check -top <top>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
|
|
fine:
|
|
extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14
|
|
clean
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map
|
|
opt -undriven -fine
|
|
techmap -map +/techmap.v -map +/greenpak4/cells_latch.v
|
|
dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
|
|
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
|
|
|
|
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
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
json:
|
|
write_json <file-name>
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_ice40 -- synthesis for iCE40 FPGAs}
|
|
\label{cmd:synth_ice40}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_ice40 [options]
|
|
|
|
This command runs synthesis for iCE40 FPGAs.
|
|
|
|
-device < hx | lp | u >
|
|
relevant only for '-abc9' flow, optimise timing for the specified device.
|
|
default: hx
|
|
|
|
-top <module>
|
|
use the specified module as top module
|
|
|
|
-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.
|
|
|
|
-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 -D 1' options
|
|
|
|
-nocarry
|
|
do not use SB_CARRY cells in output netlist
|
|
|
|
-nodffe
|
|
do not use SB_DFFE* cells in output netlist
|
|
|
|
-dffe_min_ce_use <min_ce_use>
|
|
do not use SB_DFFE* cells if the resulting CE line would go to less
|
|
than min_ce_use SB_DFFE* in output netlist
|
|
|
|
-nobram
|
|
do not use SB_RAM40_4K* cells in output netlist
|
|
|
|
-dsp
|
|
use iCE40 UltraPlus DSP cells for large arithmetic
|
|
|
|
-noabc
|
|
use built-in Yosys LUT techmapping instead of abc
|
|
|
|
-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)
|
|
|
|
-abc9
|
|
use new ABC9 flow (EXPERIMENTAL)
|
|
|
|
-flowmap
|
|
use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -D ICE40_HX -lib -specify +/ice40/cells_sim.v
|
|
hierarchy -check -top <top>
|
|
proc
|
|
|
|
flatten: (unless -noflatten)
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
|
|
coarse:
|
|
opt_expr
|
|
opt_clean
|
|
check
|
|
opt
|
|
wreduce
|
|
peepopt
|
|
opt_clean
|
|
share
|
|
techmap -map +/cmp2lut.v -D LUT_WIDTH=4
|
|
opt_expr
|
|
opt_clean
|
|
memory_dff
|
|
wreduce t:$mul
|
|
techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 -D DSP_NAME=$__MUL16X16 (if -dsp)
|
|
select a:mul2dsp (if -dsp)
|
|
setattr -unset mul2dsp (if -dsp)
|
|
opt_expr -fine (if -dsp)
|
|
wreduce (if -dsp)
|
|
select -clear (if -dsp)
|
|
ice40_dsp (if -dsp)
|
|
chtype -set $mul t:$__soft_mul (if -dsp)
|
|
alumacc
|
|
opt
|
|
fsm
|
|
opt -fast
|
|
memory -nomap
|
|
opt_clean
|
|
|
|
map_bram: (skip if -nobram)
|
|
memory_bram -rules +/ice40/brams.txt
|
|
techmap -map +/ice40/brams_map.v
|
|
ice40_braminit
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine
|
|
memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
|
|
opt -undriven -fine
|
|
|
|
map_gates:
|
|
ice40_wrapcarry
|
|
techmap -map +/techmap.v -map +/ice40/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
ice40_opt
|
|
|
|
map_ffs:
|
|
dff2dffe -direct-match $_DFF_*
|
|
techmap -D NO_LUT -D NO_ADDER -map +/ice40/cells_map.v
|
|
opt_expr -mux_undef
|
|
simplemap
|
|
ice40_ffinit
|
|
ice40_ffssr
|
|
ice40_opt -full
|
|
|
|
map_luts:
|
|
abc (only if -abc2)
|
|
ice40_opt (only if -abc2)
|
|
techmap -map +/ice40/latches_map.v
|
|
simplemap (if -noabc or -flowmap)
|
|
techmap -map +/gate2lut.v -D LUT_WIDTH=4 (only if -noabc)
|
|
flowmap -maxlut 4 (only if -flowmap)
|
|
abc -dress -lut 4 (skip if -noabc)
|
|
ice40_wrapcarry -unwrap
|
|
techmap -D NO_LUT -map +/ice40/cells_map.v
|
|
clean
|
|
opt_lut -dlogic SB_CARRY:I0=2:I1=1:CI=0
|
|
|
|
map_cells:
|
|
techmap -map +/ice40/cells_map.v (with -D NO_LUT in vpr mode)
|
|
clean
|
|
|
|
check:
|
|
autoname
|
|
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{synth\_intel -- synthesis for Intel (Altera) FPGAs.}
|
|
\label{cmd:synth_intel}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_intel [options]
|
|
|
|
This command runs synthesis for Intel FPGAs.
|
|
|
|
-family <max10 | arria10gx | cyclone10lp | cyclonev | cycloneiv | cycloneive>
|
|
generate the synthesis netlist for the specified family.
|
|
MAX10 is the default target if no family argument specified.
|
|
For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use cycloneive.
|
|
Cyclone V and Arria 10 GX devices are experimental.
|
|
|
|
-top <module>
|
|
use the specified module as top module (default='top')
|
|
|
|
-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.
|
|
Note that this backend has not been tested and is likely incompatible
|
|
with recent versions of Quartus.
|
|
|
|
-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.
|
|
|
|
-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.
|
|
|
|
-iopads
|
|
use IO pad cells in output netlist
|
|
|
|
-nobram
|
|
do not use block RAM cells in output netlist
|
|
|
|
-noflatten
|
|
do not flatten design before synthesis
|
|
|
|
-retime
|
|
run 'abc' with '-dff -D 1' options
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
|
|
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>
|
|
|
|
flatten: (unless -noflatten)
|
|
proc
|
|
flatten
|
|
tribuf -logic
|
|
deminout
|
|
|
|
coarse:
|
|
synth -run coarse
|
|
|
|
map_bram: (skip if -nobram)
|
|
memory_bram -rules +/intel/common/brams_m9k.txt (if applicable for family)
|
|
techmap -map +/intel/common/brams_map_m9k.v (if applicable for family)
|
|
|
|
map_ffram:
|
|
opt -fast -mux_undef -undriven -fine -full
|
|
memory_map
|
|
opt -undriven -fine
|
|
dff2dffe -direct-match $_DFF_*
|
|
opt -fine
|
|
techmap -map +/techmap.v
|
|
opt -full
|
|
clean -purge
|
|
setundef -undriven -zero
|
|
abc -markgroups -dff -D 1 (only if -retime)
|
|
|
|
map_luts:
|
|
abc -lut 4
|
|
clean
|
|
|
|
map_cells:
|
|
iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I (if -iopads)
|
|
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>
|
|
|
|
|
|
WARNING: THE 'synth_intel' COMMAND IS EXPERIMENTAL.
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_sf2 -- synthesis for SmartFusion2 and IGLOO2 FPGAs}
|
|
\label{cmd:synth_sf2}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_sf2 [options]
|
|
|
|
This command runs synthesis for SmartFusion2 and IGLOO2 FPGAs.
|
|
|
|
-top <module>
|
|
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.
|
|
|
|
-vlog <file>
|
|
write the design to the specified Verilog 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.
|
|
|
|
-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
|
|
|
|
-noiobs
|
|
run synthesis in "block mode", i.e. do not insert IO buffers
|
|
|
|
-clkbuf
|
|
insert direct PAD->global_net buffers
|
|
|
|
-retime
|
|
run 'abc' with '-dff -D 1' options
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib +/sf2/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
|
|
memory_map
|
|
opt -undriven -fine
|
|
techmap -map +/techmap.v -map +/sf2/arith_map.v
|
|
opt -fast
|
|
abc -dff -D 1 (only if -retime)
|
|
|
|
map_ffs:
|
|
techmap -D NO_LUT -map +/sf2/cells_map.v
|
|
opt_expr -mux_undef
|
|
simplemap
|
|
|
|
map_luts:
|
|
abc -lut 4
|
|
clean
|
|
|
|
map_cells:
|
|
techmap -map +/sf2/cells_map.v
|
|
clean
|
|
|
|
map_iobs:
|
|
sf2_iobs [-clkbuf] (unless -noiobs)
|
|
clean
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat
|
|
check -noinit
|
|
|
|
edif:
|
|
write_edif -gndvccy <file-name>
|
|
|
|
vlog:
|
|
write_verilog <file-name>
|
|
|
|
json:
|
|
write_json <file-name>
|
|
\end{lstlisting}
|
|
|
|
\section{synth\_xilinx -- synthesis for Xilinx FPGAs}
|
|
\label{cmd:synth_xilinx}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
synth_xilinx [options]
|
|
|
|
This command runs synthesis for Xilinx FPGAs. This command does not operate on
|
|
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
|
|
|
|
-family <family>
|
|
run synthesis for the specified Xilinx architecture
|
|
generate the synthesis netlist for the specified family.
|
|
supported values:
|
|
- xcup: Ultrascale Plus
|
|
- xcu: Ultrascale
|
|
- xc7: Series 7 (default)
|
|
- xc6s: Spartan 6
|
|
- xc6v: Virtex 6
|
|
- xc5v: Virtex 5 (EXPERIMENTAL)
|
|
- xc4v: Virtex 4 (EXPERIMENTAL)
|
|
- xc3sda: Spartan 3A DSP (EXPERIMENTAL)
|
|
- xc3sa: Spartan 3A (EXPERIMENTAL)
|
|
- xc3se: Spartan 3E (EXPERIMENTAL)
|
|
- xc3s: Spartan 3 (EXPERIMENTAL)
|
|
- xc2vp: Virtex 2 Pro (EXPERIMENTAL)
|
|
- xc2v: Virtex 2 (EXPERIMENTAL)
|
|
- xcve: Virtex E, Spartan 2E (EXPERIMENTAL)
|
|
- xcv: Virtex, Spartan 2 (EXPERIMENTAL)
|
|
|
|
-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)
|
|
|
|
-ise
|
|
generate an output netlist suitable for ISE
|
|
|
|
-nobram
|
|
do not use block RAM cells in output netlist
|
|
|
|
-nolutram
|
|
do not use distributed RAM cells in output netlist
|
|
|
|
-nosrl
|
|
do not use distributed SRL cells in output netlist
|
|
|
|
-nocarry
|
|
do not use XORCY/MUXCY/CARRY4 cells in output netlist
|
|
|
|
-nowidelut
|
|
do not use MUXF[5-9] resources to implement LUTs larger than native for the target
|
|
|
|
-nodsp
|
|
do not use DSP48*s to implement multipliers and associated logic
|
|
|
|
-noiopad
|
|
disable I/O buffer insertion (useful for hierarchical or
|
|
out-of-context flows)
|
|
|
|
-noclkbuf
|
|
disable automatic clock buffer insertion
|
|
|
|
-uram
|
|
infer URAM288s for large memories (xcup only)
|
|
|
|
-widemux <int>
|
|
enable inference of hard multiplexer resources (MUXF[78]) for muxes at or
|
|
above this number of inputs (minimum value 2, recommended value >= 5).
|
|
default: 0 (no inference)
|
|
|
|
-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
|
|
|
|
-dff
|
|
run 'abc'/'abc9' with -dff option
|
|
|
|
-retime
|
|
run 'abc' with '-D 1' option to enable flip-flop retiming.
|
|
implies -dff.
|
|
|
|
-abc9
|
|
use new ABC9 flow (EXPERIMENTAL)
|
|
|
|
|
|
The following commands are executed by this synthesis command:
|
|
|
|
begin:
|
|
read_verilog -lib -specify +/xilinx/cells_sim.v
|
|
read_verilog -lib +/xilinx/cells_xtra.v
|
|
hierarchy -check -auto-top
|
|
|
|
prepare:
|
|
proc
|
|
flatten (with '-flatten')
|
|
tribuf -logic
|
|
deminout
|
|
opt_expr
|
|
opt_clean
|
|
check
|
|
opt
|
|
wreduce [-keepdc] (option for '-widemux')
|
|
peepopt
|
|
opt_clean
|
|
muxpack ('-widemux' only)
|
|
pmux2shiftx (skip if '-nosrl' and '-widemux=0')
|
|
clean (skip if '-nosrl' and '-widemux=0')
|
|
|
|
map_dsp: (skip if '-nodsp')
|
|
memory_dff
|
|
techmap -map +/mul2dsp.v -map +/xilinx/{family}_dsp_map.v {options}
|
|
select a:mul2dsp
|
|
setattr -unset mul2dsp
|
|
opt_expr -fine
|
|
wreduce
|
|
select -clear
|
|
xilinx_dsp -family <family>
|
|
chtype -set $mul t:$__soft_mul
|
|
|
|
coarse:
|
|
techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=[46]
|
|
alumacc
|
|
share
|
|
opt
|
|
fsm
|
|
opt -fast
|
|
memory -nomap
|
|
opt_clean
|
|
|
|
map_uram: (only if '-uram')
|
|
memory_bram -rules +/xilinx/{family}_urams.txt
|
|
techmap -map +/xilinx/{family}_urams_map.v
|
|
|
|
map_bram: (skip if '-nobram')
|
|
memory_bram -rules +/xilinx/{family}_brams.txt
|
|
techmap -map +/xilinx/{family}_brams_map.v
|
|
|
|
map_lutram: (skip if '-nolutram')
|
|
memory_bram -rules +/xilinx/lut[46]_lutrams.txt
|
|
techmap -map +/xilinx/lutrams_map.v
|
|
|
|
map_ffram:
|
|
simplemap t:$dff t:$adff t:$mux
|
|
dff2dffs [-match-init] (-match-init for xc6s only)
|
|
opt -fast -full
|
|
memory_map
|
|
|
|
fine:
|
|
dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
|
|
muxcover <internal options> ('-widemux' only)
|
|
opt -full
|
|
xilinx_srl -variable -minlen 3 (skip if '-nosrl')
|
|
techmap -map +/techmap.v -D LUT_SIZE=[46] [-map +/xilinx/mux_map.v] -map +/xilinx/arith_map.v
|
|
opt -fast
|
|
|
|
map_cells:
|
|
iopadmap -bits -outpad OBUF I:O -inpad IBUF O:I -toutpad $__XILINX_TOUTPAD OE:I:O -tinoutpad $__XILINX_TINOUTPAD OE:O:I:IO A:top (skip if '-noiopad')
|
|
techmap -map +/techmap.v -map +/xilinx/cells_map.v
|
|
clean
|
|
|
|
map_ffs:
|
|
techmap -map +/xilinx/{family}_ff_map.v ('-abc9' only)
|
|
|
|
map_luts:
|
|
opt_expr -mux_undef
|
|
abc -luts 2:2,3,6:5[,10,20] [-dff] [-D 1] (option for 'nowidelut', '-dff', '-retime')
|
|
clean
|
|
xilinx_srl -fixed -minlen 3 (skip if '-nosrl')
|
|
techmap -map +/xilinx/lut_map.v -map +/xilinx/cells_map.v -map +/xilinx/{family}_ff_map.v -D LUT_WIDTH=[46]
|
|
xilinx_dffopt [-lut4]
|
|
opt_lut_ins -tech xilinx
|
|
|
|
finalize:
|
|
clkbufmap -buf BUFG O:I (skip if '-noclkbuf')
|
|
extractinv -inv INV O:I (only if '-ise')
|
|
clean
|
|
|
|
check:
|
|
hierarchy -check
|
|
stat -tech xilinx
|
|
check -noinit
|
|
|
|
edif:
|
|
write_edif -pvector bra
|
|
|
|
blif:
|
|
write_blif
|
|
\end{lstlisting}
|
|
|
|
\section{tcl -- execute a TCL script file}
|
|
\label{cmd:tcl}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
tcl <filename> [args]
|
|
|
|
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. 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.
|
|
|
|
If any arguments are specified, these arguments are provided to the script via
|
|
the standard $argc and $argv variables.
|
|
\end{lstlisting}
|
|
|
|
\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
|
|
file.
|
|
|
|
-map filename
|
|
the library of cell implementations to be used.
|
|
without this parameter a builtin library is used that
|
|
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 on each module.
|
|
default: unlimited
|
|
|
|
-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.
|
|
|
|
-wb
|
|
Ignore the 'whitebox' attribute on cell implementations.
|
|
|
|
-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. 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.
|
|
|
|
When a port on a module in the map file has the 'techmap_autopurge' attribute
|
|
set, and that port is not connected in the instantiation that is mapped, then
|
|
then a cell port connected only to such wires will be omitted in the mapped
|
|
version of the circuit.
|
|
|
|
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 special
|
|
wires are supported:
|
|
|
|
_TECHMAP_FAIL_
|
|
When this wire is set to a non-zero constant value, techmap will not
|
|
use this module and instead try the next module with a matching
|
|
'techmap_celltype' attribute.
|
|
|
|
When such a wire exists but does not have a constant value after all
|
|
_TECHMAP_DO_* commands have been executed, an error is generated.
|
|
|
|
_TECHMAP_DO_*
|
|
This wires are evaluated in alphabetical order. The constant text value
|
|
of this wire is a yosys command (or sequence of commands) that is run
|
|
by techmap on the module. A common use case is to run 'proc' on modules
|
|
that are written using always-statements.
|
|
|
|
When such a wire has a non-constant value at the time it is to be
|
|
evaluated, an error is produced. That means it is possible for such a
|
|
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; '.
|
|
|
|
_TECHMAP_REMOVEINIT_<port-name>_
|
|
When this wire is set to a constant value, the init attribute of the wire(s)
|
|
connected to this port will be consumed. This wire must have the same
|
|
width as the given port, and for every bit that is set to 1 in the value,
|
|
the corresponding init attribute bit will be changed to 1'bx. If all
|
|
bits of an init attribute are left as x, it will be removed.
|
|
|
|
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_WIREINIT_<port-name>_
|
|
When a parameter with this name exists, it will be set to the initial
|
|
value of the wire(s) connected to the given port, as specified by the init
|
|
attribute. If the attribute doesn't exist, x will be filled for the
|
|
missing bits. To remove the init attribute bits used, use the
|
|
_TECHMAP_REMOVEINIT_*_ wires.
|
|
|
|
_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.
|
|
A cell with a name of the form `_TECHMAP_REPLACE_.<suffix>` in the map file will
|
|
be named thus but with the `_TECHMAP_REPLACE_' prefix substituted with the name
|
|
of the cell being replaced.
|
|
Similarly, a wire named in the form `_TECHMAP_REPLACE_.<suffix>` will cause a
|
|
new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'
|
|
prefix also substituted.
|
|
|
|
See 'help extract' for a pass that does the opposite thing.
|
|
|
|
See 'help flatten' for a pass that does flatten the design (which is
|
|
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/subtract 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{test\_autotb -- generate simple test benches}
|
|
\label{cmd:test_autotb}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
test_autotb [options] [filename]
|
|
|
|
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.
|
|
|
|
This can be used to check the synthesis results for simple circuits by
|
|
comparing the testbench output for the input files and the synthesis results.
|
|
|
|
The backend automatically detects clock signals. Additionally a signal can
|
|
be forced to be interpreted as clock signal by setting the attribute
|
|
'gentb_clock' on the signal.
|
|
|
|
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.
|
|
|
|
The attribute 'gentb_skip' can be attached to modules to suppress testbench
|
|
generation.
|
|
|
|
-n <int>
|
|
number of iterations the test bench should run (default = 1000)
|
|
|
|
-seed <int>
|
|
seed used for pseudo-random number generation (default = 0).
|
|
a value of 0 will cause an arbitrary seed to be chosen, based on
|
|
the current system time.
|
|
\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{test\_pmgen -- test pass for pmgen}
|
|
\label{cmd:test_pmgen}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
test_pmgen -reduce_chain [options] [selection]
|
|
|
|
Demo for recursive pmgen patterns. Map chains of AND/OR/XOR to $reduce_*.
|
|
|
|
|
|
test_pmgen -reduce_tree [options] [selection]
|
|
|
|
Demo for recursive pmgen patterns. Map trees of AND/OR/XOR to $reduce_*.
|
|
|
|
|
|
test_pmgen -eqpmux [options] [selection]
|
|
|
|
Demo for recursive pmgen patterns. Optimize EQ/NE/PMUX circuits.
|
|
|
|
|
|
test_pmgen -generate [options] <pattern_name>
|
|
|
|
Create modules that match the specified pattern.
|
|
\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 [-L <libname>] {-sv|-vhdl|...} <hdl-file>
|
|
|
|
Look up external definitions in the specified library.
|
|
(-L may be used more than once)
|
|
|
|
|
|
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
|
|
|
|
-fullinit
|
|
Keep all register initializations, even those for non-FF registers.
|
|
|
|
-chparam name value
|
|
Elaborate the specified top modules (all modules when -all given) using
|
|
this parameter value. Modules on which this parameter does not exist will
|
|
cause Verific to produce a VERI-1928 or VHDL-1676 message. This option
|
|
can be specified multiple times to override multiple parameters.
|
|
String values must be passed in double quotes (").
|
|
|
|
-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.
|
|
|
|
|
|
Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.
|
|
https://www.yosyshq.com/\n");
|
|
|
|
Contact office@yosyshq.com for free evaluation
|
|
binaries of YosysHQ Tabby CAD Suite.
|
|
\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'
|
|
|
|
-reset
|
|
clear list of defined preprocessor symbols
|
|
|
|
-list
|
|
list currently defined preprocessor symbols
|
|
\end{lstlisting}
|
|
|
|
\section{wbflip -- flip the whitebox attribute}
|
|
\label{cmd:wbflip}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
wbflip [selection]
|
|
|
|
Flip the whitebox attribute on selected cells. I.e. if it's set, unset it, and
|
|
vice-versa. Blackbox cells are not effected by this command.
|
|
\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.
|
|
|
|
-keepdc
|
|
Do not optimize explicit don't-care values.
|
|
\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 AIGER 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
|
|
|
|
-I, -O, -B, -L
|
|
If the design contains no input/output/assert/flip-flop then create one
|
|
dummy input/output/bad_state-pin or latch to make the tools reading the
|
|
AIGER file happy.
|
|
\end{lstlisting}
|
|
|
|
\section{write\_blif -- write design to BLIF file}
|
|
\label{cmd:write_blif}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_blif [options] [filename]
|
|
|
|
Write the current design to an BLIF file.
|
|
|
|
-top top_module
|
|
set the specified module as design top module
|
|
|
|
-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>
|
|
-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.
|
|
|
|
-icells
|
|
do not translate Yosys's internal gates to generic BLIF logic
|
|
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, $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
|
|
|
|
-c
|
|
Output cover properties using 'bad' statements instead of asserts
|
|
|
|
-i <filename>
|
|
Create additional info file with auxiliary information
|
|
\end{lstlisting}
|
|
|
|
\section{write\_cxxrtl -- convert design to C++ RTL simulation}
|
|
\label{cmd:write_cxxrtl}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_cxxrtl [options] [filename]
|
|
|
|
Write C++ code for simulating the design. The generated code requires a driver;
|
|
the following simple driver is provided as an example:
|
|
|
|
#include "top.cc"
|
|
|
|
int main() {
|
|
cxxrtl_design::p_top top;
|
|
while (1) {
|
|
top.p_clk.next = value<1> {1u};
|
|
top.step();
|
|
top.p_clk.next = value<1> {0u};
|
|
top.step();
|
|
}
|
|
}
|
|
|
|
The following options are supported by this backend:
|
|
|
|
-O <level>
|
|
set the optimization level. the default is -O5. higher optimization
|
|
levels dramatically decrease compile and run time, and highest level
|
|
possible for a design should be used.
|
|
|
|
-O0
|
|
no optimization.
|
|
|
|
-O1
|
|
elide internal wires if possible.
|
|
|
|
-O2
|
|
like -O1, and localize internal wires if possible.
|
|
|
|
-O3
|
|
like -O2, and elide public wires not marked (*keep*) if possible.
|
|
|
|
-O4
|
|
like -O3, and localize public wires not marked (*keep*) if possible.
|
|
|
|
-O5
|
|
like -O4, and run `splitnets -driver; opt_clean -purge` first.
|
|
\end{lstlisting}
|
|
|
|
\section{write\_edif -- write design to EDIF netlist file}
|
|
\label{cmd:write_edif}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_edif [options] [filename]
|
|
|
|
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)
|
|
|
|
-gndvccy
|
|
create "GND" and "VCC" cells with "Y" outputs. (the default is "G"
|
|
for "GND" and "P" for "VCC".)
|
|
|
|
-attrprop
|
|
create EDIF properties for cell attributes
|
|
|
|
-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.
|
|
The following commands are executed by this command:
|
|
pmuxtree
|
|
\end{lstlisting}
|
|
|
|
\section{write\_ilang -- write design to ilang file}
|
|
\label{cmd:write_ilang}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_ilang [filename]
|
|
|
|
Write the current design to an 'ilang' file. (ilang is a text representation
|
|
of a design in yosys's internal format.)
|
|
|
|
-selected
|
|
only write selected parts of the design.
|
|
\end{lstlisting}
|
|
|
|
\section{write\_intersynth -- write design to InterSynth netlist file}
|
|
\label{cmd:write_intersynth}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_intersynth [options] [filename]
|
|
|
|
Write the current design to an 'intersynth' netlist file. InterSynth is
|
|
a tool for Coarse-Grain Example-Driven Interconnect Synthesis.
|
|
|
|
-notypes
|
|
do not generate celltypes and conntypes commands. i.e. just output
|
|
the netlists. this is used for postsilicon synthesis.
|
|
|
|
-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.
|
|
|
|
-selected
|
|
only write selected modules. modules must be selected entirely or
|
|
not at all.
|
|
|
|
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
|
|
|
|
-compat-int
|
|
emit 32-bit or smaller fully-defined parameter values directly
|
|
as JSON numbers (for compatibility with old parsers)
|
|
|
|
|
|
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", "1", "x", or
|
|
"z" instead of a number.
|
|
|
|
Bit vectors (including integers) are written as string holding the binaryrepresentation of the value. Strings are written as strings, with an appendedblank in cases of strings of the form /[01xz]* */.
|
|
|
|
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 written 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 proof
|
|
(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]
|
|
write_spice [options] [filename]
|
|
|
|
Write the current design to an SPICE netlist file.
|
|
|
|
-big_endian
|
|
generate multi-bit ports in MSB first order
|
|
(default is LSB first)
|
|
|
|
-neg net_name
|
|
set the net name for constant 0 (default: Vss)
|
|
|
|
-pos net_name
|
|
set the net name for constant 1 (default: Vdd)
|
|
|
|
-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\_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.
|
|
|
|
-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
|
|
|
|
-attr2comment
|
|
with this option attributes are included as comments in the output
|
|
|
|
-noexpr
|
|
without this option all internal cells are converted to Verilog
|
|
expressions.
|
|
|
|
-siminit
|
|
add initial statements with hierarchical refs to initialize FFs when
|
|
in -noexpr mode.
|
|
|
|
-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.
|
|
|
|
-extmem
|
|
instead of initializing memories using assignments to individual
|
|
elements, use the '$readmemh' function to read initialization data
|
|
from a file. This data is written to a file named by appending
|
|
a sequential index to the Verilog filename and replacing the extension
|
|
with '.mem', e.g. 'write_verilog -extmem foo.v' writes 'foo-1.mem',
|
|
'foo-2.mem' and so on.
|
|
|
|
-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
|
|
are written to the output 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{write\_xaiger -- write design to XAIGER file}
|
|
\label{cmd:write_xaiger}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
write_xaiger [options] [filename]
|
|
|
|
Write the top module (according to the (* top *) attribute or if only one module
|
|
is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, $_ABC9_FF_, ornon (* abc9_box_id *) cells will be converted into psuedo-inputs and
|
|
pseudo-outputs. Whitebox contents will be taken from the '<module-name>$holes'
|
|
module, if it exists.
|
|
|
|
-ascii
|
|
write ASCII version of AIGER format
|
|
|
|
-map <filename>
|
|
write an extra file with port and box symbols
|
|
\end{lstlisting}
|
|
|
|
\section{xilinx\_dffopt -- Xilinx: optimize FF control signal usage}
|
|
\label{cmd:xilinx_dffopt}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
xilinx_dffopt [options] [selection]
|
|
|
|
Converts hardware clock enable and set/reset signals on FFs to emulation
|
|
using LUTs, if doing so would improve area. Operates on post-techmap Xilinx
|
|
cells (LUT*, FD*).
|
|
|
|
-lut4
|
|
Assume a LUT4-based device (instead of a LUT6-based device).
|
|
\end{lstlisting}
|
|
|
|
\section{xilinx\_dsp -- Xilinx: pack resources into DSPs}
|
|
\label{cmd:xilinx_dsp}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
xilinx_dsp [options] [selection]
|
|
|
|
Pack input registers (A2, A1, B2, B1, C, D, AD; with optional enable/reset),
|
|
pipeline registers (M; with optional enable/reset), output registers (P; with
|
|
optional enable/reset), pre-adder and/or post-adder into Xilinx DSP resources.
|
|
|
|
Multiply-accumulate operations using the post-adder with feedback on the 'C'
|
|
input will be folded into the DSP. In this scenario only, the 'C' input can be
|
|
used to override the current accumulation result with a new value, which will
|
|
be added to the multiplier result to form the next accumulation result.
|
|
|
|
Use of the dedicated 'PCOUT' -> 'PCIN' cascade path is detected for 'P' -> 'C'
|
|
connections (optionally, where 'P' is right-shifted by 17-bits and used as an
|
|
input to the post-adder -- a pattern common for summing partial products to
|
|
implement wide multipliers). Limited support also exists for similar cascading
|
|
for A and B using '[AB]COUT' -> '[AB]CIN'. Currently, cascade chains are limited
|
|
to a maximum length of 20 cells, corresponding to the smallest Xilinx 7 Series
|
|
device.
|
|
|
|
This pass is a no-op if the scratchpad variable 'xilinx_dsp.multonly' is set
|
|
to 1.
|
|
|
|
|
|
Experimental feature: addition/subtractions less than 12 or 24 bits with the
|
|
'(* use_dsp="simd" *)' attribute attached to the output wire or attached to
|
|
the add/subtract operator will cause those operations to be implemented using
|
|
the 'SIMD' feature of DSPs.
|
|
|
|
Experimental feature: the presence of a `$ge' cell attached to the registered
|
|
P output implementing the operation "(P >= <power-of-2>)" will be transformed
|
|
into using the DSP48E1's pattern detector feature for overflow detection.
|
|
|
|
-family {xcup|xcu|xc7|xc6v|xc5v|xc4v|xc6s|xc3sda}
|
|
select the family to target
|
|
default: xc7
|
|
\end{lstlisting}
|
|
|
|
\section{xilinx\_srl -- Xilinx shift register extraction}
|
|
\label{cmd:xilinx_srl}
|
|
\begin{lstlisting}[numbers=left,frame=single]
|
|
xilinx_srl [options] [selection]
|
|
|
|
This pass converts chains of built-in flops (bit-level: $_DFF_[NP]_, $_DFFE_*
|
|
and word-level: $dff, $dffe) as well as Xilinx flops (FDRE, FDRE_1) into a
|
|
$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock polarity,
|
|
enable, and enable polarity (where relevant).
|
|
Flops with resets cannot be mapped to Xilinx devices and will not be inferred.
|
|
-minlen N
|
|
min length of shift register (default = 3)
|
|
|
|
-fixed
|
|
infer fixed-length shift registers.
|
|
|
|
-variable
|
|
infer variable-length shift registers (i.e. fixed-length shifts where
|
|
each element also fans-out to a $shiftx cell).
|
|
\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}
|
|
|