1 % Generated using the yosys 'help -write-tex-command-reference-manual' command.
3 \section{abc -- use ABC for technology mapping
}
5 \begin{lstlisting
}[numbers=left,frame=single
]
6 abc
[options
] [selection
]
8 This pass uses the ABC tool
[1] for technology mapping of yosys's internal gate
9 library to a target architecture.
12 use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC.
13 This can e.g. be used to call a specific version of ABC or a wrapper.
16 use the specified ABC script file instead of the default script.
18 if <file> starts with a plus sign (+), then the rest of the filename
19 string is interpreted as the command string to be passed to ABC. The
20 leading plus sign is removed and all commas (,) in the string are
21 replaced with blanks before the string is passed to ABC.
23 if no -script parameter is given, the following scripts are used:
25 for -liberty/-genlib without -constr:
26 strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
29 for -liberty/-genlib with -constr:
30 strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
31 &nf
{D
}; &put; buffer; upsize
{D
}; dnsize
{D
}; stime -p
33 for -lut/-luts (only one LUT size):
34 strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2;
37 for -lut/-luts (different LUT sizes):
38 strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2
41 strash; ifraig; scorr; dc2; dretime; strash; dch -f;
45 strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
49 use different default scripts that are slightly faster (at the cost
52 for -liberty/-genlib without -constr:
53 strash; dretime; map
{D
}
55 for -liberty/-genlib with -constr:
56 strash; dretime; map
{D
}; buffer; upsize
{D
}; dnsize
{D
};
63 strash; dretime; cover
{I
} {P
}
69 generate netlists for the specified cell library (using the liberty
73 generate netlists for the specified cell library (using the SIS Genlib
77 pass this file with timing constraints to ABC.
78 use with -liberty/-genlib.
80 a constr file contains two lines:
81 set_driving_cell <cell_name>
82 set_load <floating_point_number>
84 the set_driving_cell statement defines which cell type is assumed to
85 drive the primary inputs and the set_load statement sets the load in
86 femtofarads for each primary output.
89 set delay target. the string
{D
} in the default scripts above is
90 replaced by this option when used, and an empty string otherwise.
91 this also replaces 'dretime' with 'dretime; retime -o
{D
}' in the
92 default scripts above.
95 maximum number of SOP inputs.
96 (replaces
{I
} in the default scripts above)
99 maximum number of SOP products.
100 (replaces
{P
} in the default scripts above)
103 maximum number of LUT inputs shared.
104 (replaces
{S
} in the default scripts above, default: -S
1)
107 generate netlist using luts of (max) the specified width.
110 generate netlist using luts of (max) the specified width <w2>. All
111 luts with width <= <w1> have constant cost. for luts larger than <w1>
112 the area cost doubles with each additional input bit. the delay cost
113 is still constant for all lut widths.
115 -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,..
116 generate netlist using luts. Use the specified costs for luts with
1,
120 map to sum-of-product cells and inverters
123 Map to the specified list of gate types. Supported gates types are:
124 AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX,
125 NMUX, AOI3, OAI3, AOI4, OAI4.
126 (The NOT gate is always added to this list automatically.)
128 The following aliases can be used to reference common sets of gate types:
129 simple: AND OR XOR MUX
131 cmos3: NAND NOR AOI3 OAI3
132 cmos4: NAND NOR AOI3 OAI3 AOI4 OAI4
133 cmos: NAND NOR AOI3 OAI3 AOI4 OAI4 NMUX MUX XOR XNOR
134 gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT
135 aig: AND NAND OR NOR ANDNOT ORNOT
137 The alias 'all' represent the full set of all gate types.
139 Prefix a gate type with a '-' to remove it from the list. For example
140 the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent.
142 The default is 'all,-NMUX,-AOI3,-OAI3,-AOI4,-OAI4'.
145 also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many
146 clock domains are automatically partitioned in clock domains and each
147 domain is passed through ABC independently.
149 -clk
[!
]<clock-signal-name>
[,
[!
]<enable-signal-name>
]
150 use only the specified clock domain. this is like -dff, but only FF
151 cells that belong to the specified clock domain are used.
154 set the "keep" attribute on flip-flop output wires. (and thus preserve
155 them, for example for equivalence checking.)
158 when this option is used, the temporary files created by this pass
159 are not removed. this is useful for debugging.
162 print the temp dir name in log. usually this is suppressed so that the
163 command output is identical across runs.
166 set a 'abcgroup' attribute on all objects created by ABC. The value of
167 this attribute is a unique integer for each ABC process started. This
168 is useful for debugging the partitioning of clock domains.
171 run the 'dress' command after all other ABC commands. This aims to
172 preserve naming by an equivalence check between the original and post-ABC
173 netlists (experimental).
175 When no target cell library is specified the Yosys standard cell library is
176 loaded into ABC before the ABC script is executed.
178 Note that this is a logic optimization pass within Yosys that is calling ABC
179 internally. This is not going to "run ABC on your design". It will instead run
180 ABC on logic snippets extracted from your design. You will not get any useful
181 output when passing an ABC script that writes a file. Instead write your full
182 design as BLIF file with write_blif and then load that into ABC externally if
183 you want to use ABC to convert your design into another format.
185 [1] http://www.eecs.berkeley.edu/~alanmi/abc/
188 \section{abc9 -- use ABC9 for technology mapping
}
190 \begin{lstlisting
}[numbers=left,frame=single
]
191 abc9
[options
] [selection
]
193 This script pass performs a sequence of commands to facilitate the use of the ABC
194 tool
[1] for technology mapping of the current design to a target FPGA
195 architecture. Only fully-selected modules are supported.
197 -run <from_label>:<to_label>
198 only run the commands between the labels (see below). an empty
199 from label is synonymous to 'begin', and empty to label is
200 synonymous to the end of the command list.
203 use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC.
204 This can e.g. be used to call a specific version of ABC or a wrapper.
207 use the specified ABC script file instead of the default script.
209 if <file> starts with a plus sign (+), then the rest of the filename
210 string is interpreted as the command string to be passed to ABC. The
211 leading plus sign is removed and all commas (,) in the string are
212 replaced with blanks before the string is passed to ABC.
214 if no -script parameter is given, the following scripts are used:
215 &scorr; &sweep; &dc2; &dch -f; &ps; &if
{C
} {W
} {D
} {R
} -v; &mfs
218 use different default scripts that are slightly faster (at the cost
220 &if
{C
} {W
} {D
} {R
} -v
223 set delay target. the string
{D
} in the default scripts above is
224 replaced by this option when used, and an empty string otherwise
225 (indicating best possible delay).
228 generate netlist using luts of (max) the specified width.
231 generate netlist using luts of (max) the specified width <w2>. All
232 luts with width <= <w1> have constant cost. for luts larger than <w1>
233 the area cost doubles with each additional input bit. the delay cost
234 is still constant for all lut widths.
237 pass this file with lut library to ABC.
239 -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,..
240 generate netlist using luts. Use the specified costs for luts with
1,
244 when auto-generating the lut library, discard all luts equal to or
245 greater than this size (applicable when neither -lut nor -luts is
249 also pass $_DFF_
[NP
]_ cells through to ABC. modules with many clock
250 domains are supported and automatically partitioned by ABC.
253 when this option is used, the temporary files created by this pass
254 are not removed. this is useful for debugging.
257 print the temp dir name in log. usually this is suppressed so that the
258 command output is identical across runs.
261 pass this file with box library to ABC.
263 Note that this is a logic optimization pass within Yosys that is calling ABC
264 internally. This is not going to "run ABC on your design". It will instead run
265 ABC on logic snippets extracted from your design. You will not get any useful
266 output when passing an ABC script that writes a file. Instead write your full
267 design as an XAIGER file with `write_xaiger' and then load that into ABC
268 externally if you want to use ABC to convert your design into another format.
270 [1] http://www.eecs.berkeley.edu/~alanmi/abc/
274 abc9_ops -check
[-dff
] (option if -dff)
277 abc9_ops -prep_hier
[-dff
] (option if -dff)
278 scc -specify -set_attr abc9_scc_id
{}
279 abc9_ops -prep_bypass
[-prep_dff
] (option if -dff)
281 design -load $abc9_map
284 techmap -wb -map
%$abc9 -map +/techmap.v A:abc9_flop
286 abc9_ops -prep_dff_submod (only if -dff)
287 setattr -set submod "$abc9_flop" t:$_DFF_?_
%ci* %co* t:$_DFF_?_ %d (only if -dff)
288 submod (only if -dff)
289 setattr -mod -set whitebox
1 -set abc9_flop
1 -set abc9_box
1 *_$abc9_flop (only if -dff)
290 foreach module in design
291 rename <module-name>_$abc9_flop _TECHMAP_REPLACE_ (only if -dff)
292 abc9_ops -prep_dff_unmap (only if -dff)
293 design -copy-to $abc9 =*_$abc9_flop (only if -dff)
294 delete =*_$abc9_flop (only if -dff)
295 design -stash $abc9_map
298 techmap -wb -max_iter
1 -map
%$abc9_map -map +/abc9_map.v [-D DFF] (option if -dff)
299 design -delete $abc9_map
302 read_verilog -icells -lib -specify +/abc9_model.v
303 abc9_ops -break_scc -prep_delays -prep_xaiger
[-dff
] (option for -dff)
304 abc9_ops -prep_lut <maxlut> (skip if -lut or -luts)
305 abc9_ops -prep_box (skip if -box)
307 design -load $abc9_holes
308 techmap -wb -map
%$abc9 -map +/techmap.v
311 design -stash $abc9_holes
317 foreach module in selection
318 abc9_ops -write_lut <abc-temp-dir>/input.lut (skip if '-lut' or '-luts')
319 abc9_ops -write_box <abc-temp-dir>/input.box (skip if '-box')
320 write_xaiger -map <abc-temp-dir>/input.sym
[-dff
] <abc-temp-dir>/input.xaig
321 abc9_exe
[options
] -cwd <abc-temp-dir> -lut
[<abc-temp-dir>/input.lut
] -box
[<abc-temp-dir>/input.box
]
322 read_aiger -xaiger -wideports -module_name <module-name>$abc9 -map <abc-temp-dir>/input.sym <abc-temp-dir>/output.aig
323 abc9_ops -reintegrate
[-dff
]
326 techmap -wb -map
%$abc9_unmap -map +/abc9_unmap.v
327 design -delete $abc9_unmap
328 design -delete $abc9_holes
330 setattr -mod -unset abc9_box_id
333 \section{abc9
\_exe -- use ABC9 for technology mapping
}
335 \begin{lstlisting
}[numbers=left,frame=single
]
339 This pass uses the ABC tool
[1] for technology mapping of the top module
340 (according to the
(* top *) attribute or if only one module is currently selected)
341 to a target FPGA architecture.
344 use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC.
345 This can e.g. be used to call a specific version of ABC or a wrapper.
348 use the specified ABC script file instead of the default script.
350 if <file> starts with a plus sign (+), then the rest of the filename
351 string is interpreted as the command string to be passed to ABC. The
352 leading plus sign is removed and all commas (,) in the string are
353 replaced with blanks before the string is passed to ABC.
355 if no -script parameter is given, the following scripts are used:
356 &scorr; &sweep; &dc2; &dch -f; &ps; &if
{C
} {W
} {D
} {R
} -v; &mfs
359 use different default scripts that are slightly faster (at the cost
361 &if
{C
} {W
} {D
} {R
} -v
364 set delay target. the string
{D
} in the default scripts above is
365 replaced by this option when used, and an empty string otherwise
366 (indicating best possible delay).
369 generate netlist using luts of (max) the specified width.
372 generate netlist using luts of (max) the specified width <w2>. All
373 luts with width <= <w1> have constant cost. for luts larger than <w1>
374 the area cost doubles with each additional input bit. the delay cost
375 is still constant for all lut widths.
378 pass this file with lut library to ABC.
380 -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,..
381 generate netlist using luts. Use the specified costs for luts with
1,
385 print the temp dir name in log. usually this is suppressed so that the
386 command output is identical across runs.
389 pass this file with box library to ABC.
392 use this as the current working directory, inside which the 'input.xaig'
393 file is expected. temporary files will be created in this directory, and
394 the mapped result will be written to 'output.aig'.
396 Note that this is a logic optimization pass within Yosys that is calling ABC
397 internally. This is not going to "run ABC on your design". It will instead run
398 ABC on logic snippets extracted from your design. You will not get any useful
399 output when passing an ABC script that writes a file. Instead write your full
400 design as BLIF file with write_blif and then load that into ABC externally if
401 you want to use ABC to convert your design into another format.
403 [1] http://www.eecs.berkeley.edu/~alanmi/abc/
406 \section{abc9
\_ops -- helper functions for ABC9
}
408 \begin{lstlisting
}[numbers=left,frame=single
]
409 abc9_ops
[options
] [selection
]
411 This pass contains a set of supporting operations for use during ABC technology
412 mapping, and is expected to be called in conjunction with other operations from
413 the `abc9' script pass. Only fully-selected modules are supported.
416 check that the design is valid, e.g.
(* abc9_box_id *) values are unique,
417 (* abc9_carry *) is only given for one input/output port, etc.
420 derive all used
(* abc9_box *) or
(* abc9_flop *) (if -dff option)
421 whitebox modules. with
(* abc9_flop *) modules, only those containing
422 $dff/$_DFF_
[NP
]_ cells with zero initial state -- due to an ABC limitation
426 create techmap rules in the '$abc9_map' and '$abc9_unmap' designs for
427 bypassing sequential
(* abc9_box *) modules using a combinatorial box
428 (named *_$abc9_byp). bypassing is necessary if sequential elements (e.g.
429 $dff, $mem, etc.) are discovered inside so that any combinatorial paths
430 will be correctly captured. this bypass box will only contain ports that
431 are referenced by a simple path declaration ($specify2 cell) inside a
435 select all
(* abc9_flop *) modules instantiated in the design and store
436 in the named selection '$abc9_flops'.
439 within
(* abc9_flop *) modules, rewrite all edge-sensitive path
440 declarations and $setup() timing checks ($specify3 and $specrule cells)
441 that share a 'DST' port with the $_DFF_
[NP
]_.Q port from this 'Q' port to
442 the DFF's 'D' port. this is to prepare such specify cells to be moved
446 populate the '$abc9_unmap' design with techmap rules for mapping *_$abc9_flop
447 cells back into their derived cell types (where the rules created by
448 -prep_hier will then map back to the original cell with parameters).
451 insert `$__ABC9_DELAY' blackbox cells into the design to account for
452 certain required times.
455 for an arbitrarily chosen cell in each unique SCC of each selected module
456 (tagged with an
(* abc9_scc_id = <int> *) attribute) interrupt all wires
457 driven by this cell's outputs with a temporary $__ABC9_SCC_BREAKER cell
461 prepare the design for XAIGER output. this includes computing the
462 topological ordering of ABC9 boxes, as well as preparing the '$abc9_holes'
463 design that contains the logic behaviour of ABC9 whiteboxes.
466 consider flop cells (those instantiating modules marked with
(* abc9_flop *))
467 during -prep_
{delays,xaiger,box
}.
470 pre-compute the lut library by analysing all modules marked with
471 (* abc9_lut=<area> *).
474 write the pre-computed lut library to <dst>.
477 pre-compute the box library by analysing all modules marked with
481 write the pre-computed box library to <dst>.
484 for each selected module, re-intergrate the module '<module-name>$abc9'
485 by first recovering ABC9 boxes, and then stitching in the remaining primary
489 \section{add -- add objects to the design
}
491 \begin{lstlisting
}[numbers=left,frame=single
]
492 add <command>
[selection
]
494 This command adds objects to the design. It operates on all fully selected
495 modules. So e.g. 'add -wire foo' will add a wire foo to all selected modules.
498 add
{-wire|-input|-inout|-output
} <name> <width>
[selection
]
500 Add a wire (input, inout, output port) with the given name and width. The
501 command will fail if the object exists already and has different properties
502 than the object to be created.
505 add -global_input <name> <width>
[selection
]
507 Like 'add -input', but also connect the signal between instances of the
511 add
{-assert|-assume|-live|-fair|-cover
} <name1>
[-if <name2>
]
513 Add an $assert, $assume, etc. cell connected to a wire named name1, with its
514 enable signal optionally connected to a wire named name2 (default:
1'b1).
519 Add module
[s
] with the specified name
[s
].
522 \section{aigmap -- map logic to and-inverter-graph circuit
}
524 \begin{lstlisting
}[numbers=left,frame=single
]
525 aigmap
[options
] [selection
]
527 Replace all logic cells with circuits made of only $_AND_ and
531 Enable creation of $_NAND_ cells
534 Overwrite replaced cells in the current selection with new $_AND_,
535 $_NOT_, and $_NAND_, cells
538 \section{alumacc -- extract ALU and MACC cells
}
540 \begin{lstlisting
}[numbers=left,frame=single
]
543 This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu
547 \section{anlogic
\_eqn -- Anlogic: Calculate equations for luts
}
548 \label{cmd:anlogic_eqn
}
549 \begin{lstlisting
}[numbers=left,frame=single
]
550 anlogic_eqn
[selection
]
552 Calculate equations for luts since bitstream generator depends on it.
555 \section{anlogic
\_fixcarry -- Anlogic: fix carry chain
}
556 \label{cmd:anlogic_fixcarry
}
557 \begin{lstlisting
}[numbers=left,frame=single
]
558 anlogic_fixcarry
[options
] [selection
]
560 Add Anlogic adders to fix carry chain if needed.
563 \section{assertpmux -- adds asserts for parallel muxes
}
564 \label{cmd:assertpmux
}
565 \begin{lstlisting
}[numbers=left,frame=single
]
566 assertpmux
[options
] [selection
]
568 This command adds asserts to the design that assert that all parallel muxes
569 ($pmux cells) have a maximum of one of their inputs enable at any time.
572 do not enforce the pmux condition during the init state
575 usually the $pmux condition is only checked when the $pmux output
576 is used by the mux tree it drives. this option will deactivate this
577 additional constraint and check the $pmux condition always.
580 \section{async2sync -- convert async FF inputs to sync circuits
}
581 \label{cmd:async2sync
}
582 \begin{lstlisting
}[numbers=left,frame=single
]
583 async2sync
[options
] [selection
]
585 This command replaces async FF inputs with sync circuits emulating the same
586 behavior for when the async signals are actually synchronized to the clock.
588 This pass assumes negative hold time for the async FF inputs. For example when
589 a reset deasserts with the clock edge, then the FF output will still drive the
590 reset value in the next cycle regardless of the data-in value at the time of
594 \section{attrmap -- renaming attributes
}
596 \begin{lstlisting
}[numbers=left,frame=single
]
597 attrmap
[options
] [selection
]
599 This command renames attributes and/or maps key/value pairs to
600 other key/value pairs.
603 Match attribute names case-insensitively and set it to the specified
606 -rename <old_name> <new_name>
607 Rename attributes as specified
609 -map <old_name>=<old_value> <new_name>=<new_value>
610 Map key/value pairs as indicated.
612 -imap <old_name>=<old_value> <new_name>=<new_value>
613 Like -map, but use case-insensitive match for <old_value> when
614 it is a string value.
616 -remove <name>=<value>
617 Remove attributes matching this pattern.
620 Operate on module attributes instead of attributes on wires and cells.
622 For example, mapping Xilinx-style "keep" attributes to Yosys-style:
624 attrmap -tocase keep -imap keep="true" keep=
1 \
625 -imap keep="false" keep=
0 -remove keep=
0
628 \section{attrmvcp -- move or copy attributes from wires to driving cells
}
630 \begin{lstlisting
}[numbers=left,frame=single
]
631 attrmvcp
[options
] [selection
]
633 Move or copy attributes on wires to the cells driving them.
636 By default, attributes are moved. This will only add
637 the attribute to the cell, without removing it from
641 If no selected cell consumes the attribute, then it is
642 left on the wire by default. This option will cause the
643 attribute to be removed from the wire, even if no selected
647 By default, attriburtes are moved to the cell driving the
648 wire. With this option set it will be moved to the cell
649 driven by the wire instead.
652 Move or copy this attribute. This option can be used
656 \section{autoname -- automatically assign names to objects
}
658 \begin{lstlisting
}[numbers=left,frame=single
]
661 Assign auto-generated public names to objects with private names (the ones
665 \section{blackbox -- convert modules into blackbox modules
}
667 \begin{lstlisting
}[numbers=left,frame=single
]
668 blackbox
[options
] [selection
]
670 Convert modules into blackbox modules (remove contents and set the blackbox
674 \section{bmuxmap -- transform \$bmux cells to trees of \$mux cells
}
676 \begin{lstlisting
}[numbers=left,frame=single
]
679 This pass transforms $bmux cells to trees of $mux cells.
682 \section{bugpoint -- minimize testcases
}
684 \begin{lstlisting
}[numbers=left,frame=single
]
685 bugpoint
[options
] [-script <filename> | -command "<command>"
]
687 This command minimizes the current design that is known to crash Yosys with the
688 given script into a smaller testcase. It does this by removing an arbitrary part
689 of the design and recursively invokes a new Yosys process with this modified design
690 and the same script, repeating these steps while it can find a smaller design that
691 still causes a crash. Once this command finishes, it replaces the current design
692 with the smallest testcase it was able to produce.
693 In order to save the reduced testcase you must write this out to a file with
694 another command after `bugpoint` like `write_rtlil` or `write_verilog`.
696 -script <filename> | -command "<command>"
697 use this script file or command to crash Yosys. required.
700 use this Yosys binary. if not specified, `yosys` is used.
703 only consider crashes that place this string in the log file.
706 run `proc_clean; clean -purge` after each minimization step. converges
707 faster, but produces larger testcases, and may fail to produce any
708 testcase at all if the crash is related to dangling wires.
711 run `proc_clean; clean -purge` before checking testcase and after
712 finishing. produces smaller and more useful testcases, but may fail to
713 produce any testcase at all if the crash is related to dangling wires.
715 It is possible to constrain which parts of the design will be considered for
716 removal. Unless one or more of the following options are specified, all parts
720 try to remove modules. modules with a
(* bugpoint_keep *) attribute
724 try to remove module ports. ports with a
(* bugpoint_keep *) attribute
725 will be skipped (useful for clocks, resets, etc.)
728 try to remove cells. cells with a
(* bugpoint_keep *) attribute will
732 try to reconnect ports to 'x.
735 try to remove processes. processes with a
(* bugpoint_keep *) attribute
739 try to remove process assigns from cases.
742 try to remove process updates from syncs.
745 child process wrapping command, e.g., "timeout
30", or valgrind.
748 \section{cd -- a shortcut for 'select -module <name>'
}
750 \begin{lstlisting
}[numbers=left,frame=single
]
753 This is just a shortcut for 'select -module <modname>'.
758 When no module with the specified name is found, but there is a cell
759 with the specified name in the current module, then this is equivalent
764 Remove trailing substrings that start with '.' in current module name until
765 the name of a module in the current design is generated, then switch to that
766 module. Otherwise clear the current selection.
770 This is just a shortcut for 'select -clear'.
773 \section{check -- check for obvious problems in the design
}
775 \begin{lstlisting
}[numbers=left,frame=single
]
776 check
[options
] [selection
]
778 This pass identifies the following problems in the current design:
780 - combinatorial loops
781 - two or more conflicting drivers for one wire
782 - used wires that do not have a driver
787 also check for wires which have the 'init' attribute set
790 also check for wires that have the 'init' attribute set and are not
791 driven by an FF cell type
794 also check for internal cells that have not been mapped to cells of the
798 modify the -mapped behavior to still allow $_TBUF_ cells
801 produce a runtime error if any problems are found in the current design
804 \section{chformal -- change formal constraints of the design
}
806 \begin{lstlisting
}[numbers=left,frame=single
]
807 chformal
[types
] [mode
] [options
] [selection
]
809 Make changes to the formal constraints of the design. The
[types
] options
810 the type of constraint to operate on. If none of the following options are given,
811 the command will operate on all constraint types:
813 -assert $assert cells, representing assert(...) constraints
814 -assume $assume cells, representing assume(...) constraints
815 -live $live cells, representing assert(s_eventually ...)
816 -fair $fair cells, representing assume(s_eventually ...)
817 -cover $cover cells, representing cover() statements
819 Exactly one of the following modes must be specified:
822 remove the cells and thus constraints from the design
825 bypass FFs that only delay the activation of a constraint
828 delay activation of the constraint by <N> clock cycles
831 ignore activation of the constraint in the first <N> clock cycles
837 change the roles of cells as indicated. these options can be combined
840 \section{chparam -- re-evaluate modules with new parameters
}
842 \begin{lstlisting
}[numbers=left,frame=single
]
843 chparam
[ -set name value
]...
[selection
]
845 Re-evaluate the selected modules with new parameters. String values must be
846 passed in double quotes (").
849 chparam -list
[selection
]
851 List the available parameters of the selected modules.
854 \section{chtype -- change type of cells in the design
}
856 \begin{lstlisting
}[numbers=left,frame=single
]
857 chtype
[options
] [selection
]
859 Change the types of cells in the design.
862 set the cell type to the given type
864 -map <old_type> <new_type>
865 change cells types that match <old_type> to <new_type>
868 \section{clean -- remove unused cells and wires
}
870 \begin{lstlisting
}[numbers=left,frame=single
]
871 clean
[options
] [selection
]
873 This is identical to 'opt_clean', but less verbose.
875 When commands are separated using the ';;' token, this command will be executed
876 between the commands.
878 When commands are separated using the ';;;' token, this command will be executed
879 in -purge mode between the commands.
882 \section{clean
\_zerowidth -- clean zero-width connections from the design
}
883 \label{cmd:clean_zerowidth
}
884 \begin{lstlisting
}[numbers=left,frame=single
]
885 clean_zerowidth
[selection
]
887 Fixes the selected cells and processes to contain no zero-width connections.
888 Depending on the cell type, this may be implemented by removing the connection,
889 widening it to
1-bit, or removing the cell altogether.
892 \section{clk2fflogic -- convert clocked FFs to generic \$ff cells
}
893 \label{cmd:clk2fflogic
}
894 \begin{lstlisting
}[numbers=left,frame=single
]
895 clk2fflogic
[options
] [selection
]
897 This command replaces clocked flip-flops with generic $ff cells that use the
898 implicit global clock. This is useful for formal verification of designs with
902 \section{clkbufmap -- insert clock buffers on clock networks
}
903 \label{cmd:clkbufmap
}
904 \begin{lstlisting
}[numbers=left,frame=single
]
905 clkbufmap
[options
] [selection
]
907 Inserts clock buffers between nets connected to clock inputs and their drivers.
909 In the absence of any selection, all wires without the 'clkbuf_inhibit'
910 attribute will be considered for clock buffer insertion.
911 Alternatively, to consider all wires without the 'buffer_type' attribute set to
912 'none' or 'bufr' one would specify:
913 'w:* a:buffer_type=none a:buffer_type=bufr
%u %d'
916 -buf <celltype> <portname_out>:<portname_in>
917 Specifies the cell type to use for the clock buffers
918 and its port names. The first port will be connected to
919 the clock network sinks, and the second will be connected
920 to the actual clock source.
922 -inpad <celltype> <portname_out>:<portname_in>
923 If specified, a PAD cell of the given type is inserted on
924 clock nets that are also top module's inputs (in addition
925 to the clock buffer, if any).
927 At least one of -buf or -inpad should be specified.
930 \section{connect -- create or remove connections
}
932 \begin{lstlisting
}[numbers=left,frame=single
]
933 connect
[-nomap
] [-nounset
] -set <lhs-expr> <rhs-expr>
935 Create a connection. This is equivalent to adding the statement 'assign
936 <lhs-expr> = <rhs-expr>;' to the Verilog input. Per default, all existing
937 drivers for <lhs-expr> are unconnected. This can be overwritten by using
941 connect
[-nomap
] -unset <expr>
943 Unconnect all existing drivers for the specified expression.
946 connect
[-nomap
] [-assert
] -port <cell> <port> <expr>
948 Connect the specified cell port to the specified cell port.
951 Per default signal alias names are resolved and all signal names are mapped
952 the the signal name of the primary driver. Using the -nomap option deactivates
955 The connect command operates in one module only. Either only one module must
956 be selected or an active module must be set using the 'cd' command.
958 The -assert option verifies that the connection already exists, instead of
961 This command does not operate on module with processes.
964 \section{connect
\_rpc -- connect to RPC frontend
}
965 \label{cmd:connect_rpc
}
966 \begin{lstlisting
}[numbers=left,frame=single
]
967 connect_rpc -exec <command>
[args...
]
968 connect_rpc -path <path>
970 Load modules using an out-of-process frontend.
972 -exec <command>
[args...
]
973 run <command> with arguments
[args...
]. send requests on stdin, read
974 responses from stdout.
977 connect to Unix domain socket at <path>. (Unix)
978 connect to bidirectional byte-type named pipe at <path>. (Windows)
980 A simple JSON-based, newline-delimited protocol is used for communicating with
981 the frontend. Yosys requests data from the frontend by sending exactly
1 line
982 of JSON. Frontend responds with data or error message by replying with exactly
983 1 line of JSON as well.
985 ->
{"method": "modules"
}
986 <-
{"modules":
["<module-name>", ...
]}
987 <-
{"error": "<error-message>"
}
988 request for the list of modules that can be derived by this frontend.
989 the 'hierarchy' command will call back into this frontend if a cell
990 with type <module-name> is instantiated in the design.
992 ->
{"method": "derive", "module": "<module-name">, "parameters":
{
993 "<param-name>":
{"type": "
[unsigned|signed|string|real
]",
994 "value": "<param-value>"
}, ...
}}
995 <-
{"frontend": "
[rtlil|verilog|...
]","source": "<source>"
}}
996 <-
{"error": "<error-message>"
}
997 request for the module <module-name> to be derived for a specific set of
998 parameters. <param-name> starts with \ for named parameters, and with $
999 for unnamed parameters, which are numbered starting at
1.<param-value>
1000 for integer parameters is always specified as a binary string of unlimited
1001 precision. the <source> returned by the frontend is hygienically parsed
1002 by a built-in Yosys <frontend>, allowing the RPC frontend to return any
1003 convenient representation of the module. the derived module is cached,
1004 so the response should be the same whenever the same set of parameters
1008 \section{connwrappers -- match width of input-output port pairs
}
1009 \label{cmd:connwrappers
}
1010 \begin{lstlisting
}[numbers=left,frame=single
]
1011 connwrappers
[options
] [selection
]
1013 Wrappers are used in coarse-grain synthesis to wrap cells with smaller ports
1014 in wrapper cells with a (larger) constant port size. I.e. the upper bits
1015 of the wrapper output are signed/unsigned bit extended. This command uses this
1016 knowledge to rewire the inputs of the driven cells to match the output of
1019 -signed <cell_type> <port_name> <width_param>
1020 -unsigned <cell_type> <port_name> <width_param>
1021 consider the specified signed/unsigned wrapper output
1023 -port <cell_type> <port_name> <width_param> <sign_param>
1024 use the specified parameter to decide if signed or unsigned
1026 The options -signed, -unsigned, and -port can be specified multiple times.
1029 \section{coolrunner2
\_fixup -- insert necessary buffer cells for CoolRunner-II architecture
}
1030 \label{cmd:coolrunner2_fixup
}
1031 \begin{lstlisting
}[numbers=left,frame=single
]
1032 coolrunner2_fixup
[options
] [selection
]
1034 Insert necessary buffer cells for CoolRunner-II architecture.
1037 \section{coolrunner2
\_sop -- break \$sop cells into ANDTERM/ORTERM cells
}
1038 \label{cmd:coolrunner2_sop
}
1039 \begin{lstlisting
}[numbers=left,frame=single
]
1040 coolrunner2_sop
[options
] [selection
]
1042 Break $sop cells into ANDTERM/ORTERM cells.
1045 \section{copy -- copy modules in the design
}
1047 \begin{lstlisting
}[numbers=left,frame=single
]
1048 copy old_name new_name
1050 Copy the specified module. Note that selection patterns are not supported
1054 \section{cover -- print code coverage counters
}
1056 \begin{lstlisting
}[numbers=left,frame=single
]
1057 cover
[options
] [pattern
]
1059 Print the code coverage counters collected using the cover() macro in the Yosys
1060 C++ code. This is useful to figure out what parts of Yosys are utilized by a
1064 Do not print output to the normal destination (console and/or log file)
1067 Write output to this file, truncate if exists.
1070 Write output to this file, append if exists.
1073 Write output to a newly created file in the specified directory.
1075 When one or more pattern (shell wildcards) are specified, then only counters
1076 matching at least one pattern are printed.
1079 It is also possible to instruct Yosys to print the coverage counters on program
1080 exit to a file using environment variables:
1082 YOSYS_COVER_DIR="
{dir-name
}" yosys
{args
}
1084 This will create a file (with an auto-generated name) in this
1085 directory and write the coverage counters to it.
1087 YOSYS_COVER_FILE="
{file-name
}" yosys
{args
}
1089 This will append the coverage counters to the specified file.
1092 Hint: Use the following AWK command to consolidate Yosys coverage files:
1094 gawk '
{ p
[$
3] = $
1; c
[$
3] += $
2;
} END
{ for (i in p)
1095 printf "
%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3
1098 Coverage counters are only available in Yosys for Linux.
1101 \section{cutpoint -- adds formal cut points to the design
}
1102 \label{cmd:cutpoint
}
1103 \begin{lstlisting
}[numbers=left,frame=single
]
1104 cutpoint
[options
] [selection
]
1106 This command adds formal cut points to the design.
1109 set cupoint nets to undef (x). the default behavior is to create a
1110 $anyseq cell and drive the cutpoint net from that
1113 \section{debug -- run command with debug log messages enabled
}
1115 \begin{lstlisting
}[numbers=left,frame=single
]
1118 Execute the specified command with debug log messages enabled
1121 \section{delete -- delete objects in the design
}
1123 \begin{lstlisting
}[numbers=left,frame=single
]
1126 Deletes the selected objects. This will also remove entire modules, if the
1127 whole module is selected.
1130 delete
{-input|-output|-port
} [selection
]
1132 Does not delete any object but removes the input and/or output flag on the
1133 selected wires, thus 'deleting' module ports.
1136 \section{deminout -- demote inout ports to input or output
}
1137 \label{cmd:deminout
}
1138 \begin{lstlisting
}[numbers=left,frame=single
]
1139 deminout
[options
] [selection
]
1141 "Demote" inout ports to input or output ports, if possible.
1144 \section{demuxmap -- transform \$demux cells to \$eq + \$mux cells
}
1145 \label{cmd:demuxmap
}
1146 \begin{lstlisting
}[numbers=left,frame=single
]
1147 demuxmap
[selection
]
1149 This pass transforms $demux cells to a bunch of equality comparisons.
1152 \section{design -- save, restore and reset current design
}
1154 \begin{lstlisting
}[numbers=left,frame=single
]
1157 Clear the current design.
1162 Save the current design under the given name.
1165 design -stash <name>
1167 Save the current design under the given name and then clear the current design.
1172 Push the current design to the stack and then clear the current design.
1177 Push the current design to the stack without clearing the current design.
1182 Reset the current design and pop the last design from the stack.
1187 Reset the current design and load the design previously saved under the given
1191 design -copy-from <name>
[-as <new_mod_name>
] <selection>
1193 Copy modules from the specified design into the current one. The selection is
1194 evaluated in the other design.
1197 design -copy-to <name>
[-as <new_mod_name>
] [selection
]
1199 Copy modules from the current design into the specified one.
1202 design -import <name>
[-as <new_top_name>
] [selection
]
1204 Import the specified design into the current design. The source design must
1205 either have a selected top module or the selection must contain exactly one
1206 module that is then used as top module for this command.
1211 The Verilog front-end remembers defined macros and top-level declarations
1212 between calls to 'read_verilog'. This command resets this memory.
1214 design -delete <name>
1216 Delete the design previously saved under the given name.
1219 \section{dffinit -- set INIT param on FF cells
}
1221 \begin{lstlisting
}[numbers=left,frame=single
]
1222 dffinit
[options
] [selection
]
1224 This pass sets an FF cell parameter to the the initial value of the net it
1225 drives. (This is primarily used in FPGA flows.)
1227 -ff <cell_name> <output_port> <init_param>
1228 operate on the specified cell type. this option can be used
1232 use the string values "high" and "low" to represent a single-bit
1233 initial value of
1 or
0. (multi-bit values are not supported in this
1236 -strinit <string for high> <string for low>
1237 use string values in the command line to represent a single-bit
1238 initial value of
1 or
0. (multi-bit values are not supported in this
1242 fail if the FF cell has already a defined initial value set in other
1243 passes and the initial value of the net it drives is not equal to
1244 the already defined initial value.
1247 \section{dfflegalize -- convert FFs to types supported by the target
}
1248 \label{cmd:dfflegalize
}
1249 \begin{lstlisting
}[numbers=left,frame=single
]
1250 dfflegalize
[options
] [selection
]
1252 Converts FFs to types supported by the target.
1254 -cell <cell_type_pattern> <init_values>
1255 specifies a supported group of FF cells. <cell_type_pattern>
1256 is a yosys internal fine cell name, where ? characters can be
1257 as a wildcard matching any character. <init_values> specifies
1258 which initialization values these FF cells can support, and can
1261 - x (no init value supported)
1264 - r (init value has to match reset value, only for some FF types)
1265 -
01 (both
0 and
1 supported).
1268 specifies a minimum number of FFs that should be using any given
1269 clock enable signal. If a clock enable signal doesn't meet this
1270 threshold, it is unmapped into soft logic.
1273 specifies a minimum number of FFs that should be using any given
1274 sync set/reset signal. If a sync set/reset signal doesn't meet this
1275 threshold, it is unmapped into soft logic.
1277 The following cells are supported by this pass (ie. will be ingested,
1278 and can be specified as allowed targets):
1282 - $_DFF_
[NP
][NP
][01]_
1283 - $_DFFE_
[NP
][NP
][01][NP
]_
1285 - $_ALDFFE_
[NP
][NP
][NP
]_
1286 - $_DFFSR_
[NP
][NP
][NP
]_
1287 - $_DFFSRE_
[NP
][NP
][NP
][NP
]_
1288 - $_SDFF_
[NP
][NP
][01]_
1289 - $_SDFFE_
[NP
][NP
][01][NP
]_
1290 - $_SDFFCE_
[NP
][NP
][01][NP
]_
1293 - $_DLATCH_
[NP
][NP
][01]_
1294 - $_DLATCHSR_
[NP
][NP
][NP
]_
1296 The following transformations are performed by this pass:
1297 - upconversion from a less capable cell to a more capable cell, if the less capable cell is not supported (eg. dff -> dffe, or adff -> dffsr)
1298 - unmapping FFs with clock enable (due to unsupported cell type or -mince)
1299 - unmapping FFs with sync reset (due to unsupported cell type or -minsrst)
1300 - adding inverters on the control pins (due to unsupported polarity)
1301 - adding inverters on the D and Q pins and inverting the init/reset values
1302 (due to unsupported init or reset value)
1303 - converting sr into adlatch (by tying D to
1 and using E as set input)
1304 - emulating unsupported dffsr cell by adff + adff + sr + mux
1305 - emulating unsupported dlatchsr cell by adlatch + adlatch + sr + mux
1306 - emulating adff when the (reset, init) value combination is unsupported by
1307 dff + adff + dlatch + mux
1308 - emulating adlatch when the (reset, init) value combination is unsupported by
1309 - dlatch + adlatch + dlatch + mux
1310 If the pass is unable to realize a given cell type (eg. adff when only plain dffis available), an error is raised.
1313 \section{dfflibmap -- technology mapping of flip-flops
}
1314 \label{cmd:dfflibmap
}
1315 \begin{lstlisting
}[numbers=left,frame=single
]
1316 dfflibmap
[-prepare
] [-map-only
] [-info
] -liberty <file>
[selection
]
1318 Map internal flip-flop cells to the flip-flop cells in the technology
1319 library specified in the given liberty file.
1321 This pass may add inverters as needed. Therefore it is recommended to
1322 first run this pass and then map the logic paths to the target technology.
1324 When called with -prepare, this command will convert the internal FF cells
1325 to the internal cell types that best match the cells found in the given
1326 liberty file, but won't actually map them to the target cells.
1328 When called with -map-only, this command will only map internal cell
1329 types that are already of exactly the right type to match the target
1330 cells, leaving remaining internal cells untouched.
1332 When called with -info, this command will only print the target cell
1333 list, along with their associated internal cell types, and the argumentsthat would be passed to the dfflegalize pass. The design will not be
1337 \section{dffunmap -- unmap clock enable and synchronous reset from FFs
}
1338 \label{cmd:dffunmap
}
1339 \begin{lstlisting
}[numbers=left,frame=single
]
1340 dffunmap
[options
] [selection
]
1342 This pass transforms FF types with clock enable and/or synchronous reset into
1343 their base type (with neither clock enable nor sync reset) by emulating the clock
1344 enable and synchronous reset with multiplexers on the cell input.
1347 unmap only clock enables, leave synchronous resets alone.
1350 unmap only synchronous resets, leave clock enables alone.
1353 \section{dump -- print parts of the design in RTLIL format
}
1355 \begin{lstlisting
}[numbers=left,frame=single
]
1356 dump
[options
] [selection
]
1358 Write the selected parts of the design to the console or specified file in
1362 also dump the module headers, even if only parts of a single
1366 only dump the module headers if the entire module is selected
1369 write to the specified file.
1372 like -outfile but append instead of overwrite
1375 \section{echo -- turning echoing back of commands on and off
}
1377 \begin{lstlisting
}[numbers=left,frame=single
]
1380 Print all commands to log before executing them.
1385 Do not print all commands to log before executing them. (default)
1388 \section{ecp5
\_gsr -- ECP5: handle GSR
}
1389 \label{cmd:ecp5_gsr
}
1390 \begin{lstlisting
}[numbers=left,frame=single
]
1391 ecp5_gsr
[options
] [selection
]
1393 Trim active low async resets connected to GSR and resolve GSR parameter,
1394 if a GSR or SGSR primitive is used in the design.
1396 If any cell has the GSR parameter set to "AUTO", this will be resolved
1397 to "ENABLED" if a GSR primitive is present and the
(* nogsr *) attribute
1398 is not set, otherwise it will be resolved to "DISABLED".
1401 \section{edgetypes -- list all types of edges in selection
}
1402 \label{cmd:edgetypes
}
1403 \begin{lstlisting
}[numbers=left,frame=single
]
1404 edgetypes
[options
] [selection
]
1406 This command lists all unique types of 'edges' found in the selection. An 'edge'
1407 is a
4-tuple of source and sink cell type and port name.
1410 \section{efinix
\_fixcarry -- Efinix: fix carry chain
}
1411 \label{cmd:efinix_fixcarry
}
1412 \begin{lstlisting
}[numbers=left,frame=single
]
1413 efinix_fixcarry
[options
] [selection
]
1415 Add Efinix adders to fix carry chain if needed.
1418 \section{equiv
\_add -- add a \$equiv cell
}
1419 \label{cmd:equiv_add
}
1420 \begin{lstlisting
}[numbers=left,frame=single
]
1421 equiv_add
[-try
] gold_sig gate_sig
1423 This command adds an $equiv cell for the specified signals.
1426 equiv_add
[-try
] -cell gold_cell gate_cell
1428 This command adds $equiv cells for the ports of the specified cells.
1431 \section{equiv
\_induct -- proving \$equiv cells using temporal induction
}
1432 \label{cmd:equiv_induct
}
1433 \begin{lstlisting
}[numbers=left,frame=single
]
1434 equiv_induct
[options
] [selection
]
1436 Uses a version of temporal induction to prove $equiv cells.
1438 Only selected $equiv cells are proven and only selected cells are used to
1442 enable modelling of undef states
1445 the max. number of time steps to be considered (default =
4)
1447 This command is very effective in proving complex sequential circuits, when
1448 the internal state of the circuit quickly propagates to $equiv cells.
1450 However, this command uses a weak definition of 'equivalence': This command
1451 proves that the two circuits will not diverge after they produce equal
1452 outputs (observable points via $equiv) for at least <N> cycles (the <N>
1453 specified via -seq).
1455 Combined with simulation this is very powerful because simulation can give
1456 you confidence that the circuits start out synced for at least <N> cycles
1460 \section{equiv
\_make -- prepare a circuit for equivalence checking
}
1461 \label{cmd:equiv_make
}
1462 \begin{lstlisting
}[numbers=left,frame=single
]
1463 equiv_make
[options
] gold_module gate_module equiv_module
1465 This creates a module annotated with $equiv cells from two presumably
1466 equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'
1467 to work with the created equivalent checking module.
1470 Also match cells and wires with $... names.
1473 Do not match cells or signals that match the names in the file.
1476 Match FSM encodings using the description from the file.
1477 See 'help fsm_recode' for details.
1479 Note: The circuit created by this command is not a miter (with something like
1480 a trigger output), but instead uses $equiv cells to encode the equivalence
1481 checking problem. Use 'miter -equiv' if you want to create a miter circuit.
1484 \section{equiv
\_mark -- mark equivalence checking regions
}
1485 \label{cmd:equiv_mark
}
1486 \begin{lstlisting
}[numbers=left,frame=single
]
1487 equiv_mark
[options
] [selection
]
1489 This command marks the regions in an equivalence checking module. Region
0 is
1490 the proven part of the circuit. Regions with higher numbers are connected
1491 unproven subcricuits. The integer attribute 'equiv_region' is set on all
1495 \section{equiv
\_miter -- extract miter from equiv circuit
}
1496 \label{cmd:equiv_miter
}
1497 \begin{lstlisting
}[numbers=left,frame=single
]
1498 equiv_miter
[options
] miter_module
[selection
]
1500 This creates a miter module for further analysis of the selected $equiv cells.
1503 Create a trigger output
1506 Create cmp_* outputs for individual unproven $equiv cells
1509 Create a $assert cell for each unproven $equiv cell
1512 Create compare logic that handles undefs correctly
1515 \section{equiv
\_opt -- prove equivalence for optimized circuit
}
1516 \label{cmd:equiv_opt
}
1517 \begin{lstlisting
}[numbers=left,frame=single
]
1518 equiv_opt
[options
] [command
]
1520 This command uses temporal induction to check circuit equivalence before and
1521 after an optimization pass.
1523 -run <from_label>:<to_label>
1524 only run the commands between the labels (see below). an empty
1525 from label is synonymous to the start of the command list, and empty to
1526 label is synonymous to the end of the command list.
1529 expand the modules in this file before proving equivalence. this is
1530 useful for handling architecture-specific primitives.
1533 Do not match cells or signals that match the names in the file
1534 (passed to equiv_make).
1537 produce an error if the circuits are not equivalent.
1540 run clk2fflogic before equivalence checking.
1543 run async2sync before equivalence checking.
1546 enable modelling of undef states during equiv_induct.
1548 The following commands are executed by this verification command:
1554 design -stash postopt
1557 design -copy-from preopt -as gold A:top
1558 design -copy-from postopt -as gate A:top
1560 techmap: (only with -map)
1561 techmap -wb -D EQUIV -autoproc -map <filename> ...
1564 clk2fflogic (only with -multiclock)
1565 async2sync (only with -async2sync)
1566 equiv_make -blacklist <filename> ... gold gate equiv
1567 equiv_induct
[-undef
] equiv
1568 equiv_status
[-assert
] equiv
1574 \section{equiv
\_purge -- purge equivalence checking module
}
1575 \label{cmd:equiv_purge
}
1576 \begin{lstlisting
}[numbers=left,frame=single
]
1577 equiv_purge
[options
] [selection
]
1579 This command removes the proven part of an equivalence checking module, leaving
1580 only the unproven segments in the design. This will also remove and add module
1584 \section{equiv
\_remove -- remove \$equiv cells
}
1585 \label{cmd:equiv_remove
}
1586 \begin{lstlisting
}[numbers=left,frame=single
]
1587 equiv_remove
[options
] [selection
]
1589 This command removes the selected $equiv cells. If neither -gold nor -gate is
1590 used then only proven cells are removed.
1599 \section{equiv
\_simple -- try proving simple \$equiv instances
}
1600 \label{cmd:equiv_simple
}
1601 \begin{lstlisting
}[numbers=left,frame=single
]
1602 equiv_simple
[options
] [selection
]
1604 This command tries to prove $equiv cells using a simple direct SAT approach.
1610 enable modelling of undef states
1613 create shorter input cones that stop at shared nodes. This yields
1614 simpler SAT problems but sometimes fails to prove equivalence.
1617 disabling grouping of $equiv cells by output wire
1620 the max. number of time steps to be considered (default =
1)
1623 \section{equiv
\_status -- print status of equivalent checking module
}
1624 \label{cmd:equiv_status
}
1625 \begin{lstlisting
}[numbers=left,frame=single
]
1626 equiv_status
[options
] [selection
]
1628 This command prints status information for all selected $equiv cells.
1631 produce an error if any unproven $equiv cell is found
1634 \section{equiv
\_struct -- structural equivalence checking
}
1635 \label{cmd:equiv_struct
}
1636 \begin{lstlisting
}[numbers=left,frame=single
]
1637 equiv_struct
[options
] [selection
]
1639 This command adds additional $equiv cells based on the assumption that the
1640 gold and gate circuit are structurally equivalent. Note that this can introduce
1641 bad $equiv cells in cases where the netlists are not structurally equivalent,
1642 for example when analyzing circuits with cells with commutative inputs. This
1643 command will also de-duplicate gates.
1646 by default this command performans forward sweeps until nothing can
1647 be merged by forwards sweeps, then backward sweeps until forward
1648 sweeps are effective again. with this option set only forward sweeps
1652 add the specified cell type to the list of cell types that are only
1653 merged in forward sweeps and never in backward sweeps. $equiv is in
1654 this list automatically.
1657 by default, the internal RTL and gate cell types are ignored. add
1658 this option to also process those cell types with this command.
1661 maximum number of iterations to run before aborting
1664 \section{eval -- evaluate the circuit given an input
}
1666 \begin{lstlisting
}[numbers=left,frame=single
]
1667 eval
[options
] [selection
]
1669 This command evaluates the value of a signal given the value of all required
1672 -set <signal> <value>
1673 set the specified signal to the specified value.
1676 set all unspecified source signals to undef (x)
1679 create a truth table using the specified input signals
1682 show the value for the specified signal. if no -show option is passed
1683 then all output ports of the current module are used.
1686 \section{exec -- execute commands in the operating system shell
}
1688 \begin{lstlisting
}[numbers=left,frame=single
]
1689 exec
[options
] --
[command
]
1691 Execute a command in the operating system shell. All supplied arguments are
1692 concatenated and passed as a command to popen(
3). Whitespace is not guaranteed
1693 to be preserved, even if quoted. stdin and stderr are not connected, while stdout is
1694 logged unless the "-q" option is specified.
1698 Suppress stdout and stderr from subprocess
1700 -expect-return <int>
1701 Generate an error if popen() does not return specified value.
1702 May only be specified once; the final specified value is controlling
1703 if specified multiple times.
1705 -expect-stdout <regex>
1706 Generate an error if the specified regex does not match any line
1707 in subprocess's stdout. May be specified multiple times.
1709 -not-expect-stdout <regex>
1710 Generate an error if the specified regex matches any line
1711 in subprocess's stdout. May be specified multiple times.
1714 Example: exec -q -expect-return
0 -- echo "bananapie" | grep "nana"
1717 \section{expose -- convert internal signals to module ports
}
1719 \begin{lstlisting
}[numbers=left,frame=single
]
1720 expose
[options
] [selection
]
1722 This command exposes all selected internal signals of a module as additional
1726 only consider wires that are directly driven by register cell.
1729 when exposing a wire, create an input/output pair and cut the internal
1730 signal path at that wire.
1733 when exposing a wire, create an input port and disconnect the internal
1737 only expose those signals that are shared among the selected modules.
1738 this is useful for preparing modules for equivalence checking.
1741 also turn connections to instances of other modules to additional
1742 inputs and outputs and remove the module instances.
1745 turn flip-flops to sets of inputs and outputs.
1748 when creating new wire/port names, the original object name is suffixed
1749 with this separator (default: '.') and the port name or a type
1750 designator for the exposed signal.
1753 \section{extract -- find subcircuits and replace them with cells
}
1755 \begin{lstlisting
}[numbers=left,frame=single
]
1756 extract -map <map_file>
[options
] [selection
]
1757 extract -mine <out_file>
[options
] [selection
]
1759 This pass looks for subcircuits that are isomorphic to any of the modules
1760 in the given map file and replaces them with instances of this modules. The
1761 map file can be a Verilog source file
(*.v) or an RTLIL source file (*.il).
1764 use the modules in this file as reference. This option can be used
1768 use the modules in this in-memory design as reference. This option can
1769 be used multiple times.
1772 print debug output while analyzing
1775 also find instances with constant drivers. this may be much
1776 slower than the normal operation.
1779 normally builtin port swapping rules for internal cells are used per
1780 default. This turns that off, so e.g. 'a^b' does not match 'b^a'
1781 when this option is used.
1783 -compat <needle_type> <haystack_type>
1784 Per default, the cells in the map file (needle) must have the
1785 type as the cells in the active design (haystack). This option
1786 can be used to register additional pairs of types that should
1787 match. This option can be used multiple times.
1789 -swap <needle_type> <port1>,<port2>[,...]
1790 Register a set of swappable ports for a needle cell type.
1791 This option can be used multiple times.
1793 -perm <needle_type> <port1>,<port2>[,...] <portA>,<portB>[,...]
1794 Register a valid permutation of swappable ports for a needle
1795 cell type. This option can be used multiple times.
1797 -cell_attr <attribute_name>
1798 Attributes on cells with the given name must match.
1800 -wire_attr <attribute_name>
1801 Attributes on wires with the given name must match.
1804 Do not use parameters when matching cells.
1806 -ignore_param <cell_type> <parameter_name>
1807 Do not use this parameter when matching cells.
1809 This pass does not operate on modules with unprocessed processes in it.
1810 (I.e. the 'proc' pass should be used first to convert processes to netlists.)
1812 This pass can also be used for mining for frequent subcircuits. In this mode
1813 the following options are to be used instead of the -map option.
1816 mine for frequent subcircuits and write them to the given RTLIL file
1818 -mine_cells_span <min> <max>
1819 only mine for subcircuits with the specified number of cells
1822 -mine_min_freq <num>
1823 only mine for subcircuits with at least the specified number of matches
1826 -mine_limit_matches_per_module <num>
1827 when calculating the number of matches for a subcircuit, don't count
1828 more than the specified number of matches per module
1830 -mine_max_fanout <num>
1831 don't consider internal signals with more than <num> connections
1833 The modules in the map file may have the attribute 'extract_order' set to an
1834 integer value. Then this value is used to determine the order in which the pass
1835 tries to map the modules to the design (ascending, default value is 0).
1837 See 'help techmap' for a pass that does the opposite thing.
1840 \section{extract\_counter -- Extract GreenPak4 counter cells}
1841 \label{cmd:extract_counter}
1842 \begin{lstlisting}[numbers=left,frame=single]
1843 extract_counter [options] [selection]
1845 This pass converts non-resettable or async resettable down counters to
1846 counter cells. Use a target-specific 'techmap' map file to convert those cells
1847 to the actual target cells.
1850 Only extract counters up to N bits wide (default 64)
1853 Only extract counters at least N bits wide (default 2)
1856 Allow counters to have async reset (default yes)
1859 Look for up-counters, down-counters, or both (default down)
1862 Only allow parallel output from the counter to the listed cell types
1863 (if not specified, parallel outputs are not restricted)
1866 \section{extract\_fa -- find and extract full/half adders}
1867 \label{cmd:extract_fa}
1868 \begin{lstlisting}[numbers=left,frame=single]
1869 extract_fa [options] [selection]
1871 This pass extracts full/half adders from a gate-level design.
1874 Enable cell types (fa=full adder, ha=half adder)
1875 All types are enabled if none of this options is used
1878 Set maximum depth for extracted logic cones (default=20)
1881 Set maximum breadth for extracted logic cones (default=6)
1887 \section{extract\_reduce -- converts gate chains into \$reduce\_* cells}
1888 \label{cmd:extract_reduce}
1889 \begin{lstlisting}[numbers=left,frame=single]
1890 extract_reduce [options] [selection]
1892 converts gate chains into $reduce_* cells
1894 This command finds chains of $_AND_, $_OR_, and $_XOR_ cells and replaces them
1895 with their corresponding $reduce_* cells. Because this command only operates on
1896 these cell types, it is recommended to map the design to only these cell types
1897 using the `abc -g` command. Note that, in some cases, it may be more effective
1898 to map the design to only $_AND_ cells, run extract_reduce, map the remaining
1899 parts of the design to AND/OR/XOR cells, and run extract_reduce a second time.
1902 Allows matching of cells that have loads outside the chain. These cells
1903 will be replicated and folded into the $reduce_* cell, but the original
1904 cell will remain, driving its original loads.
1907 \section{extractinv -- extract explicit inverter cells for invertible cell pins}
1908 \label{cmd:extractinv}
1909 \begin{lstlisting}[numbers=left,frame=single]
1910 extractinv [options] [selection]
1912 Searches the design for all cells with invertible pins controlled by a cell
1913 parameter (eg. IS_CLK_INVERTED on many Xilinx cells) and removes the parameter.
1914 If the parameter was set to 1, inserts an explicit inverter cell in front of
1915 the pin instead. Normally used for output to ISE, which does not support the
1916 inversion parameters.
1918 To mark a cell port as invertible, use (* invertible_pin = "param_name" *)
1919 on the wire in the blackbox module. The parameter value should have
1920 the same width as the port, and will be effectively XORed with it.
1922 -inv <celltype> <portname_out>:<portname_in>
1923 Specifies the cell type to use for the inverters and its port names.
1924 This option is required.
1927 \section{flatten -- flatten design
}
1929 \begin{lstlisting
}[numbers=left,frame=single
]
1930 flatten
[options
] [selection
]
1932 This pass flattens the design by replacing cells by their implementation. This
1933 pass is very similar to the 'techmap' pass. The only difference is that this
1934 pass is using the current design as mapping library.
1936 Cells and/or modules with the 'keep_hierarchy' attribute set will not be
1937 flattened by this command.
1940 Ignore the 'whitebox' attribute on cell implementations.
1943 \section{flowmap -- pack LUTs with FlowMap
}
1945 \begin{lstlisting
}[numbers=left,frame=single
]
1946 flowmap
[options
] [selection
]
1948 This pass uses the FlowMap technology mapping algorithm to pack logic gates
1949 into k-LUTs with optimal depth. It allows mapping any circuit elements that can
1950 be evaluated with the `eval` pass, including cells with multiple output ports
1951 and multi-bit input and output ports.
1954 perform technology mapping for a k-LUT architecture. if not specified,
1958 only produce n-input or larger LUTs. if not specified, defaults to
1.
1960 -cells <cell>
[,<cell>,...
]
1961 map specified cells. if not specified, maps $_NOT_, $_AND_, $_OR_,
1962 $_XOR_ and $_MUX_, which are the outputs of the `simplemap` pass.
1965 perform depth relaxation and area minimization.
1967 -r-alpha n, -r-beta n, -r-gamma n
1968 parameters of depth relaxation heuristic potential function.
1969 if not specified, alpha=
8, beta=
2, gamma=
1.
1972 optimize for area by trading off at most n logic levels for fewer LUTs.
1973 n may be zero, to optimize for area without increasing depth.
1977 dump intermediate graphs.
1980 explain decisions performed during depth relaxation.
1983 \section{fmcombine -- combine two instances of a cell into one
}
1984 \label{cmd:fmcombine
}
1985 \begin{lstlisting
}[numbers=left,frame=single
]
1986 fmcombine
[options
] module_name gold_cell gate_cell
1988 This pass takes two cells, which are instances of the same module, and replaces
1989 them with one instance of a special 'combined' module, that effectively
1990 contains two copies of the original module, plus some formal properties.
1992 This is useful for formal test benches that check what differences in behavior
1993 a slight difference in input causes in a module.
1996 Insert assumptions that initially all FFs in both circuits have the
1997 same initial values.
2000 Do not duplicate $anyseq/$anyconst cells.
2003 Insert forward hint assumptions into the combined module.
2006 Insert backward hint assumptions into the combined module.
2007 (Backward hints are logically equivalend to fordward hits, but
2008 some solvers are faster with bwd hints, or even both -bwd and -fwd.)
2011 Don't insert hint assumptions into the combined module.
2012 (This should not provide any speedup over the original design, but
2013 strangely sometimes it does.)
2015 If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.
2018 \section{fminit -- set init values/sequences for formal
}
2020 \begin{lstlisting
}[numbers=left,frame=single
]
2021 fminit
[options
] <selection>
2023 This pass creates init constraints (for example for reset sequences) in a formal
2026 -seq <signal> <sequence>
2027 Set sequence using comma-separated list of values, use 'z for
2028 unconstrained bits. The last value is used for the remainder of the
2031 -set <signal> <value>
2032 Add constant value constraint
2036 Set clock for init sequences
2039 \section{freduce -- perform functional reduction
}
2041 \begin{lstlisting
}[numbers=left,frame=single
]
2042 freduce
[options
] [selection
]
2044 This pass performs functional reduction in the circuit. I.e. if two nodes are
2045 equivalent, they are merged to one node and one of the redundant drivers is
2046 disconnected. A subsequent call to 'clean' will remove the redundant drivers.
2049 enable verbose or very verbose output
2052 enable explicit handling of inverted signals
2055 stop after <n> reduction operations. this is mostly used for
2056 debugging the freduce command itself.
2059 dump the design to <prefix>_<module>_<num>.il after each reduction
2060 operation. this is mostly used for debugging the freduce command.
2062 This pass is undef-aware, i.e. it considers don't-care values for detecting
2065 All selected wires are considered for rewiring. The selected cells cover the
2066 circuit that is analyzed.
2069 \section{fsm -- extract and optimize finite state machines
}
2071 \begin{lstlisting
}[numbers=left,frame=single
]
2072 fsm
[options
] [selection
]
2074 This pass calls all the other fsm_* passes in a useful order. This performs
2075 FSM extraction and optimization. It also calls opt_clean as needed:
2077 fsm_detect unless got option -nodetect
2084 fsm_expand if got option -expand
2085 opt_clean if got option -expand
2086 fsm_opt if got option -expand
2088 fsm_recode unless got option -norecode
2092 fsm_export if got option -export
2093 fsm_map unless got option -nomap
2097 -expand, -norecode, -export, -nomap
2098 enable or disable passes as indicated above
2101 call expand with -full option
2104 -fm_set_fsm_file file
2106 passed through to fsm_recode pass
2109 \section{fsm
\_detect -- finding FSMs in design
}
2110 \label{cmd:fsm_detect
}
2111 \begin{lstlisting
}[numbers=left,frame=single
]
2112 fsm_detect
[selection
]
2114 This pass detects finite state machines by identifying the state signal.
2115 The state signal is then marked by setting the attribute 'fsm_encoding'
2116 on the state signal to "auto".
2118 Existing 'fsm_encoding' attributes are not changed by this pass.
2120 Signals can be protected from being detected by this pass by setting the
2121 'fsm_encoding' attribute to "none".
2124 \section{fsm
\_expand -- expand FSM cells by merging logic into it
}
2125 \label{cmd:fsm_expand
}
2126 \begin{lstlisting
}[numbers=left,frame=single
]
2127 fsm_expand
[-full
] [selection
]
2129 The fsm_extract pass is conservative about the cells that belong to a finite
2130 state machine. This pass can be used to merge additional auxiliary gates into
2131 the finite state machine.
2133 By default, fsm_expand is still a bit conservative regarding merging larger
2134 word-wide cells. Call with -full to consider all cells for merging.
2137 \section{fsm
\_export -- exporting FSMs to KISS2 files
}
2138 \label{cmd:fsm_export
}
2139 \begin{lstlisting
}[numbers=left,frame=single
]
2140 fsm_export
[-noauto
] [-o filename
] [-origenc
] [selection
]
2142 This pass creates a KISS2 file for every selected FSM. For FSMs with the
2143 'fsm_export' attribute set, the attribute value is used as filename, otherwise
2144 the module and cell name is used as filename. If the parameter '-o' is given,
2145 the first exported FSM is written to the specified filename. This overwrites
2146 the setting as specified with the 'fsm_export' attribute. All other FSMs are
2147 exported to the default name as mentioned above.
2150 only export FSMs that have the 'fsm_export' attribute set
2153 filename of the first exported FSM
2156 use binary state encoding as state names instead of s0, s1, ...
2159 \section{fsm
\_extract -- extracting FSMs in design
}
2160 \label{cmd:fsm_extract
}
2161 \begin{lstlisting
}[numbers=left,frame=single
]
2162 fsm_extract
[selection
]
2164 This pass operates on all signals marked as FSM state signals using the
2165 'fsm_encoding' attribute. It consumes the logic that creates the state signal
2166 and uses the state signal to generate control signal and replaces it with an
2169 The generated FSM cell still generates the original state signal with its
2170 original encoding. The 'fsm_opt' pass can be used in combination with the
2171 'opt_clean' pass to eliminate this signal.
2174 \section{fsm
\_info -- print information on finite state machines
}
2175 \label{cmd:fsm_info
}
2176 \begin{lstlisting
}[numbers=left,frame=single
]
2177 fsm_info
[selection
]
2179 This pass dumps all internal information on FSM cells. It can be useful for
2180 analyzing the synthesis process and is called automatically by the 'fsm'
2181 pass so that this information is included in the synthesis log file.
2184 \section{fsm
\_map -- mapping FSMs to basic logic
}
2186 \begin{lstlisting
}[numbers=left,frame=single
]
2189 This pass translates FSM cells to flip-flops and logic.
2192 \section{fsm
\_opt -- optimize finite state machines
}
2194 \begin{lstlisting
}[numbers=left,frame=single
]
2197 This pass optimizes FSM cells. It detects which output signals are actually
2198 not used and removes them from the FSM. This pass is usually used in
2199 combination with the 'opt_clean' pass (see also 'help fsm').
2202 \section{fsm
\_recode -- recoding finite state machines
}
2203 \label{cmd:fsm_recode
}
2204 \begin{lstlisting
}[numbers=left,frame=single
]
2205 fsm_recode
[options
] [selection
]
2207 This pass reassign the state encodings for FSM cells. At the moment only
2208 one-hot encoding and binary encoding is supported.
2210 specify the encoding scheme used for FSMs without the
2211 'fsm_encoding' attribute or with the attribute set to `auto'.
2213 -fm_set_fsm_file <file>
2214 generate a file containing the mapping from old to new FSM encoding
2215 in form of Synopsys Formality set_fsm_* commands.
2218 write the mappings from old to new FSM encoding to a file in the
2221 .fsm <module_name> <state_signal>
2222 .map <old_bitpattern> <new_bitpattern>
2225 \section{fst2tb -- generate testbench out of fst file
}
2227 \begin{lstlisting
}[numbers=left,frame=single
]
2228 fst2tb
[options
] [top-level
]
2230 This command generates testbench for the circuit using the given top-level module
2231 and simulus signal from FST file
2234 generated testbench name.
2235 files <name>.v and <name>.txt are created as result.
2238 read simulation FST file
2241 name of top-level clock input
2244 name of top-level clock input (inverse polarity)
2247 scope of simulation top model
2250 start co-simulation in arbitary time (default
0)
2253 stop co-simulation in arbitary time (default END)
2256 number of clock cycles to simulate (default:
20)
2259 \section{glift -- create GLIFT models and optimization problems
}
2261 \begin{lstlisting
}[numbers=left,frame=single
]
2262 glift <command>
[options
] [selection
]
2264 Augments the current or specified module with gate-level information flow tracking
2265 (GLIFT) logic using the "constructive mapping" approach. Also can set up QBF-SAT
2266 optimization problems in order to optimize GLIFT models or trade off precision and
2272 -create-precise-model
2273 Replaces the current or specified module with one that has corresponding "taint"
2274 inputs, outputs, and internal nets along with precise taint tracking logic.
2275 For example, precise taint tracking logic for an AND gate is:
2277 y_t = a & b_t | b & a_t | a_t & b_t
2280 -create-imprecise-model
2281 Replaces the current or specified module with one that has corresponding "taint"
2282 inputs, outputs, and internal nets along with imprecise "All OR" taint tracking
2288 -create-instrumented-model
2289 Replaces the current or specified module with one that has corresponding "taint"
2290 inputs, outputs, and internal nets along with
4 varying-precision versions of taint
2291 tracking logic. Which version of taint tracking logic is used for a given gate is
2292 determined by a MUX selected by an $anyconst cell. By default, unless the
2293 `-no-cost-model` option is provided, an additional wire named `__glift_weight` with
2294 the `keep` and `minimize` attributes is added to the module along with pmuxes and
2295 adders to calculate a rough estimate of the number of logic gates in the GLIFT model
2296 given an assignment for the $anyconst cells. The four versions of taint tracking logic
2297 for an AND gate are:
2298 y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`)
2301 y_t = a_t | b_t (like `-create-imprecise-model`)
2307 Constant values in the design are labeled as tainted.
2308 (default: label constants as un-tainted)
2311 Do not remove module outputs. Taint tracking outputs will appear in the module ports
2312 alongside the orignal outputs.
2313 (default: original module outputs are removed)
2316 Do not model logic area. Instead model the number of non-zero assignments to $anyconsts.
2317 Taint tracking logic versions vary in their size, but all reduced-precision versions are
2318 significantly smaller than the fully-precise version. A non-zero $anyconst assignment means
2319 that reduced-precision taint tracking logic was chosen for some gate.
2320 Only applicable in combination with `-create-instrumented-model`.
2321 (default: use a complex model and give that wire the "keep" and "minimize" attributes)
2324 Do not model taint tracking logic area and do not create a `__glift_weight` wire.
2325 Only applicable in combination with `-create-instrumented-model`.
2326 (default: model area and give that wire the "keep" and "minimize" attributes)
2329 Allow choice from more versions of (even simpler) taint tracking logic. A total
2330 of
8 versions of taint tracking logic will be added per gate, including the
4
2331 versions from `-create-instrumented-model` and these additional versions:
2338 Only applicable in combination with `-create-instrumented-model`.
2339 (default: do not add more versions of taint tracking logic.
2342 \section{greenpak4
\_dffinv -- merge greenpak4 inverters and DFF/latches
}
2343 \label{cmd:greenpak4_dffinv
}
2344 \begin{lstlisting
}[numbers=left,frame=single
]
2345 greenpak4_dffinv
[options
] [selection
]
2347 Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells.
2350 \section{help -- display help messages
}
2352 \begin{lstlisting
}[numbers=left,frame=single
]
2353 help ................ list all commands
2354 help <command> ...... print help message for given command
2355 help -all ........... print complete command reference
2357 help -cells .......... list all cell types
2358 help <celltype> ..... print help message for given cell type
2359 help <celltype>+ .... print verilog code for given cell type
2362 \section{hierarchy -- check, expand and clean up design hierarchy
}
2363 \label{cmd:hierarchy
}
2364 \begin{lstlisting
}[numbers=left,frame=single
]
2365 hierarchy
[-check
] [-top <module>
]
2366 hierarchy -generate <cell-types> <port-decls>
2368 In parametric designs, a module might exists in several variations with
2369 different parameter values. This pass looks at all modules in the current
2370 design and re-runs the language frontends for the parametric modules as
2371 needed. It also resolves assignments to wired logic data types (wand/wor),
2372 resolves positional module parameters, unrolls array instances, and more.
2375 also check the design hierarchy. this generates an error when
2376 an unknown module is used as cell type.
2379 like -check, but also throw an error if blackbox modules are
2380 instantiated, and throw an error if the design has no top module.
2383 by default the hierarchy command will not remove library (blackbox)
2384 modules. use this option to also remove unused blackbox modules.
2387 search for files named <module_name>.v in the specified directory
2388 for unknown modules and automatically run read_verilog for each
2392 per default this pass also converts positional arguments in cells
2393 to arguments using port names. This option disables this behavior.
2396 per default this pass adjusts the port width on cells that are
2397 module instances when the width does not match the module port. This
2398 option disables this behavior.
2401 do not resolve input port default values
2404 per default this pass sets the "keep" attribute on all modules
2405 that directly or indirectly contain one or more formal properties.
2406 This option disables this behavior.
2409 use the specified top module to build the design hierarchy. Modules
2410 outside this tree (unused modules) are removed.
2412 when the -top option is used, the 'top' attribute will be set on the
2413 specified top module. otherwise a module with the 'top' attribute set
2414 will implicitly be used as top module, if such a module exists.
2417 automatically determine the top of the design hierarchy and mark it.
2420 elaborate the top module using this parameter value. Modules on which
2421 this parameter does not exist may cause a warning message to be output.
2422 This option can be specified multiple times to override multiple
2423 parameters. String values must be passed in double quotes (").
2425 In -generate mode this pass generates blackbox modules for the given cell
2426 types (wildcards supported). For this the design is searched for cells that
2427 match the given types and then the given port declarations are used to
2428 determine the direction of the ports. The syntax for a port declaration is:
2430 {i|o|io
}[@<num>
]:<portname>
2432 Input ports are specified with the 'i' prefix, output ports with the 'o'
2433 prefix and inout ports with the 'io' prefix. The optional <num> specifies
2434 the position of the port in the parameter list (needed when instantiated
2435 using positional arguments). When <num> is not specified, the <portname> can
2436 also contain wildcard characters.
2438 This pass ignores the current selection and always operates on all modules
2439 in the current design.
2442 \section{hilomap -- technology mapping of constant hi- and/or lo-drivers
}
2444 \begin{lstlisting
}[numbers=left,frame=single
]
2445 hilomap
[options
] [selection
]
2447 Map constants to 'tielo' and 'tiehi' driver cells.
2449 -hicell <celltype> <portname>
2450 Replace constant hi bits with this cell.
2452 -locell <celltype> <portname>
2453 Replace constant lo bits with this cell.
2456 Create only one hi/lo cell and connect all constant bits
2457 to that cell. Per default a separate cell is created for
2461 \section{history -- show last interactive commands
}
2463 \begin{lstlisting
}[numbers=left,frame=single
]
2466 This command prints all commands in the shell history buffer. This are
2467 all commands executed in an interactive session, but not the commands
2468 from executed scripts.
2471 \section{ice40
\_braminit -- iCE40: perform SB
\_RAM40\_4K initialization from file
}
2472 \label{cmd:ice40_braminit
}
2473 \begin{lstlisting
}[numbers=left,frame=single
]
2476 This command processes all SB_RAM40_4K blocks with a non-empty INIT_FILE
2477 parameter and converts it into the required INIT_x attributes
2480 \section{ice40
\_dsp -- iCE40: map multipliers
}
2481 \label{cmd:ice40_dsp
}
2482 \begin{lstlisting
}[numbers=left,frame=single
]
2483 ice40_dsp
[options
] [selection
]
2485 Map multipliers ($mul/SB_MAC16) and multiply-accumulate ($mul/SB_MAC16 + $add)
2486 cells into iCE40 DSP resources.
2487 Currently, only the
16x16 multiply mode is supported and not the
2 x
8x8 mode.
2489 Pack input registers (A, B,
{C,D
}; with optional hold), pipeline registers
2490 (
{F,J,K,G
}, H), output registers (O -- full
32-bits or lower
16-bits only; with
2491 optional hold), and post-adder into into the SB_MAC16 resource.
2493 Multiply-accumulate operations using the post-adder with feedback on the
{C,D
}
2494 input will be folded into the DSP. In this scenario only, resetting the
2495 the accumulator to an arbitrary value can be inferred to use the
{C,D
} input.
2498 \section{ice40
\_opt -- iCE40: perform simple optimizations
}
2499 \label{cmd:ice40_opt
}
2500 \begin{lstlisting
}[numbers=left,frame=single
]
2501 ice40_opt
[options
] [selection
]
2503 This command executes the following script:
2506 <ice40 specific optimizations>
2507 opt_expr -mux_undef -undriven
[-full
]
2511 while <changed design>
2514 \section{ice40
\_wrapcarry -- iCE40: wrap carries
}
2515 \label{cmd:ice40_wrapcarry
}
2516 \begin{lstlisting
}[numbers=left,frame=single
]
2517 ice40_wrapcarry
[selection
]
2519 Wrap manually instantiated SB_CARRY cells, along with their associated SB_LUT4s,
2520 into an internal $__ICE40_CARRY_WRAPPER cell for preservation across technology
2523 Attributes on both cells will have their names prefixed with 'SB_CARRY.' or
2524 'SB_LUT4.' and attached to the wrapping cell.
2525 A
(* keep *) attribute on either cell will be logically OR-ed together.
2528 unwrap $__ICE40_CARRY_WRAPPER cells back into SB_CARRYs and SB_LUT4s,
2529 including restoring their attributes.
2532 \section{insbuf -- insert buffer cells for connected wires
}
2534 \begin{lstlisting
}[numbers=left,frame=single
]
2535 insbuf
[options
] [selection
]
2537 Insert buffer cells into the design for directly connected wires.
2539 -buf <celltype> <in-portname> <out-portname>
2540 Use the given cell type instead of $_BUF_. (Notice that the next
2541 call to "clean" will remove all $_BUF_ in the design.)
2544 \section{iopadmap -- technology mapping of i/o pads (or buffers)
}
2545 \label{cmd:iopadmap
}
2546 \begin{lstlisting
}[numbers=left,frame=single
]
2547 iopadmap
[options
] [selection
]
2549 Map module inputs/outputs to PAD cells from a library. This pass
2550 can only map to very simple PAD cells. Use 'techmap' to further map
2551 the resulting cells to more sophisticated PAD cells.
2553 -inpad <celltype> <in_port>
[:<ext_port>
]
2554 Map module input ports to the given cell type with the
2555 given output port name. if a
2nd portname is given, the
2556 signal is passed through the pad cell, using the
2nd
2557 portname as the port facing the module port.
2559 -outpad <celltype> <out_port>
[:<ext_port>
]
2560 -inoutpad <celltype> <io_port>
[:<ext_port>
]
2561 Similar to -inpad, but for output and inout ports.
2563 -toutpad <celltype> <oe_port>:<out_port>
[:<ext_port>
]
2564 Merges $_TBUF_ cells into the output pad cell. This takes precedence
2565 over the other -outpad cell. The first portname is the enable input
2566 of the tristate driver, which can be prefixed with `~` for negative
2569 -tinoutpad <celltype> <oe_port>:<in_port>:<out_port>
[:<ext_port>
]
2570 Merges $_TBUF_ cells into the inout pad cell. This takes precedence
2571 over the other -inoutpad cell. The first portname is the enable input
2572 of the tristate driver and the
2nd portname is the internal output
2573 buffering the external signal. Like with `-toutpad`, the enable can
2574 be marked as negative polarity by prefixing the name with `~`.
2576 -ignore <celltype> <portname>
[:<portname>
]*
2577 Skips mapping inputs/outputs that are already connected to given
2578 ports of the given cell. Can be used multiple times. This is in
2579 addition to the cells specified as mapping targets.
2581 -widthparam <param_name>
2582 Use the specified parameter name to set the port width.
2584 -nameparam <param_name>
2585 Use the specified parameter to set the port name.
2588 create individual bit-wide buffers even for ports that
2589 are wider. (the default behavior is to create word-wide
2590 buffers using -widthparam to set the word size on the cell.)
2592 Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode.
2595 \section{jny -- write design and metadata
}
2597 \begin{lstlisting
}[numbers=left,frame=single
]
2598 jny
[options
] [selection
]
2600 Write a JSON netlist metadata for the current design
2603 write to the specified file.
2606 Don't include connection information in the netlist output.
2609 Don't include attributed information in the netlist output.
2612 Don't include property information in the netlist output.
2614 See 'help write_jny' for a description of the JSON format used.
2617 \section{json -- write design in JSON format
}
2619 \begin{lstlisting
}[numbers=left,frame=single
]
2620 json
[options
] [selection
]
2622 Write a JSON netlist of all selected objects.
2625 write to the specified file.
2628 also include AIG models for the different gate types
2631 emit
32-bit or smaller fully-defined parameter values directly
2632 as JSON numbers (for compatibility with old parsers)
2634 See 'help write_json' for a description of the JSON format used.
2637 \section{log -- print text and log files
}
2639 \begin{lstlisting
}[numbers=left,frame=single
]
2642 Print the given string to the screen and/or the log file. This is useful for TCL
2643 scripts, because the TCL command "puts" only goes to stdout but not to
2647 Print the output to stdout too. This is useful when all Yosys is executed
2648 with a script and the -q (quiet operation) argument to notify the user.
2651 Print the output to stderr too.
2654 Don't use the internal log() command. Use either -stdout or -stderr,
2655 otherwise no output will be generated at all.
2658 do not append a newline
2661 \section{logger -- set logger properties
}
2663 \begin{lstlisting
}[numbers=left,frame=single
]
2666 This command sets global logger properties, also available using command line
2670 enable/disable display of timestamp in log output.
2673 enable/disable logging errors to stderr.
2676 print a warning for all log messages matching the regex.
2679 if a warning message matches the regex, it is printed as regular
2683 if a warning message matches the regex, it is printed as error
2684 message instead and the tool terminates with a nonzero return code.
2687 globally enable/disable debug log messages.
2689 -experimental <feature>
2690 do not print warnings for the specified experimental feature
2692 -expect <type> <regex> <expected_count>
2693 expect log, warning or error to appear. matched errors will terminate
2697 gives error in case there is at least one warning that is not expected.
2700 verifies that the patterns previously set up by -expect have actually
2701 been met, then clears the expected log list. If this is not called
2702 manually, the check will happen at yosys exist time instead.
2705 \section{ls -- list modules or objects in modules
}
2707 \begin{lstlisting
}[numbers=left,frame=single
]
2710 When no active module is selected, this prints a list of modules.
2712 When an active module is selected, this prints a list of objects in the module.
2715 \section{ltp -- print longest topological path
}
2717 \begin{lstlisting
}[numbers=left,frame=single
]
2718 ltp
[options
] [selection
]
2720 This command prints the longest topological path in the design. (Only considers
2721 paths within a single module, so the design must be flattened.)
2724 automatically exclude FF cell types
2727 \section{lut2mux -- convert \$lut to \$
\_MUX\_}
2729 \begin{lstlisting
}[numbers=left,frame=single
]
2730 lut2mux
[options
] [selection
]
2732 This pass converts $lut cells to $_MUX_ gates.
2735 \section{maccmap -- mapping macc cells
}
2737 \begin{lstlisting
}[numbers=left,frame=single
]
2738 maccmap
[-unmap
] [selection
]
2740 This pass maps $macc cells to yosys $fa and $alu cells. When the -unmap option
2741 is used then the $macc cell is mapped to $add, $sub, etc. cells instead.
2744 \section{memory -- translate memories to basic cells
}
2746 \begin{lstlisting
}[numbers=left,frame=single
]
2747 memory
[-nomap
] [-nordff
] [-nowiden
] [-nosat
] [-memx
] [-bram <bram_rules>
] [selection
]
2749 This pass calls all the other memory_* passes in a useful order:
2754 memory_dff (skipped if called with -nordff or -memx)
2756 memory_share
[-nowiden
] [-nosat
]
2758 memory_memx (when called with -memx)
2761 memory_bram -rules <bram_rules> (when called with -bram)
2762 memory_map (skipped if called with -nomap)
2764 This converts memories to word-wide DFFs and address decoders
2765 or multiport memory blocks if called with the -nomap option.
2768 \section{memory
\_bram -- map memories to block rams
}
2769 \label{cmd:memory_bram
}
2770 \begin{lstlisting
}[numbers=left,frame=single
]
2771 memory_bram -rules <rule_file>
[selection
]
2773 This pass converts the multi-port $mem memory cells into block ram instances.
2774 The given rules file describes the available resources and how they should be
2777 The rules file contains configuration options, a set of block ram description
2778 and a sequence of match rules.
2780 The option 'attr_icase' configures how attribute values are matched. The value
0
2781 means case-sensitive,
1 means case-insensitive.
2783 A block ram description looks like this:
2785 bram RAMB1024X32 # name of BRAM cell
2786 init
1 # set to '
1' if BRAM can be initialized
2787 abits
10 # number of address bits
2788 dbits
32 # number of data bits
2789 groups
2 # number of port groups
2790 ports
1 1 # number of ports in each group
2791 wrmode
1 0 # set to '
1' if this groups is write ports
2792 enable
4 1 # number of enable bits
2793 transp
0 2 # transparent (for read ports)
2794 clocks
1 2 # clock configuration
2795 clkpol
2 2 # clock polarity configuration
2798 For the option 'transp' the value
0 means non-transparent,
1 means transparent
2799 and a value greater than
1 means configurable. All groups with the same
2800 value greater than
1 share the same configuration bit.
2802 For the option 'clocks' the value
0 means non-clocked, and a value greater
2803 than
0 means clocked. All groups with the same value share the same clock
2806 For the option 'clkpol' the value
0 means negative edge,
1 means positive edge
2807 and a value greater than
1 means configurable. All groups with the same value
2808 greater than
1 share the same configuration bit.
2810 Using the same bram name in different bram blocks will create different variants
2811 of the bram. Verilog configuration parameters for the bram are created as needed.
2813 It is also possible to create variants by repeating statements in the bram block
2814 and appending '@<label>' to the individual statements.
2816 A match rule looks like this:
2819 max waste
16384 # only use this bram if <=
16k ram bits are unused
2820 min efficiency
80 # only use this bram if efficiency is at least
80%
2823 It is possible to match against the following values with min/max rules:
2825 words ........ number of words in memory in design
2826 abits ........ number of address bits on memory in design
2827 dbits ........ number of data bits on memory in design
2828 wports ....... number of write ports on memory in design
2829 rports ....... number of read ports on memory in design
2830 ports ........ number of ports on memory in design
2831 bits ......... number of bits in memory in design
2832 dups .......... number of duplications for more read ports
2834 awaste ....... number of unused address slots for this match
2835 dwaste ....... number of unused data bits for this match
2836 bwaste ....... number of unused bram bits for this match
2837 waste ........ total number of unused bram bits (bwaste*dups)
2838 efficiency ... total percentage of used and non-duplicated bits
2840 acells ....... number of cells in 'address-direction'
2841 dcells ....... number of cells in 'data-direction'
2842 cells ........ total number of cells (acells*dcells*dups)
2844 A match containing the command 'attribute' followed by a list of space
2845 separated 'name
[=string_value
]' values requires that the memory contains any
2846 one of the given attribute name and string values (where specified), or name
2847 and integer
1 value (if no string_value given, since Verilog will interpret
2848 '
(* attr *)' as '
(* attr=1 *)').
2849 A name prefixed with '!' indicates that the attribute must not exist.
2851 The interface for the created bram instances is derived from the bram
2852 description. Use 'techmap' to convert the created bram instances into
2853 instances of the actual bram cells of your target architecture.
2855 A match containing the command 'or_next_if_better' is only used if it
2856 has a higher efficiency than the next match (and the one after that if
2857 the next also has 'or_next_if_better' set, and so forth).
2859 A match containing the command 'make_transp' will add external circuitry
2860 to simulate 'transparent read', if necessary.
2862 A match containing the command 'make_outreg' will add external flip-flops
2863 to implement synchronous read ports, if necessary.
2865 A match containing the command 'shuffle_enable A' will re-organize
2866 the data bits to accommodate the enable pattern of port A.
2869 \section{memory
\_collect -- creating multi-port memory cells
}
2870 \label{cmd:memory_collect
}
2871 \begin{lstlisting
}[numbers=left,frame=single
]
2872 memory_collect
[selection
]
2874 This pass collects memories and memory ports and creates generic multiport
2878 \section{memory
\_dff -- merge input/output DFFs into memory read ports
}
2879 \label{cmd:memory_dff
}
2880 \begin{lstlisting
}[numbers=left,frame=single
]
2881 memory_dff
[options
] [selection
]
2883 This pass detects DFFs at memory read ports and merges them into the memory port.
2884 I.e. it consumes an asynchronous memory port and the flip-flops at its
2885 interface and yields a synchronous memory port.
2888 \section{memory
\_map -- translate multiport memories to basic cells
}
2889 \label{cmd:memory_map
}
2890 \begin{lstlisting
}[numbers=left,frame=single
]
2891 memory_map
[options
] [selection
]
2893 This pass converts multiport memory cells as generated by the memory_collect
2894 pass to word-wide DFFs and address decoders.
2897 do not map memories that have attribute <name> set.
2899 -attr <name>
[=<value>
]
2900 for memories that have attribute <name> set, only map them if its value
2901 is a string <value> (if specified), or an integer
1 (otherwise). if this
2902 option is specified multiple times, map the memory if the attribute is
2903 to any of the values.
2906 for -attr, ignore case of <value>.
2909 \section{memory
\_memx -- emulate vlog sim behavior for mem ports
}
2910 \label{cmd:memory_memx
}
2911 \begin{lstlisting
}[numbers=left,frame=single
]
2912 memory_memx
[selection
]
2914 This pass adds additional circuitry that emulates the Verilog simulation
2915 behavior for out-of-bounds memory reads and writes.
2918 \section{memory
\_narrow -- split up wide memory ports
}
2919 \label{cmd:memory_narrow
}
2920 \begin{lstlisting
}[numbers=left,frame=single
]
2921 memory_narrow
[options
] [selection
]
2923 This pass splits up wide memory ports into several narrow ports.
2926 \section{memory
\_nordff -- extract read port FFs from memories
}
2927 \label{cmd:memory_nordff
}
2928 \begin{lstlisting
}[numbers=left,frame=single
]
2929 memory_nordff
[options
] [selection
]
2931 This pass extracts FFs from memory read ports. This results in a netlist
2932 similar to what one would get from not calling memory_dff.
2935 \section{memory
\_share -- consolidate memory ports
}
2936 \label{cmd:memory_share
}
2937 \begin{lstlisting
}[numbers=left,frame=single
]
2938 memory_share
[-nosat
] [-nowiden
] [selection
]
2940 This pass merges share-able memory ports into single memory ports.
2942 The following methods are used to consolidate the number of memory ports:
2944 - When multiple write ports access the same address then this is converted
2945 to a single write port with a more complex data and/or enable logic path.
2947 - When multiple read or write ports access adjacent aligned addresses, they are
2948 merged to a single wide read or write port. This transformation can be
2949 disabled with the "-nowiden" option.
2951 - When multiple write ports are never accessed at the same time (a SAT
2952 solver is used to determine this), then the ports are merged into a single
2953 write port. This transformation can be disabled with the "-nosat" option.
2955 Note that in addition to the algorithms implemented in this pass, the $memrd
2956 and $memwr cells are also subject to generic resource sharing passes (and other
2957 optimizations) such as "share" and "opt_merge".
2960 \section{memory
\_unpack -- unpack multi-port memory cells
}
2961 \label{cmd:memory_unpack
}
2962 \begin{lstlisting
}[numbers=left,frame=single
]
2963 memory_unpack
[selection
]
2965 This pass converts the multi-port $mem memory cells into individual $memrd and
2966 $memwr cells. It is the counterpart to the memory_collect pass.
2969 \section{miter -- automatically create a miter circuit
}
2971 \begin{lstlisting
}[numbers=left,frame=single
]
2972 miter -equiv
[options
] gold_name gate_name miter_name
2974 Creates a miter circuit for equivalence checking. The gold- and gate- modules
2975 must have the same interfaces. The miter circuit will have all inputs of the
2976 two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'
2977 output that goes high if an output mismatch between the two source modules is
2981 a undef (x) bit in the gold module output will match any value in
2982 the gate module output.
2985 also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs
2986 on the miter circuit.
2989 also create a cmp_* output for each gold/gate output pair.
2992 also create an 'assert' cell that checks if trigger is always low.
2995 call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.
2998 miter -assert
[options
] module
[miter_name
]
3000 Creates a miter circuit for property checking. All input ports are kept,
3001 output ports are discarded. An additional output 'trigger' is created that
3002 goes high when an assert is violated. Without a miter_name, the existing
3006 keep module output ports.
3009 call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.
3012 \section{mutate -- generate or apply design mutations
}
3014 \begin{lstlisting
}[numbers=left,frame=single
]
3015 mutate -list N
[options
] [selection
]
3017 Create a list of N mutations using an even sampling.
3020 Write list to this file instead of console output
3023 Write a list of all src tags found in the design to the specified file
3026 RNG seed for selecting mutations
3029 Include a "none" mutation in the output
3031 -ctrl name width value
3032 Add -ctrl options to the output. Use 'value' for first mutation, then
3033 simply count up from there.
3044 Filter list of mutation candidates to those matching
3045 the given parameters.
3048 Set a configuration option. Options available:
3049 weight_pq_w weight_pq_b weight_pq_c weight_pq_s
3050 weight_pq_mw weight_pq_mb weight_pq_mc weight_pq_ms
3051 weight_cover pick_cover_prcnt
3054 mutate -mode MODE
[options
]
3056 Apply the given mutation.
3058 -ctrl name width value
3059 Add a control signal with the given name and width. The mutation is
3060 activated if the control signal equals the given value.
3067 Mutation parameters, as generated by 'mutate -list N'.
3072 Ignored. (They are generated by -list for documentation purposes.)
3075 \section{muxcover -- cover trees of MUX cells with wider MUXes
}
3076 \label{cmd:muxcover
}
3077 \begin{lstlisting
}[numbers=left,frame=single
]
3078 muxcover
[options
] [selection
]
3080 Cover trees of $_MUX_ cells with $_MUX
{4,
8,
16}_ cells
3082 -mux4
[=cost
], -mux8
[=cost
], -mux16
[=cost
]
3083 Cover $_MUX_ trees using the specified types of MUXes (with optional
3084 integer costs). If none of these options are given, the effect is the
3085 same as if all of them are.
3086 Default costs: $_MUX4_ =
220, $_MUX8_ =
460,
3090 Use the specified cost for $_MUX_ cells when making covering decisions.
3091 Default cost: $_MUX_ =
100
3094 Use the specified cost for $_MUX_ cells used in decoders.
3098 Do not insert decoder logic. This reduces the number of possible
3099 substitutions, but guarantees that the resulting circuit is not
3100 less efficient than the original circuit.
3103 Do not consider mappings that use $_MUX<N>_ to select from less
3104 than <N> different signals.
3107 \section{muxpack -- \$mux/\$pmux cascades to \$pmux
}
3109 \begin{lstlisting
}[numbers=left,frame=single
]
3112 This pass converts cascaded chains of $pmux cells (e.g. those create from case
3113 constructs) and $mux cells (e.g. those created by if-else constructs) into
3116 This optimisation is conservative --- it will only pack $mux or $pmux cells
3117 whose select lines are driven by '$eq' cells with other such cells if it can be
3118 certain that their select inputs are mutually exclusive.
3121 \section{nlutmap -- map to LUTs of different sizes
}
3123 \begin{lstlisting
}[numbers=left,frame=single
]
3124 nlutmap
[options
] [selection
]
3126 This pass uses successive calls to 'abc' to map to an architecture. That
3127 provides a small number of differently sized LUTs.
3129 -luts N_1,N_2,N_3,...
3130 The number of LUTs with
1,
2,
3, ... inputs that are
3131 available in the target architecture.
3134 Create an error if not all logic can be mapped
3136 Excess logic that does not fit into the specified LUTs is mapped back
3137 to generic logic gates ($_AND_, etc.).
3140 \section{onehot -- optimize \$eq cells for onehot signals
}
3142 \begin{lstlisting
}[numbers=left,frame=single
]
3143 onehot
[options
] [selection
]
3145 This pass optimizes $eq cells that compare one-hot signals against constants
3151 \section{opt -- perform simple optimizations
}
3153 \begin{lstlisting
}[numbers=left,frame=single
]
3154 opt
[options
] [selection
]
3156 This pass calls all the other opt_* passes in a useful order. This performs
3157 a series of trivial optimizations and cleanups. This pass executes the other
3158 passes in the following order:
3160 opt_expr
[-mux_undef
] [-mux_bool
] [-undriven
] [-noclkinv
] [-fine
] [-full
] [-keepdc
]
3161 opt_merge
[-share_all
] -nomux
3165 opt_reduce
[-fine
] [-full
]
3166 opt_merge
[-share_all
]
3167 opt_share (-full only)
3168 opt_dff
[-nodffe
] [-nosdff
] [-keepdc
] [-sat
] (except when called with -noff)
3170 opt_expr
[-mux_undef
] [-mux_bool
] [-undriven
] [-noclkinv
] [-fine
] [-full
] [-keepdc
]
3171 while <changed design>
3173 When called with -fast the following script is used instead:
3176 opt_expr
[-mux_undef
] [-mux_bool
] [-undriven
] [-noclkinv
] [-fine
] [-full
] [-keepdc
]
3177 opt_merge
[-share_all
]
3178 opt_dff
[-nodffe
] [-nosdff
] [-keepdc
] [-sat
] (except when called with -noff)
3180 while <changed design in opt_dff>
3182 Note: Options in square brackets (such as
[-keepdc
]) are passed through to
3183 the opt_* commands when given to 'opt'.
3186 \section{opt
\_clean -- remove unused cells and wires
}
3187 \label{cmd:opt_clean
}
3188 \begin{lstlisting
}[numbers=left,frame=single
]
3189 opt_clean
[options
] [selection
]
3191 This pass identifies wires and cells that are unused and removes them. Other
3192 passes often remove cells but leave the wires in the design or reconnect the
3193 wires but leave the old cells in the design. This pass can be used to clean up
3194 after the passes that do the actual work.
3196 This pass only operates on completely selected modules without processes.
3199 also remove internal nets if they have a public name
3202 \section{opt
\_demorgan -- Optimize reductions with DeMorgan equivalents
}
3203 \label{cmd:opt_demorgan
}
3204 \begin{lstlisting
}[numbers=left,frame=single
]
3205 opt_demorgan
[selection
]
3207 This pass pushes inverters through $reduce_* cells if this will reduce the
3208 overall gate count of the circuit
3211 \section{opt
\_dff -- perform DFF optimizations
}
3213 \begin{lstlisting
}[numbers=left,frame=single
]
3214 opt_dff
[-nodffe
] [-nosdff
] [-keepdc
] [-sat
] [selection
]
3216 This pass converts flip-flops to a more suitable type by merging clock enables
3217 and synchronous reset multiplexers, removing unused control inputs, or potentially
3218 removes the flip-flop altogether, converting it to a constant driver.
3221 disables dff -> dffe conversion, and other transforms recognizing clock enable
3224 disables dff -> sdff conversion, and other transforms recognizing sync resets
3227 only enables clock enable recognition transform for obvious cases
3230 additionally invoke SAT solver to detect and remove flip-flops (with
3231 non-constant inputs) that can also be replaced with a constant driver
3234 some optimizations change the behavior of the circuit with respect to
3235 don't-care bits. for example in 'a+
0' a single x-bit in 'a' will cause
3236 all result bits to be set to x. this behavior changes when 'a+
0' is
3237 replaced by 'a'. the -keepdc option disables all such optimizations.
3240 \section{opt
\_expr -- perform const folding and simple expression rewriting
}
3241 \label{cmd:opt_expr
}
3242 \begin{lstlisting
}[numbers=left,frame=single
]
3243 opt_expr
[options
] [selection
]
3245 This pass performs const folding on internal cell types with constant inputs.
3246 It also performs some simple expression rewriting.
3249 remove 'undef' inputs from $mux, $pmux and $_MUX_ cells
3252 replace $mux cells with inverters or buffers when possible
3255 replace undriven nets with undef (x) constants
3258 do not optimize clock inverters by changing FF types
3261 perform fine-grain optimizations
3264 alias for -mux_undef -mux_bool -undriven -fine
3267 some optimizations change the behavior of the circuit with respect to
3268 don't-care bits. for example in 'a+
0' a single x-bit in 'a' will cause
3269 all result bits to be set to x. this behavior changes when 'a+
0' is
3270 replaced by 'a'. the -keepdc option disables all such optimizations.
3273 \section{opt
\_lut -- optimize LUT cells
}
3275 \begin{lstlisting
}[numbers=left,frame=single
]
3276 opt_lut
[options
] [selection
]
3278 This pass combines cascaded $lut cells with unused inputs.
3280 -dlogic <type>:<cell-port>=<LUT-input>
[:<cell-port>=<LUT-input>...
]
3281 preserve connections to dedicated logic cell <type> that has ports
3282 <cell-port> connected to LUT inputs <LUT-input>. this includes
3283 the case where both LUT and dedicated logic input are connected to
3287 only perform the first N combines, then stop. useful for debugging.
3290 \section{opt
\_lut\_ins -- discard unused LUT inputs
}
3291 \label{cmd:opt_lut_ins
}
3292 \begin{lstlisting
}[numbers=left,frame=single
]
3293 opt_lut_ins
[options
] [selection
]
3295 This pass removes unused inputs from LUT cells (that is, inputs that can not
3296 influence the output signal given this LUT's value). While such LUTs cannot
3297 be directly emitted by ABC, they can be a result of various post-ABC
3298 transformations, such as mapping wide LUTs (not all sub-LUTs will use the
3299 full set of inputs) or optimizations such as xilinx_dffopt.
3302 Instead of generic $lut cells, operate on LUT cells specific
3303 to the given technology. Valid values are: xilinx, ecp5, gowin.
3306 \section{opt
\_mem -- optimize memories
}
3308 \begin{lstlisting
}[numbers=left,frame=single
]
3309 opt_mem
[options
] [selection
]
3311 This pass performs various optimizations on memories in the design.
3314 \section{opt
\_mem\_feedback -- convert memory read-to-write port feedback paths to write enables
}
3315 \label{cmd:opt_mem_feedback
}
3316 \begin{lstlisting
}[numbers=left,frame=single
]
3317 opt_mem_feedback
[selection
]
3319 This pass detects cases where an asynchronous read port is only connected via
3320 a mux tree to a write port with the same address. When such a connection is
3321 found, it is replaced with a new condition on an enable signal, allowing
3322 for removal of the read port.
3325 \section{opt
\_mem\_priority -- remove priority relations between write ports that can never collide
}
3326 \label{cmd:opt_mem_priority
}
3327 \begin{lstlisting
}[numbers=left,frame=single
]
3328 opt_mem_priority
[selection
]
3330 This pass detects cases where one memory write port has priority over another
3331 even though they can never collide with each other -- ie. there can never be
3332 a situation where a given memory bit is written by both ports at the same
3333 time, for example because of always-different addresses, or mutually exclusive
3334 enable signals. In such cases, the priority relation is removed.
3337 \section{opt
\_mem\_widen -- optimize memories where all ports are wide
}
3338 \label{cmd:opt_mem_widen
}
3339 \begin{lstlisting
}[numbers=left,frame=single
]
3340 opt_mem_widen
[options
] [selection
]
3342 This pass looks for memories where all ports are wide and adjusts the base
3343 memory width up until that stops being the case.
3346 \section{opt
\_merge -- consolidate identical cells
}
3347 \label{cmd:opt_merge
}
3348 \begin{lstlisting
}[numbers=left,frame=single
]
3349 opt_merge
[options
] [selection
]
3351 This pass identifies cells with identical type and input signals. Such cells
3352 are then merged to one cell.
3355 Do not merge MUX cells.
3358 Operate on all cell types, not just built-in types.
3361 Do not merge flipflops with don't-care bits in their initial value.
3364 \section{opt
\_muxtree -- eliminate dead trees in multiplexer trees
}
3365 \label{cmd:opt_muxtree
}
3366 \begin{lstlisting
}[numbers=left,frame=single
]
3367 opt_muxtree
[selection
]
3369 This pass analyzes the control signals for the multiplexer trees in the design
3370 and identifies inputs that can never be active. It then removes this dead
3371 branches from the multiplexer trees.
3373 This pass only operates on completely selected modules without processes.
3376 \section{opt
\_reduce -- simplify large MUXes and AND/OR gates
}
3377 \label{cmd:opt_reduce
}
3378 \begin{lstlisting
}[numbers=left,frame=single
]
3379 opt_reduce
[options
] [selection
]
3381 This pass performs two interlinked optimizations:
3383 1. it consolidates trees of large AND gates or OR gates and eliminates
3386 2. it identifies duplicated inputs to MUXes and replaces them with a single
3387 input with the original control signals OR'ed together.
3390 perform fine-grain optimizations
3396 \section{opt
\_share -- merge mutually exclusive cells of the same type that share an input signal
}
3397 \label{cmd:opt_share
}
3398 \begin{lstlisting
}[numbers=left,frame=single
]
3399 opt_share
[selection
]
3401 This pass identifies mutually exclusive cells of the same type that:
3402 (a) share an input signal,
3403 (b) drive the same $mux, $_MUX_, or $pmux multiplexing cell,
3405 allowing the cell to be merged and the multiplexer to be moved from
3406 multiplexing its output to multiplexing the non-shared input signals.
3409 \section{paramap -- renaming cell parameters
}
3411 \begin{lstlisting
}[numbers=left,frame=single
]
3412 paramap
[options
] [selection
]
3414 This command renames cell parameters and/or maps key/value pairs to
3415 other key/value pairs.
3418 Match attribute names case-insensitively and set it to the specified
3421 -rename <old_name> <new_name>
3422 Rename attributes as specified
3424 -map <old_name>=<old_value> <new_name>=<new_value>
3425 Map key/value pairs as indicated.
3427 -imap <old_name>=<old_value> <new_name>=<new_value>
3428 Like -map, but use case-insensitive match for <old_value> when
3429 it is a string value.
3431 -remove <name>=<value>
3432 Remove attributes matching this pattern.
3434 For example, mapping Diamond-style ECP5 "init" attributes to Yosys-style:
3436 paramap -tocase INIT t:LUT4
3439 \section{peepopt -- collection of peephole optimizers
}
3441 \begin{lstlisting
}[numbers=left,frame=single
]
3442 peepopt
[options
] [selection
]
3444 This pass applies a collection of peephole optimizers to the current design.
3447 \section{plugin -- load and list loaded plugins
}
3449 \begin{lstlisting
}[numbers=left,frame=single
]
3452 Load and list loaded plugins.
3454 -i <plugin_filename>
3455 Load (install) the specified plugin.
3458 Register the specified alias name for the loaded plugin
3464 \section{pmux2shiftx -- transform \$pmux cells to \$shiftx cells
}
3465 \label{cmd:pmux2shiftx
}
3466 \begin{lstlisting
}[numbers=left,frame=single
]
3467 pmux2shiftx
[options
] [selection
]
3469 This pass transforms $pmux cells to $shiftx cells.
3474 -min_density <percentage>
3475 specifies the minimum density for the shifter
3479 specified the minimum number of choices for a control signal
3482 -onehot ignore|pmux|shiftx
3483 select strategy for one-hot encoded control signals
3487 disable $sub inference for "range decoders"
3490 \section{pmuxtree -- transform \$pmux cells to trees of \$mux cells
}
3491 \label{cmd:pmuxtree
}
3492 \begin{lstlisting
}[numbers=left,frame=single
]
3493 pmuxtree
[selection
]
3495 This pass transforms $pmux cells to trees of $mux cells.
3498 \section{portlist -- list (top-level) ports
}
3499 \label{cmd:portlist
}
3500 \begin{lstlisting
}[numbers=left,frame=single
]
3501 portlist
[options
] [selection
]
3503 This command lists all module ports found in the selected modules.
3505 If no selection is provided then it lists the ports on the top module.
3508 print verilog blackbox module definitions instead of port lists
3511 \section{prep -- generic synthesis script
}
3513 \begin{lstlisting
}[numbers=left,frame=single
]
3516 This command runs a conservative RTL synthesis. A typical application for this
3517 is the preparation stage of a verification flow. This command does not operate
3518 on partly selected designs.
3521 use the specified module as top module (default='top')
3524 automatically determine the top of the design hierarchy
3527 flatten the design before synthesis. this will pass '-auto-top' to
3528 'hierarchy' if no top module is specified.
3531 passed to 'proc'. uses verilog simulation behavior for verilog if/case
3532 undef handling. this also prevents 'wreduce' from being run.
3535 simulate verilog simulation behavior for out-of-bounds memory accesses
3536 using the 'memory_memx' pass.
3539 do not run any of the memory_* passes
3542 call 'memory_dff'. This enables merging of FFs into
3546 do not call opt_* with -keepdc
3548 -run <from_label>
[:<to_label>
]
3549 only run the commands between the labels (see below). an empty
3550 from label is synonymous to 'begin', and empty to label is
3551 synonymous to the end of the command list.
3554 The following commands are executed by this synthesis command:
3557 hierarchy -check
[-top <top> | -auto-top
]
3561 flatten (if -flatten)
3566 wreduce -keepdc
[-memx
]
3567 memory_dff (if -rdff)
3568 memory_memx (if -memx)
3571 opt -noff -keepdc -fast
3578 \section{printattrs -- print attributes of selected objects
}
3579 \label{cmd:printattrs
}
3580 \begin{lstlisting
}[numbers=left,frame=single
]
3581 printattrs
[selection
]
3583 Print all attributes of the selected objects.
3586 \section{proc -- translate processes to netlists
}
3588 \begin{lstlisting
}[numbers=left,frame=single
]
3589 proc
[options
] [selection
]
3591 This pass calls all the other proc_* passes in the most common order.
3605 This replaces the processes in the design with multiplexers,
3606 flip-flops and latches.
3608 The following options are supported:
3611 Will omit the proc_mux pass.
3613 -global_arst
[!
]<netname>
3614 This option is passed through to proc_arst.
3617 This option is passed through to proc_mux. proc_rmdead is not
3618 executed in -ifx mode.
3621 Will omit the opt_expr pass.
3624 \section{proc
\_arst -- detect asynchronous resets
}
3625 \label{cmd:proc_arst
}
3626 \begin{lstlisting
}[numbers=left,frame=single
]
3627 proc_arst
[-global_arst
[!
]<netname>
] [selection
]
3629 This pass identifies asynchronous resets in the processes and converts them
3630 to a different internal representation that is suitable for generating
3631 flip-flop cells with asynchronous resets.
3633 -global_arst
[!
]<netname>
3634 In modules that have a net with the given name, use this net as async
3635 reset for registers that have been assign initial values in their
3636 declaration ('reg foobar = constant_value;'). Use the '!' modifier for
3637 active low reset signals. Note: the frontend stores the default value
3638 in the 'init' attribute on the net.
3641 \section{proc
\_clean -- remove empty parts of processes
}
3642 \label{cmd:proc_clean
}
3643 \begin{lstlisting
}[numbers=left,frame=single
]
3644 proc_clean
[options
] [selection
]
3647 do not print any messages.
3649 This pass removes empty parts of processes and ultimately removes a process
3650 if it contains only empty structures.
3653 \section{proc
\_dff -- extract flip-flops from processes
}
3654 \label{cmd:proc_dff
}
3655 \begin{lstlisting
}[numbers=left,frame=single
]
3656 proc_dff
[selection
]
3658 This pass identifies flip-flops in the processes and converts them to
3659 d-type flip-flop cells.
3662 \section{proc
\_dlatch -- extract latches from processes
}
3663 \label{cmd:proc_dlatch
}
3664 \begin{lstlisting
}[numbers=left,frame=single
]
3665 proc_dlatch
[selection
]
3667 This pass identifies latches in the processes and converts them to
3671 \section{proc
\_init -- convert initial block to init attributes
}
3672 \label{cmd:proc_init
}
3673 \begin{lstlisting
}[numbers=left,frame=single
]
3674 proc_init
[selection
]
3676 This pass extracts the 'init' actions from processes (generated from Verilog
3677 'initial' blocks) and sets the initial value to the 'init' attribute on the
3681 \section{proc
\_memwr -- extract memory writes from processes
}
3682 \label{cmd:proc_memwr
}
3683 \begin{lstlisting
}[numbers=left,frame=single
]
3684 proc_memwr
[selection
]
3686 This pass converts memory writes in processes into $memwr cells.
3689 \section{proc
\_mux -- convert decision trees to multiplexers
}
3690 \label{cmd:proc_mux
}
3691 \begin{lstlisting
}[numbers=left,frame=single
]
3692 proc_mux
[options
] [selection
]
3694 This pass converts the decision trees in processes (originating from if-else
3695 and case statements) to trees of multiplexer cells.
3698 Use Verilog simulation behavior with respect to undef values in
3699 'case' expressions and 'if' conditions.
3702 \section{proc
\_prune -- remove redundant assignments
}
3703 \label{cmd:proc_prune
}
3704 \begin{lstlisting
}[numbers=left,frame=single
]
3705 proc_prune
[selection
]
3707 This pass identifies assignments in processes that are always overwritten by
3708 a later assignment to the same signal and removes them.
3711 \section{proc
\_rmdead -- eliminate dead trees in decision trees
}
3712 \label{cmd:proc_rmdead
}
3713 \begin{lstlisting
}[numbers=left,frame=single
]
3714 proc_rmdead
[selection
]
3716 This pass identifies unreachable branches in decision trees and removes them.
3719 \section{qbfsat -- solve a
2QBF-SAT problem in the circuit
}
3721 \begin{lstlisting
}[numbers=left,frame=single
]
3722 qbfsat
[options
] [selection
]
3724 This command solves an "exists-forall"
2QBF-SAT problem defined over the currently
3725 selected module. Existentially-quantified variables are declared by assigning a wire
3726 "$anyconst". Universally-quantified variables may be explicitly declared by assigning
3727 a wire "$allconst", but module inputs will be treated as universally-quantified
3728 variables by default.
3731 Do not delete temporary files and directories. Useful for debugging.
3733 -dump-final-smt2 <file>
3734 Pass the --dump-smt2 option to yosys-smtbmc.
3737 Add an "$assume" cell for the conjunction of all one-bit module output wires.
3739 -assume-negative-polarity
3740 When adding $assume cells for one-bit module output wires, assume they are
3741 negative polarity signals and should always be low, for example like the
3742 miters created with the `miter` command.
3745 Ignore "
\minimize" and "
\maximize" attributes, do not emit "(maximize)" or
3746 "(minimize)" in the SMT-LIBv2, and generally make no attempt to optimize anything.
3749 If a wire is marked with the "
\minimize" or "
\maximize" attribute, do not
3750 attempt to optimize that value with the default iterated solving and threshold
3751 bisection approach. Instead, have yosys-smtbmc emit a "(minimize)" or "(maximize)"
3752 command in the SMT-LIBv2 output and hope that the solver supports optimizing
3753 quantified bitvector problems.
3756 Use a particular solver. Choose one of: "z3", "yices", and "cvc4".
3759 -solver-option <name> <value>
3760 Set the specified solver option in the SMT-LIBv2 problem file.
3763 Set the per-iteration timeout in seconds.
3764 (default: no timeout)
3767 Control the use of ABC to simplify the QBF-SAT problem before solving.
3770 Generate an error if the solver does not return "sat".
3773 Generate an error if the solver does not return "unsat".
3776 Print the output from yosys-smtbmc.
3779 If the problem is satisfiable, replace each "$anyconst" cell with its
3780 corresponding constant value from the model produced by the solver.
3782 -specialize-from-file <solution file>
3783 Do not run the solver, but instead only attempt to replace each "$anyconst"
3784 cell in the current module with a constant value provided by the specified file.
3786 -write-solution <solution file>
3787 If the problem is satisfiable, write the corresponding constant value for each
3788 "$anyconst" cell from the model produced by the solver to the specified file.
3791 \section{qwp -- quadratic wirelength placer
}
3793 \begin{lstlisting
}[numbers=left,frame=single
]
3794 qwp
[options
] [selection
]
3796 This command runs quadratic wirelength placement on the selected modules and
3797 annotates the cells in the design with 'qwp_position' attributes.
3800 Add left-to-right constraints: constrain all inputs on the left border
3801 outputs to the right border.
3804 Add constraints for inputs/outputs to be placed in alphanumerical
3805 order along the y-axis (top-to-bottom).
3808 Number of grid divisions in x- and y-direction. (default=
16)
3810 -dump <html_file_name>
3811 Dump a protocol of the placement algorithm to the html file.
3814 Verbose solver output for profiling or debugging
3816 Note: This implementation of a quadratic wirelength placer uses exact
3817 dense matrix operations. It is only a toy-placer for small circuits.
3820 \section{read -- load HDL designs
}
3822 \begin{lstlisting
}[numbers=left,frame=single
]
3823 read
{-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal
} <verilog-file>..
3825 Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support
3826 is only available via Verific.)
3828 Additional -D<macro>
[=<value>
] options may be added after the option indicating
3829 the language version (and before file names) to set additional verilog defines.
3832 read
{-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl
} <vhdl-file>..
3834 Load the specified VHDL files. (Requires Verific.)
3837 read
{-f|-F
} <command-file>
3839 Load and execute the specified command file. (Requires Verific.)
3840 Check verific command for more information about supported commands in file.
3843 read -define <macro>
[=<value>
]..
3845 Set global Verilog/SystemVerilog defines.
3848 read -undef <macro>..
3850 Unset global Verilog/SystemVerilog defines.
3853 read -incdir <directory>
3855 Add directory to global Verilog/SystemVerilog include directories.
3861 Subsequent calls to 'read' will either use or not use Verific. Calling 'read'
3862 with -verific will result in an error on Yosys binaries that are built without
3863 Verific support. The default is to use Verific if it is available.
3866 \section{read
\_aiger -- read AIGER file
}
3867 \label{cmd:read_aiger
}
3868 \begin{lstlisting
}[numbers=left,frame=single
]
3869 read_aiger
[options
] [filename
]
3871 Load module from an AIGER file into the current design.
3873 -module_name <module_name>
3874 name of module to be created (default: <filename>)
3876 -clk_name <wire_name>
3877 if specified, AIGER latches to be transformed into $_DFF_P_ cells
3878 clocked by wire of this name. otherwise, $_FF_ cells will be used
3881 read file with port and latch symbols
3884 merge ports that match the pattern 'name
[int
]' into a single
3885 multi-bit port 'name'
3888 read XAIGER extensions
3891 \section{read
\_blif -- read BLIF file
}
3892 \label{cmd:read_blif
}
3893 \begin{lstlisting
}[numbers=left,frame=single
]
3894 read_blif
[options
] [filename
]
3896 Load modules from a BLIF file into the current design.
3899 Create $sop cells instead of $lut cells
3902 Merge ports that match the pattern 'name
[int
]' into a single
3903 multi-bit port 'name'.
3906 \section{read
\_ilang -- (deprecated) alias of read
\_rtlil}
3907 \label{cmd:read_ilang
}
3908 \begin{lstlisting
}[numbers=left,frame=single
]
3909 See `help read_rtlil`.
3912 \section{read
\_json -- read JSON file
}
3913 \label{cmd:read_json
}
3914 \begin{lstlisting
}[numbers=left,frame=single
]
3915 read_json
[filename
]
3917 Load modules from a JSON file into the current design See "help write_json"
3918 for a description of the file format.
3921 \section{read
\_liberty -- read cells from liberty file
}
3922 \label{cmd:read_liberty
}
3923 \begin{lstlisting
}[numbers=left,frame=single
]
3924 read_liberty
[filename
]
3926 Read cells from liberty file as modules into current design.
3929 only create empty blackbox modules
3932 ignore re-definitions of modules. (the default behavior is to
3933 create an error message if the existing module is not a blackbox
3934 module, and overwrite the existing module if it is a blackbox module.)
3937 overwrite existing modules with the same name
3940 ignore cells with missing function specification of outputs
3943 ignore cells with a missing or invalid direction
3944 specification on a pin
3946 -ignore_miss_data_latch
3947 ignore latches with missing data and/or enable pins
3949 -setattr <attribute_name>
3950 set the specified attribute (to the value
1) on all loaded modules
3953 \section{read
\_rtlil -- read modules from RTLIL file
}
3954 \label{cmd:read_rtlil
}
3955 \begin{lstlisting
}[numbers=left,frame=single
]
3956 read_rtlil
[filename
]
3958 Load modules from an RTLIL file to the current design. (RTLIL is a text
3959 representation of a design in yosys's internal format.)
3962 ignore re-definitions of modules. (the default behavior is to
3963 create an error message if the existing module is not a blackbox
3964 module, and overwrite the existing module if it is a blackbox module.)
3967 overwrite existing modules with the same name
3970 only create empty blackbox modules
3973 \section{read
\_verilog -- read modules from Verilog file
}
3974 \label{cmd:read_verilog
}
3975 \begin{lstlisting
}[numbers=left,frame=single
]
3976 read_verilog
[options
] [filename
]
3978 Load modules from a Verilog file to the current design. A large subset of
3979 Verilog-
2005 is supported.
3982 enable support for SystemVerilog features. (only a small subset
3983 of SystemVerilog is supported)
3986 enable support for SystemVerilog assertions and some Yosys extensions
3987 replace the implicit -D SYNTHESIS with -D FORMAL
3990 don't add implicit -D SYNTHESIS
3993 ignore assert() statements
3996 ignore assume() statements
3999 ignore restrict() statements
4002 treat all assert() statements like assume() statements
4005 treat all assume() statements like assert() statements
4008 alias for -dump_ast1 -dump_ast2 -dump_vlog1 -dump_vlog2 -yydebug
4011 dump abstract syntax tree (before simplification)
4014 dump abstract syntax tree (after simplification)
4017 do not include hex memory addresses in dump (easier to diff dumps)
4020 dump ast as Verilog code (before simplification)
4023 dump ast as Verilog code (after simplification)
4026 dump generated RTLIL netlist
4029 enable parser debug output
4032 usually latches are synthesized into logic loops
4033 this option prohibits this and sets the output to 'x'
4034 in what would be the latches hold condition
4036 this behavior can also be achieved by setting the
4037 'nolatches' attribute on the respective module or
4041 under certain conditions memories are converted to registers
4042 early during simplification to ensure correct handling of
4043 complex corner cases. this option disables this behavior.
4045 this can also be achieved by setting the 'nomem2reg'
4046 attribute on the respective module or register.
4048 This is potentially dangerous. Usually the front-end has good
4049 reasons for converting an array to a list of registers.
4050 Prohibiting this step will likely result in incorrect synthesis
4054 always convert memories to registers. this can also be
4055 achieved by setting the 'mem2reg' attribute on the respective
4059 do not infer $meminit cells and instead convert initialized
4060 memories to registers directly in the front-end.
4063 dump Verilog code after pre-processor
4066 do not run the pre-processor
4069 disable DPI-C support
4072 do not automatically add a
(* blackbox *) attribute to an
4076 only create empty blackbox modules. This implies -DBLACKBOX.
4077 modules with the
(* whitebox *) attribute will be preserved.
4078 (* lib_whitebox *) will be treated like
(* whitebox *).
4081 delete
(* whitebox *) and
(* lib_whitebox *) attributes from
4085 parse and import specify blocks
4088 don't perform basic optimizations (such as const folding) in the
4089 high-level front-end.
4092 interpret cell types starting with '$' as internal cell types
4095 add a wire for each module parameter
4098 ignore re-definitions of modules. (the default behavior is to
4099 create an error message if the existing module is not a black box
4100 module, and overwrite the existing module otherwise.)
4103 overwrite existing modules with the same name
4106 only read the abstract syntax tree and defer actual compilation
4107 to a later 'hierarchy' command. Useful in cases where the default
4108 parameters of modules yield invalid or not synthesizable code.
4111 make the default of `default_nettype be "none" instead of "wire".
4113 -setattr <attribute_name>
4114 set the specified attribute (to the value
1) on all loaded modules
4117 define the preprocessor symbol 'name' and set its optional value
4121 add 'dir' to the directories which are used when searching include
4124 The command 'verilog_defaults' can be used to register default options for
4125 subsequent calls to 'read_verilog'.
4127 Note that the Verilog frontend does a pretty good job of processing valid
4128 verilog input, but has not very good error reporting. It generally is
4129 recommended to use a simulator (for example Icarus Verilog) for checking
4130 the syntax of the code, rather than to rely on read_verilog for that.
4132 Depending on if read_verilog is run in -formal mode, either the macro
4133 SYNTHESIS or FORMAL is defined automatically, unless -nosynthesis is used.
4134 In addition, read_verilog always defines the macro YOSYS.
4136 See the Yosys README file for a list of non-standard Verilog features
4137 supported by the Yosys Verilog front-end.
4140 \section{rename -- rename object in the design
}
4142 \begin{lstlisting
}[numbers=left,frame=single
]
4143 rename old_name new_name
4145 Rename the specified object. Note that selection patterns are not supported
4150 rename -output old_name new_name
4152 Like above, but also make the wire an output. This will fail if the object is
4156 rename -src
[selection
]
4158 Assign names auto-generated from the src attribute to all selected wires and
4159 cells with private names.
4162 rename -wire
[selection
]
4164 Assign auto-generated names based on the wires they drive to all selected
4165 cells with private names. Ignores cells driving privatly named wires.
4168 rename -enumerate
[-pattern <pattern>
] [selection
]
4170 Assign short auto-generated names to all selected wires and cells with private
4171 names. The -pattern option can be used to set the pattern for the new names.
4172 The character
% in the pattern is replaced with a integer number. The default
4176 rename -hide
[selection
]
4178 Assign private names (the ones with $-prefix) to all selected wires and cells
4179 with public names. This ignores all selected ports.
4182 rename -top new_name
4187 \section{rmports -- remove module ports with no connections
}
4189 \begin{lstlisting
}[numbers=left,frame=single
]
4192 This pass identifies ports in the selected modules which are not used or
4193 driven and removes them.
4196 \section{sat -- solve a SAT problem in the circuit
}
4198 \begin{lstlisting
}[numbers=left,frame=single
]
4199 sat
[options
] [selection
]
4201 This command solves a SAT problem defined over the currently selected circuit
4202 and additional constraints passed as parameters.
4205 show all solutions to the problem (this can grow exponentially, use
4206 -max <N> instead to get <N> solutions)
4209 like -all, but limit number of solutions to <N>
4212 enable modeling of undef value (aka 'x-bits')
4213 this option is implied by -set-def, -set-undef et. cetera
4216 maximize the number of undef bits in solutions, giving a better
4217 picture of which input bits are actually vital to the solution.
4219 -set <signal> <value>
4220 set the specified signal to the specified value.
4223 add a constraint that all bits of the given signal must be defined
4225 -set-any-undef <signal>
4226 add a constraint that at least one bit of the given signal is undefined
4228 -set-all-undef <signal>
4229 add a constraint that all bits of the given signal are undefined
4232 add -set-def constraints for all module inputs
4235 show the model for the specified signal. if no -show option is
4236 passed then a set of signals to be shown is automatically selected.
4238 -show-inputs, -show-outputs, -show-ports
4239 add all module (input/output) ports to the list of shown signals
4241 -show-regs, -show-public, -show-all
4242 show all registers, show signals with 'public' names, show all signals
4245 ignore all solutions that involve a division by zero
4247 -ignore_unknown_cells
4248 ignore all cells that can not be matched to a SAT model
4250 The following options can be used to set up a sequential problem:
4253 set up a sequential problem with <N> time steps. The steps will
4254 be numbered from
1 to N.
4256 note: for large <N> it can be significantly faster to use
4257 -tempinduct-baseonly -maxsteps <N> instead of -seq <N>.
4259 -set-at <N> <signal> <value>
4260 -unset-at <N> <signal>
4261 set or unset the specified signal to the specified value in the
4262 given timestep. this has priority over a -set for the same signal.
4265 set all assumptions provided via $assume cells
4267 -set-def-at <N> <signal>
4268 -set-any-undef-at <N> <signal>
4269 -set-all-undef-at <N> <signal>
4270 add undef constraints in the given timestep.
4272 -set-init <signal> <value>
4273 set the initial value for the register driving the signal to the value
4276 set all initial states (not set using -set-init) to undef
4279 do not force a value for the initial state but do not allow undef
4282 set all initial states (not set using -set-init) to zero
4284 -dump_vcd <vcd-file-name>
4285 dump SAT model (counter example in proof) to VCD file
4287 -dump_json <json-file-name>
4288 dump SAT model (counter example in proof) to a WaveJSON file.
4290 -dump_cnf <cnf-file-name>
4291 dump CNF of SAT problem (in DIMACS format). in temporal induction
4292 proofs this is the CNF of the first induction step.
4294 The following additional options can be used to set up a proof. If also -seq
4295 is passed, a temporal induction proof is performed.
4298 Perform a temporal induction proof. In a temporal induction proof it is
4299 proven that the condition holds forever after the number of time steps
4300 specified using -seq.
4303 Perform a temporal induction proof. Assume an initial state with all
4304 registers set to defined values for the induction step.
4306 -tempinduct-baseonly
4307 Run only the basecase half of temporal induction (requires -maxsteps)
4309 -tempinduct-inductonly
4310 Run only the induction half of temporal induction
4312 -tempinduct-skip <N>
4313 Skip the first <N> steps of the induction proof.
4315 note: this will assume that the base case holds for <N> steps.
4316 this must be proven independently with "-tempinduct-baseonly
4317 -maxsteps <N>". Use -initsteps if you just want to set a
4318 minimal induction length.
4320 -prove <signal> <value>
4321 Attempt to proof that <signal> is always <value>.
4323 -prove-x <signal> <value>
4324 Like -prove, but an undef (x) bit in the lhs matches any value on
4325 the right hand side. Useful for equivalence checking.
4328 Prove that all asserts in the design hold.
4331 Do not enforce the prove-condition for the first <N> time steps.
4334 Set a maximum length for the induction.
4337 Set initial length for the induction.
4338 This will speed up the search of the right induction length
4339 for deep induction proofs.
4342 Increase the size of the induction proof in steps of <N>.
4343 This will speed up the search of the right induction length
4344 for deep induction proofs.
4347 Maximum number of seconds a single SAT instance may take.
4350 Return an error and stop the synthesis script if the proof fails.
4353 Like -verify but do not return an error for timeouts.
4356 Return an error and stop the synthesis script if the proof succeeds.
4359 Like -falsify but do not return an error for timeouts.
4362 \section{scatter -- add additional intermediate nets
}
4364 \begin{lstlisting
}[numbers=left,frame=single
]
4367 This command adds additional intermediate nets on all cell ports. This is used
4368 for testing the correct use of the SigMap helper in passes. If you don't know
4369 what this means: don't worry -- you only need this pass when testing your own
4370 extensions to Yosys.
4372 Use the opt_clean command to get rid of the additional nets.
4375 \section{scc -- detect strongly connected components (logic loops)
}
4377 \begin{lstlisting
}[numbers=left,frame=single
]
4378 scc
[options
] [selection
]
4380 This command identifies strongly connected components (aka logic loops) in the
4384 expect to find exactly <num> SCCs. A different number of SCCs will
4388 limit to loops not longer than the specified number of cells. This
4389 can e.g. be useful in identifying small local loops in a module that
4390 implements one large SCC.
4393 do not count cells that have their output fed back into one of their
4394 inputs as single-cell scc.
4397 Usually this command only considers internal non-memory cells. With
4398 this option set, all cells are considered. For unknown cells all ports
4399 are assumed to be bidirectional 'inout' ports.
4401 -set_attr <name> <value>
4402 set the specified attribute on all cells that are part of a logic
4403 loop. the special token
{} in the value is replaced with a unique
4404 identifier for the logic loop.
4407 replace the current selection with a selection of all cells and wires
4408 that are part of a found logic loop
4411 examine specify rules to detect logic loops in whitebox/blackbox cells
4414 \section{scratchpad -- get/set values in the scratchpad
}
4415 \label{cmd:scratchpad
}
4416 \begin{lstlisting
}[numbers=left,frame=single
]
4417 scratchpad
[options
]
4419 This pass allows to read and modify values from the scratchpad of the current
4423 print the value saved in the scratchpad under the given identifier.
4425 -set <identifier> <value>
4426 save the given value in the scratchpad under the given identifier.
4429 remove the entry for the given identifier from the scratchpad.
4431 -copy <identifier_from> <identifier_to>
4432 copy the value of the first identifier to the second identifier.
4434 -assert <identifier> <value>
4435 assert that the entry for the given identifier is set to the given value.
4437 -assert-set <identifier>
4438 assert that the entry for the given identifier exists.
4440 -assert-unset <identifier>
4441 assert that the entry for the given identifier does not exist.
4443 The identifier may not contain whitespace. By convention, it is usually prefixed
4444 by the name of the pass that uses it, e.g. 'opt.did_something'. If the value
4445 contains whitespace, it must be enclosed in double quotes.
4448 \section{script -- execute commands from file or wire
}
4450 \begin{lstlisting
}[numbers=left,frame=single
]
4451 script <filename>
[<from_label>:<to_label>
]
4452 script -scriptwire
[selection
]
4454 This command executes the yosys commands in the specified file (default
4455 behaviour), or commands embedded in the constant text value connected to the
4458 In the default (file) case, the
2nd argument can be used to only execute the
4459 section of the file between the specified labels. An empty from label is
4460 synonymous with the beginning of the file and an empty to label is synonymous
4461 with the end of the file.
4463 If only one label is specified (without ':') then only the block
4464 marked with that label (until the next label) is executed.
4466 In "-scriptwire" mode, the commands on the selected wire(s) will be executed
4467 in the scope of (and thus, relative to) the wires' owning module(s). This
4468 '-module' mode can be exited by using the 'cd' command.
4471 \section{select -- modify and view the list of selected objects
}
4473 \begin{lstlisting
}[numbers=left,frame=single
]
4474 select
[ -add | -del | -set <name>
] {-read <filename> | <selection>
}
4475 select
[ -unset <name>
]
4476 select
[ <assert_option>
] {-read <filename> | <selection>
}
4477 select
[ -list | -write <filename> | -count | -clear
]
4478 select -module <modname>
4480 Most commands use the list of currently selected objects to determine which part
4481 of the design to operate on. This command can be used to modify and view this
4482 list of selected objects.
4484 Note that many commands support an optional
[selection
] argument that can be
4485 used to override the global selection for the command. The syntax of this
4486 optional argument is identical to the syntax of the <selection> argument
4490 add or remove the given objects to the current selection.
4491 without this options the current selection is replaced.
4494 do not modify the current selection. instead save the new selection
4495 under the given name (see @<name> below). to save the current selection,
4496 use "select -set <name>
%"
4499 do not modify the current selection. instead remove a previously saved
4500 selection under the given name (see @<name> below).
4502 do not modify the current selection. instead assert that the given
4503 selection is empty. i.e. produce an error if any object matching the
4507 do not modify the current selection. instead assert that the given
4508 selection is non-empty. i.e. produce an error if no object matching
4509 the selection is found.
4512 do not modify the current selection. instead assert that the given
4513 selection contains exactly N objects.
4516 do not modify the current selection. instead assert that the given
4517 selection contains less than or exactly N objects.
4520 do not modify the current selection. instead assert that the given
4521 selection contains at least N objects.
4524 list all objects in the current selection
4527 like -list but write the output to the specified file
4530 read the specified file (written by -write)
4533 count all objects in the current selection
4536 clear the current selection. this effectively selects the whole
4537 design. it also resets the selected module (see -module). use the
4538 command 'select *' to select everything but stay in the current module.
4541 create an empty selection. the current module is unchanged.
4544 limit the current scope to the specified module.
4545 the difference between this and simply selecting the module
4546 is that all object names are interpreted relative to this
4547 module after this command until the selection is cleared again.
4549 When this command is called without an argument, the current selection
4550 is displayed in a compact form (i.e. only the module name when a whole module
4553 The <selection> argument itself is a series of commands for a simple stack
4554 machine. Each element on the stack represents a set of selected objects.
4555 After this commands have been executed, the union of all remaining sets
4556 on the stack is computed and used as selection for the command.
4558 Pushing (selecting) object when not in -module mode:
4561 select the specified module(s)
4563 <mod_pattern>/<obj_pattern>
4564 select the specified object(s) from the module(s)
4566 Pushing (selecting) object when in -module mode:
4569 select the specified object(s) from the current module
4571 By default, patterns will not match black/white-box modules or theircontents. To include such objects, prefix the pattern with '='.
4573 A <mod_pattern> can be a module name, wildcard expression
(*, ?, [..])
4574 matching module names, or one of the following:
4576 A:<pattern>, A:<pattern>=<pattern>
4577 all modules with an attribute matching the given pattern
4578 in addition to = also <, <=, >=, and > are supported
4581 all modules with a name matching the given pattern
4582 (i.e. 'N:' is optional as it is the default matching rule)
4584 An <obj_pattern> can be an object name, wildcard expression, or one of
4588 all wires with a name matching the given wildcard pattern
4590 i:<pattern>, o:<pattern>, x:<pattern>
4591 all inputs (i:), outputs (o:) or any ports (x:) with matching names
4593 s:<size>, s:<min>:<max>
4594 all wires with a matching width
4597 all memories with a name matching the given pattern
4600 all cells with a name matching the given pattern
4603 all cells with a type matching the given pattern
4606 all processes with a name matching the given pattern
4609 all objects with an attribute name matching the given pattern
4611 a:<pattern>=<pattern>
4612 all objects with a matching attribute name-value-pair.
4613 in addition to = also <, <=, >=, and > are supported
4615 r:<pattern>, r:<pattern>=<pattern>
4616 cells with matching parameters. also with <, <=, >= and >.
4619 all objects with a name matching the given pattern
4620 (i.e. 'n:' is optional as it is the default matching rule)
4623 push the selection saved prior with 'select -set <name> ...'
4625 The following actions can be performed on the top sets on the stack:
4628 push a copy of the current selection to the stack
4631 replace the stack with a union of all elements on it
4634 replace top set with its invert
4637 replace the two top sets on the stack with their union
4640 replace the two top sets on the stack with their intersection
4643 pop the top set from the stack and subtract it from the new top
4646 like %d but swap the roles of two top sets on the stack
4649 create a copy of the top set from the stack and push it
4651 %x[<num1>|*][.<num2>][:<rule>[:<rule>..]]
4652 expand top set <num1> num times according to the specified rules.
4653 (i.e. select all cells connected to selected wires and select all
4654 wires connected to selected cells) The rules specify which cell
4655 ports to use for this. the syntax for a rule is a '-' for exclusion
4656 and a '+' for inclusion, followed by an optional comma separated
4657 list of cell types followed by an optional comma separated list of
4658 cell ports in square brackets. a rule can also be just a cell or wire
4659 name that limits the expansion (is included but does not go beyond).
4660 select at most <num2> objects. a warning message is printed when this
4661 limit is reached. When '*' is used instead of <num1> then the process
4662 is repeated until no further object are selected.
4664 %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]]
4665 %co[<num1>|*][.<num2>][:<rule>[:<rule>..]]
4666 similar to %x, but only select input (%ci) or output cones (%co)
4668 %xe[...] %cie[...] %coe
4669 like %x, %ci, and %co but only consider combinatorial cells
4672 expand top set by selecting all wires that are (at least in part)
4673 aliases for selected wires.
4676 expand top set by adding all modules that implement cells in selected
4680 expand top set by selecting all modules that contain selected objects
4683 select modules that implement selected cells
4686 select cells that implement selected modules
4689 select <num> random objects from top selection (default 1)
4691 Example: the following command selects all wires that are connected to a
4692 'GATE' input of a 'SWITCH' cell:
4694 select */t:SWITCH %x:+[GATE] */t:SWITCH %d
4697 \section{setattr -- set/unset attributes on objects}
4699 \begin{lstlisting}[numbers=left,frame=single]
4700 setattr [ -mod ] [ -set name value | -unset name ]... [selection]
4702 Set/unset the given attributes on the selected objects. String values must be
4703 passed in double quotes (").
4705 When called with -mod, this command will set and unset attributes on modules
4706 instead of objects within modules.
4709 \section{setparam -- set/unset parameters on objects}
4710 \label{cmd:setparam}
4711 \begin{lstlisting}[numbers=left,frame=single]
4712 setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection]
4714 Set/unset the given parameters on the selected cells. String values must be
4715 passed in double quotes (").
4717 The -type option can be used to change the cell type of the selected cells.
4720 \section{setundef -- replace undef values with defined constants}
4721 \label{cmd:setundef}
4722 \begin{lstlisting}[numbers=left,frame=single]
4723 setundef [options] [selection]
4725 This command replaces undef (x) constants with defined (0/1) constants.
4728 also set undriven nets to constant values
4731 also expose undriven nets as inputs (use with -undriven)
4734 replace with bits cleared (0)
4737 replace with bits set (1)
4740 replace with undef (x) bits, may be used with -undriven
4743 replace with $anyseq drivers (for formal)
4746 replace with $anyconst drivers (for formal)
4749 replace with random bits using the specified integer as seed
4750 value for the random number generator.
4753 also create/update init values for flip-flops
4756 replace undef in cell parameters
4759 \section{share -- perform sat-based resource sharing}
4761 \begin{lstlisting}[numbers=left,frame=single]
4762 share [options] [selection]
4764 This pass merges shareable resources into a single resource. A SAT solver
4765 is used to determine if two resources are share-able.
4768 Per default the selection of cells that is considered for sharing is
4769 narrowed using a list of cell types. With this option all selected
4770 cells are considered for resource sharing.
4772 IMPORTANT NOTE: If the -all option is used then no cells with internal
4773 state must be selected!
4776 Per default some heuristics are used to reduce the number of cells
4777 considered for resource sharing to only large resources. This options
4778 turns this heuristics off, resulting in much more cells being considered
4779 for resource sharing.
4782 Only consider the simple part of the control logic in SAT solving, resulting
4783 in much easier SAT problems at the cost of maybe missing some opportunities
4784 for resource sharing.
4787 Only perform the first N merges, then stop. This is useful for debugging.
4790 \section{shell -- enter interactive command mode}
4792 \begin{lstlisting}[numbers=left,frame=single]
4795 This command enters the interactive command mode. This can be useful
4796 in a script to interrupt the script at a certain point and allow for
4797 interactive inspection or manual synthesis of the design at this point.
4799 The command prompt of the interactive shell indicates the current
4800 selection (see 'help select'):
4803 the entire design is selected
4806 only part of the design is selected
4809 the entire module 'modname' is selected using 'select -module modname'
4812 only part of current module 'modname' is selected
4814 When in interactive shell, some errors (e.g. invalid command arguments)
4815 do not terminate yosys but return to the command prompt.
4817 This command is the default action if nothing else has been specified
4818 on the command line.
4820 Press Ctrl-D or type 'exit' to leave the interactive shell.
4823 \section{show -- generate schematics using graphviz}
4825 \begin{lstlisting}[numbers=left,frame=single]
4826 show [options] [selection]
4828 Create a graphviz DOT file for the selected part of the design and compile it
4829 to a graphics file (usually SVG or PostScript).
4832 Run the specified command with the graphics file as parameter.
4833 On Windows, this pauses yosys until the viewer exits.
4836 Generate a graphics file in the specified format. Use 'dot' to just
4837 generate a .dot file, or other <format> strings such as 'svg' or 'ps'
4838 to generate files in other formats (this calls the 'dot' command).
4840 -lib <verilog_or_rtlil_file>
4841 Use the specified library file for determining whether cell ports are
4842 inputs or outputs. This option can be used multiple times to specify
4843 more than one library.
4845 note: in most cases it is better to load the library before calling
4846 show with 'read_verilog -lib <filename>'. it is also possible to
4847 load liberty files with 'read_liberty -lib <filename>'.
4850 generate <prefix>.* instead of ~/.yosys_show.*
4852 -color <color> <object>
4853 assign the specified color to the specified object. The object can be
4854 a single selection wildcard expressions or a saved set of objects in
4855 the @<name> syntax (see "help select" for details).
4857 -label <text> <object>
4858 assign the specified label text to the specified object. The object can
4859 be a single selection wildcard expressions or a saved set of objects in
4860 the @<name> syntax (see "help select" for details).
4863 Randomly assign colors to the wires. The integer argument is the seed
4864 for the random number generator. Change the seed value if the colored
4865 graph still is ambiguous. A seed of zero deactivates the coloring.
4867 -colorattr <attribute_name>
4868 Use the specified attribute to assign colors. A unique color is
4869 assigned to each unique value of this attribute.
4872 annotate buses with a label indicating the width of the bus.
4875 mark ports (A, B) that are declared as signed (using the [AB]_SIGNED
4876 cell parameter) with an asterisk next to the port name.
4879 stretch the graph so all inputs are on the left side and all outputs
4880 (including inout ports) are on the right side.
4883 wait for the user to press enter to before returning
4886 enumerate objects with internal ($-prefixed) names
4889 do not abbreviate objects with internal ($-prefixed) names
4892 do not add the module name as graph title to the dot file
4895 don't run viewer in the background, IE wait for the viewer tool to
4896 exit before returning
4898 When no <format> is specified, 'dot' is used. When no <format> and <viewer> is
4899 specified, 'xdot' is used to display the schematic (POSIX systems only).
4901 The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
4902 unless another prefix is specified using -prefix <prefix>.
4904 Yosys on Windows and YosysJS use different defaults: The output is written
4905 to 'show.dot' in the current directory and new viewer is launched each time
4906 the 'show' command is executed.
4909 \section{shregmap -- map shift registers}
4910 \label{cmd:shregmap}
4911 \begin{lstlisting}[numbers=left,frame=single]
4912 shregmap [options] [selection]
4914 This pass converts chains of $_DFF_[NP]_ gates to target specific shift register
4915 primitives. The generated shift register will be of type $__SHREG_DFF_[NP]_ and
4916 will use the same interface as the original $_DFF_*_ cells. The cell parameter
4917 'DEPTH' will contain the depth of the shift register. Use a target-specific
4918 'techmap' map file to convert those cells to the actual target cells.
4921 minimum length of shift register (default = 2)
4922 (this is the length after -keep_before and -keep_after)
4925 maximum length of shift register (default = no limit)
4926 larger chains will be mapped to multiple shift register instances
4929 number of DFFs to keep before the shift register (default = 0)
4932 number of DFFs to keep after the shift register (default = 0)
4935 limit match to only positive or negative edge clocks. (default = any)
4937 -enpol pos|neg|none|any_or_none|any
4938 limit match to FFs with the specified enable polarity. (default = none)
4940 -match <cell_type>[:<d_port_name>:<q_port_name>]
4941 match the specified cells instead of $_DFF_N_ and $_DFF_P_. If
4942 ':<d_port_name>:<q_port_name>' is omitted then 'D' and 'Q' is used
4943 by default. E.g. the option '-clkpol pos' is just an alias for
4944 '-match $_DFF_P_', which is an alias for '-match $_DFF_P_:D:Q'.
4947 instead of encoding the clock and enable polarity in the cell name by
4948 deriving from the original cell name, simply name all generated cells
4949 $__SHREG_ and use CLKPOL and ENPOL parameters. An ENPOL value of 2 is
4950 used to denote cells without enable input. The ENPOL parameter is
4951 omitted when '-enpol none' (or no -enpol option) is passed.
4954 assume the shift register is automatically zero-initialized, so it
4955 becomes legal to merge zero initialized FFs into the shift register.
4958 map initialized registers to the shift reg, add an INIT parameter to
4959 generated cells with the initialization value. (first bit to shift out
4963 map to greenpak4 shift registers.
4966 \section{sim -- simulate the circuit}
4968 \begin{lstlisting}[numbers=left,frame=single]
4969 sim [options] [top-level]
4971 This command simulates the circuit using the given top-level module.
4974 write the simulation results to the given VCD file
4977 write the simulation results to the given FST file
4980 write the simulation results to an AIGER witness file
4981 (requires a *.aim file via -map)
4984 ignore constant x outputs in simulation file.
4987 include date and full version info in output.
4990 name of top-level clock input
4993 name of top-level clock input (inverse polarity)
4996 mark that witness file is multiclock.
4999 name of top-level reset input (active high)
5002 name of top-level inverted reset input (active low)
5005 number of cycles reset should stay active (default: 1)
5008 zero-initialize all uninitialized regs and memories
5011 include the specified timescale declaration in the vcd
5014 number of clock cycles to simulate (default: 20)
5017 use all nets in VCD/FST operations, not just those with public names
5020 writeback mode: use final simulation state as new init state
5023 read simulation results file (file formats supported: FST, VCD, AIW and WIT)
5024 VCD support requires vcd2fst external tool to be present
5027 read file with port and latch symbols, needed for AIGER witness input
5030 scope of simulation top model
5033 sets start and stop time
5036 start co-simulation in arbitary time (default 0)
5039 stop co-simulation in arbitary time (default END)
5042 simulation with stimulus from FST (default)
5045 co-simulation expect exact match
5048 co-simulation, x in simulation can match any value in FST
5051 co-simulation, x in FST can match any value in simulation
5054 disable per-cycle/sample log message
5060 \section{simplemap -- mapping simple coarse-grain cells}
5061 \label{cmd:simplemap}
5062 \begin{lstlisting}[numbers=left,frame=single]
5063 simplemap [selection]
5065 This pass maps a small selection of simple coarse-grain cells to yosys gate
5066 primitives. The following internal cell types are mapped by this pass:
5068 $not, $pos, $and, $or, $xor, $xnor
5069 $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool
5070 $logic_not, $logic_and, $logic_or, $mux, $tribuf
5071 $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff, $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr
5074 \section{splice -- create explicit splicing cells}
5076 \begin{lstlisting}[numbers=left,frame=single]
5077 splice [options] [selection]
5079 This command adds $slice and $concat cells to the design to make the splicing
5080 of multi-bit signals explicit. This for example is useful for coarse grain
5081 synthesis, where dedicated hardware is needed to splice signals.
5084 only select the cell ports to rewire by the cell. if the selection
5085 contains a cell, than all cell inputs are rewired, if necessary.
5088 only select the cell ports to rewire by the wire. if the selection
5089 contains a wire, than all cell ports driven by this wire are wired,
5093 it is sufficient if the driver of any bit of a cell port is selected.
5094 by default all bits must be selected.
5097 also add $slice and $concat cells to drive otherwise unused wires.
5100 do not rewire selected module outputs.
5103 only rewire cell ports with the specified name. can be used multiple
5104 times. implies -no_output.
5107 do not rewire cell ports with the specified name. can be used multiple
5108 times. can not be combined with -port <name>.
5110 By default selected output wires and all cell ports of selected cells driven
5111 by selected wires are rewired.
5114 \section{splitnets -- split up multi-bit nets}
5115 \label{cmd:splitnets}
5116 \begin{lstlisting}[numbers=left,frame=single]
5117 splitnets [options] [selection]
5119 This command splits multi-bit nets into single-bit nets.
5121 -format char1[char2[char3]]
5122 the first char is inserted between the net name and the bit index, the
5123 second char is appended to the netname. e.g. -format () creates net
5124 names like 'mysignal(42)'. the 3rd character is the range separation
5125 character when creating multi-bit wires. the default is '[]:'.
5128 also split module ports. per default only internal signals are split.
5131 don't blindly split nets in individual bits. instead look at the driver
5132 and split nets so that no driver drives only part of a net.
5135 \section{sta -- perform static timing analysis}
5137 \begin{lstlisting}[numbers=left,frame=single]
5138 sta [options] [selection]
5140 This command performs static timing analysis on the design. (Only considers
5141 paths within a single module, so the design must be flattened.)
5144 \section{stat -- print some statistics}
5146 \begin{lstlisting}[numbers=left,frame=single]
5147 stat [options] [selection]
5149 Print some statistics (number of objects) on the selected portion of the
5153 print design hierarchy with this module as top. if the design is fully
5154 selected and a module has the 'top' attribute set, this module is used
5155 default value for this option.
5157 -liberty <liberty_file>
5158 use cell area information from the provided liberty file
5161 print area estemate for the specified technology. Currently supported
5162 values for <technology>: xilinx, cmos
5165 annotate internal cell types with their word width.
5166 e.g. $add_8 for an 8 bit wide $add cell.
5169 \section{submod -- moving part of a module to a new submodule}
5171 \begin{lstlisting}[numbers=left,frame=single]
5172 submod [options] [selection]
5174 This pass identifies all cells with the 'submod' attribute and moves them to
5175 a newly created module. The value of the attribute is used as name for the
5176 cell that replaces the group of cells with the same attribute value.
5178 This pass can be used to create a design hierarchy in flat design. This can
5179 be useful for analyzing or reverse-engineering a design.
5181 This pass only operates on completely selected modules with no processes
5185 by default the cells are 'moved' from the source module and the source
5186 module will use an instance of the new module after this command is
5187 finished. call with -copy to not modify the source module.
5190 don't use the 'submod' attribute but instead use the selection. only
5191 objects from one module might be selected. the value of the -name option
5192 is used as the value of the 'submod' attribute instead.
5195 instead of creating submodule ports with public names, create ports with
5196 private names so that a subsequent 'flatten; clean' call will restore the
5197 original module with original public names.
5200 \section{supercover -- add hi/lo cover cells for each wire bit}
5201 \label{cmd:supercover}
5202 \begin{lstlisting}[numbers=left,frame=single]
5203 supercover [options] [selection]
5205 This command adds two cover cells for each bit of each selected wire, one
5206 checking for a hi signal level and one checking for lo level.
5209 \section{synth -- generic synthesis script}
5211 \begin{lstlisting}[numbers=left,frame=single]
5214 This command runs the default synthesis script. This command does not operate
5215 on partly selected designs.
5218 use the specified module as top module (default='top')
5221 automatically determine the top of the design hierarchy
5224 flatten the design before synthesis. this will pass '-auto-top' to
5225 'hierarchy' if no top module is specified.
5228 passed to 'fsm_recode' via 'fsm'
5231 perform synthesis for a k-LUT architecture.
5234 do not run FSM optimization
5237 do not run abc (as if yosys was compiled without ABC support)
5240 do not run 'alumacc' pass. i.e. keep arithmetic operators in
5241 their direct form ($add, $sub, etc.).
5244 passed to 'memory'. prohibits merging of FFs into memory read ports
5247 do not run SAT-based resource sharing
5249 -run <from_label>[:<to_label>]
5250 only run the commands between the labels (see below). an empty
5251 from label is synonymous to 'begin', and empty to label is
5252 synonymous to the end of the command list.
5255 use new ABC9 flow (EXPERIMENTAL)
5258 use FlowMap LUT techmapping instead of ABC
5261 The following commands are executed by this synthesis command:
5264 hierarchy -check [-top <top> | -auto-top]
5268 flatten (if -flatten)
5278 techmap -map +/cmp2lut.v -map +/cmp2lcu.v (if -lut)
5279 alumacc (unless -noalumacc)
5280 share (unless -noshare)
5290 techmap -map +/gate2lut.v (if -noabc and -lut)
5291 clean; opt_lut (if -noabc and -lut)
5292 flowmap -maxlut K (if -flowmap and -lut)
5294 abc -fast (unless -noabc, unless -lut)
5295 abc -fast -lut k (unless -noabc, if -lut)
5296 opt -fast (unless -noabc)
5304 \section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.}
5305 \label{cmd:synth_achronix}
5306 \begin{lstlisting}[numbers=left,frame=single]
5307 synth_achronix [options]
5309 This command runs synthesis for Achronix Speedster eFPGAs. This work is still experimental.
5312 use the specified module as top module (default='top')
5315 write the design to the specified Verilog netlist file. writing of an
5316 output file is omitted if this parameter is not specified.
5318 -run <from_label>:<to_label>
5319 only run the commands between the labels (see below). an empty
5320 from label is synonymous to 'begin', and empty to label is
5321 synonymous to the end of the command list.
5324 do not flatten design before synthesis
5327 run 'abc' with '-dff -D 1' options
5330 The following commands are executed by this synthesis command:
5333 read_verilog -sv -lib +/achronix/speedster22i/cells_sim.v
5334 hierarchy -check -top <top>
5336 flatten: (unless -noflatten)
5346 opt -fast -mux_undef -undriven -fine -full
5350 techmap -map +/techmap.v
5353 setundef -undriven -zero
5354 dfflegalize -cell $_DFF_P_ x
5355 abc -markgroups -dff -D 1 (only if -retime)
5362 iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I
5363 techmap -map +/achronix/speedster22i/cells_map.v
5370 blackbox =A:whitebox
5373 write_verilog -nodec -attr2comment -defparam -renameprefix syn_ <file-name>
5376 \section{synth\_anlogic -- synthesis for Anlogic FPGAs}
5377 \label{cmd:synth_anlogic}
5378 \begin{lstlisting}[numbers=left,frame=single]
5379 synth_anlogic [options]
5381 This command runs synthesis for Anlogic FPGAs.
5384 use the specified module as top module
5387 write the design to the specified EDIF file. writing of an output file
5388 is omitted if this parameter is not specified.
5391 write the design to the specified JSON file. writing of an output file
5392 is omitted if this parameter is not specified.
5394 -run <from_label>:<to_label>
5395 only run the commands between the labels (see below). an empty
5396 from label is synonymous to 'begin', and empty to label is
5397 synonymous to the end of the command list.
5400 do not flatten design before synthesis
5403 run 'abc' with '-dff -D 1' options
5406 do not use EG_LOGIC_DRAM16X4 cells in output netlist
5409 do not use EG_PHY_BRAM or EG_PHY_BRAM32K cells in output netlist
5412 The following commands are executed by this synthesis command:
5415 read_verilog -lib +/anlogic/cells_sim.v +/anlogic/eagle_bb.v
5416 hierarchy -check -top <top>
5418 flatten: (unless -noflatten)
5427 map_bram: (skip if -nobram)
5428 memory_bram -rules +/anlogic/brams.txt
5429 techmap -map +/anlogic/brams_map.v
5430 setundef -zero -params t:EG_PHY_BRAM
5431 setundef -zero -params t:EG_PHY_BRAM32K
5433 map_lutram: (skip if -nolutram)
5434 memory_bram -rules +/anlogic/lutrams.txt
5435 techmap -map +/anlogic/lutrams_map.v
5436 setundef -zero -params t:EG_LOGIC_DRAM16X4
5439 opt -fast -mux_undef -undriven -fine
5444 techmap -map +/techmap.v -map +/anlogic/arith_map.v
5446 abc -dff -D 1 (only if -retime)
5449 dfflegalize -cell $_DFFE_P??P_ r -cell $_SDFFE_P??P_ r -cell $_DLATCH_N??_ r
5450 techmap -D NO_LUT -map +/anlogic/cells_map.v
5459 techmap -map +/anlogic/cells_map.v
5470 blackbox =A:whitebox
5473 write_edif <file-name>
5476 write_json <file-name>
5479 \section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs}
5480 \label{cmd:synth_coolrunner2}
5481 \begin{lstlisting}[numbers=left,frame=single]
5482 synth_coolrunner2 [options]
5484 This command runs synthesis for Coolrunner-II CPLDs. This work is experimental.
5485 It is intended to be used with https://github.com/azonenberg/openfpga as the
5489 use the specified module as top module (default='top')
5492 write the design to the specified JSON file. writing of an output file
5493 is omitted if this parameter is not specified.
5495 -run <from_label>:<to_label>
5496 only run the commands between the labels (see below). an empty
5497 from label is synonymous to 'begin', and empty to label is
5498 synonymous to the end of the command list.
5501 do not flatten design before synthesis
5504 run 'abc' with '-dff -D 1' options
5507 The following commands are executed by this synthesis command:
5510 read_verilog -lib +/coolrunner2/cells_sim.v
5511 hierarchy -check -top <top>
5513 flatten: (unless -noflatten)
5522 extract_counter -dir up -allow_arst no
5523 techmap -map +/coolrunner2/cells_counter_map.v
5526 techmap -map +/techmap.v -map +/coolrunner2/cells_latch.v
5528 dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib
5533 extract -map +/coolrunner2/tff_extract.v
5536 abc -sop -I 40 -P 56
5540 dfflibmap -liberty +/coolrunner2/xc2_dff.lib
5541 dffinit -ff FDCP Q INIT
5542 dffinit -ff FDCP_N Q INIT
5543 dffinit -ff FTCP Q INIT
5544 dffinit -ff FTCP_N Q INIT
5545 dffinit -ff LDCP Q INIT
5546 dffinit -ff LDCP_N Q INIT
5549 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
5550 attrmvcp -attr src -attr LOC t:IOBUFE n:*
5551 attrmvcp -attr src -attr LOC -driven t:IBUF n:*
5560 blackbox =A:whitebox
5563 write_json <file-name>
5566 \section{synth\_easic -- synthesis for eASIC platform}
5567 \label{cmd:synth_easic}
5568 \begin{lstlisting}[numbers=left,frame=single]
5569 synth_easic [options]
5571 This command runs synthesis for eASIC platform.
5574 use the specified module as top module
5577 write the design to the specified structural Verilog file. writing of
5578 an output file is omitted if this parameter is not specified.
5581 set path to the eTools installation. (default=/opt/eTools)
5583 -run <from_label>:<to_label>
5584 only run the commands between the labels (see below). an empty
5585 from label is synonymous to 'begin', and empty to label is
5586 synonymous to the end of the command list.
5589 do not flatten design before synthesis
5592 run 'abc' with '-dff -D 1' options
5595 The following commands are executed by this synthesis command:
5598 read_liberty -lib <etools_phys_clk_lib>
5599 read_liberty -lib <etools_logic_lut_lib>
5600 hierarchy -check -top <top>
5602 flatten: (unless -noflatten)
5610 opt -fast -mux_undef -undriven -fine
5615 abc -dff -D 1 (only if -retime)
5616 opt_clean (only if -retime)
5619 dfflibmap -liberty <etools_phys_clk_lib>
5620 abc -liberty <etools_logic_lut_lib>
5627 blackbox =A:whitebox
5630 write_verilog -noexpr -attr2comment <file-name>
5633 \section{synth\_ecp5 -- synthesis for ECP5 FPGAs}
5634 \label{cmd:synth_ecp5}
5635 \begin{lstlisting}[numbers=left,frame=single]
5636 synth_ecp5 [options]
5638 This command runs synthesis for ECP5 FPGAs.
5641 use the specified module as top module
5644 write the design to the specified BLIF file. writing of an output file
5645 is omitted if this parameter is not specified.
5648 write the design to the specified EDIF file. writing of an output file
5649 is omitted if this parameter is not specified.
5652 write the design to the specified JSON file. writing of an output file
5653 is omitted if this parameter is not specified.
5655 -run <from_label>:<to_label>
5656 only run the commands between the labels (see below). an empty
5657 from label is synonymous to 'begin', and empty to label is
5658 synonymous to the end of the command list.
5661 do not flatten design before synthesis
5664 run 'abc'/'abc9' with -dff option
5667 run 'abc' with '-dff -D 1' options
5670 do not use CCU2 cells in output netlist
5673 do not use flipflops with CE in output netlist
5676 do not use block RAM cells in output netlist
5679 do not use LUT RAM cells in output netlist
5682 do not use PFU muxes to implement LUTs larger than LUT4s
5685 use async PRLD mode to implement ALDFF (EXPERIMENTAL)
5688 run two passes of 'abc' for slightly improved logic density
5691 use new ABC9 flow (EXPERIMENTAL)
5694 generate an output netlist (and BLIF file) suitable for VPR
5695 (this feature is experimental and incomplete)
5698 do not map multipliers to MULT18X18D
5701 The following commands are executed by this synthesis command:
5704 read_verilog -lib -specify +/ecp5/cells_sim.v +/ecp5/cells_bb.v
5705 hierarchy -check -top <top>
5722 techmap -map +/cmp2lut.v -D LUT_WIDTH=4
5725 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)
5726 chtype -set $mul t:$__soft_mul (unless -nodsp)
5732 map_bram: (skip if -nobram)
5733 memory_bram -rules +/ecp5/brams.txt
5734 techmap -map +/ecp5/brams_map.v
5736 map_lutram: (skip if -nolutram)
5737 memory_bram -rules +/ecp5/lutrams.txt
5738 techmap -map +/ecp5/lutrams_map.v
5741 opt -fast -mux_undef -undriven -fine
5742 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
5746 techmap -map +/techmap.v -map +/ecp5/arith_map.v
5748 abc -dff -D 1 (only if -retime)
5752 dfflegalize -cell $_DFF_?_ 01 -cell $_DFF_?P?_ r -cell $_SDFF_?P?_ r [-cell $_DFFE_??_ 01 -cell $_DFFE_?P??_ r -cell $_SDFFE_?P??_ r] [-cell $_ALDFF_?P_ x -cell $_ALDFFE_?P?_ x] [-cell $_DLATCH_?_ x] ($_ALDFF_*_ only if -asyncprld, $_DLATCH_* only if not -asyncprld, $_*DFFE_* only if not -nodffe)
5753 zinit -all w:* t:$_DFF_?_ t:$_DFFE_??_ t:$_SDFF* (only if -abc9 and -dff)
5754 techmap -D NO_LUT -map +/ecp5/cells_map.v
5755 opt_expr -undriven -mux_undef
5758 attrmvcp -copy -attr syn_useioff
5763 techmap -map +/ecp5/latches_map.v (skip if -asyncprld)
5768 techmap -map +/ecp5/cells_map.v (skip if -vpr)
5769 opt_lut_ins -tech ecp5
5777 blackbox =A:whitebox
5780 opt_clean -purge (vpr mode)
5781 write_blif -attr -cname -conn -param <file-name> (vpr mode)
5782 write_blif -gates -attr -param <file-name> (non-vpr mode)
5785 write_edif <file-name>
5788 write_json <file-name>
5791 \section{synth\_efinix -- synthesis for Efinix FPGAs}
5792 \label{cmd:synth_efinix}
5793 \begin{lstlisting}[numbers=left,frame=single]
5794 synth_efinix [options]
5796 This command runs synthesis for Efinix FPGAs.
5799 use the specified module as top module
5802 write the design to the specified EDIF file. writing of an output file
5803 is omitted if this parameter is not specified.
5806 write the design to the specified JSON file. writing of an output file
5807 is omitted if this parameter is not specified.
5809 -run <from_label>:<to_label>
5810 only run the commands between the labels (see below). an empty
5811 from label is synonymous to 'begin', and empty to label is
5812 synonymous to the end of the command list.
5815 do not flatten design before synthesis
5818 run 'abc' with '-dff -D 1' options
5821 do not use EFX_RAM_5K cells in output netlist
5824 The following commands are executed by this synthesis command:
5827 read_verilog -lib +/efinix/cells_sim.v
5828 hierarchy -check -top <top>
5830 flatten: (unless -noflatten)
5838 memory_bram -rules +/efinix/brams.txt
5839 techmap -map +/efinix/brams_map.v
5840 setundef -zero -params t:EFX_RAM_5K
5843 opt -fast -mux_undef -undriven -fine
5848 techmap -map +/techmap.v -map +/efinix/arith_map.v
5850 abc -dff -D 1 (only if -retime)
5853 dfflegalize -cell $_DFFE_????_ 0 -cell $_SDFFE_????_ 0 -cell $_SDFFCE_????_ 0 -cell $_DLATCH_?_ x
5854 techmap -D NO_LUT -map +/efinix/cells_map.v
5863 techmap -map +/efinix/cells_map.v
5867 clkbufmap -buf $__EFX_GBUF O:I
5868 techmap -map +/efinix/gbuf_map.v
5876 blackbox =A:whitebox
5879 write_edif <file-name>
5882 write_json <file-name>
5885 \section{synth\_gatemate -- synthesis for Cologne Chip GateMate FPGAs}
5886 \label{cmd:synth_gatemate}
5887 \begin{lstlisting}[numbers=left,frame=single]
5888 synth_gatemate [options]
5890 This command runs synthesis for Cologne Chip AG GateMate FPGAs.
5893 use the specified module as top module.
5896 write the design to the specified verilog file. Writing of an output
5897 file is omitted if this parameter is not specified.
5900 write the design to the specified JSON file. Writing of an output file
5901 is omitted if this parameter is not specified.
5903 -run <from_label>:<to_label>
5904 only run the commands between the labels (see below). An empty
5905 from label is synonymous to 'begin', and empty to label is
5906 synonymous to the end of the command list.
5909 do not flatten design before synthesis.
5912 do not use CC_BRAM_20K or CC_BRAM_40K cells in output netlist.
5915 do not use CC_ADDF full adder cells in output netlist.
5918 do not use CC_MULT multiplier cells in output netlist.
5921 do not use CC_MX{8,4} multiplexer cells in output netlist.
5924 run 'abc' with -dff option
5927 run 'abc' with '-dff -D 1' options
5930 disable I/O buffer insertion (useful for hierarchical or
5931 out-of-context flows).
5934 disable automatic clock buffer insertion.
5936 The following commands are executed by this synthesis command:
5939 read_verilog -lib -specify +/gatemate/cells_sim.v +/gatemate/cells_bb.v
5940 hierarchy -check -top <top>
5958 techmap -map +/cmp2lut.v -D LUT_WIDTH=4
5962 map_mult: (skip if '-nomult')
5963 techmap -map +/gatemate/mul_map.v
5971 map_bram: (skip if '-nobram')
5972 memory_bram -rules +/gatemate/brams.txt
5973 setundef -zero -params t:$__CC_BRAM_CASCADE t:$__CC_BRAM_40K_SDP t:$__CC_BRAM_20K_SDP t:$__CC_BRAM_20K_TDP t:$__CC_BRAM_40K_TDP
5974 techmap -map +/gatemate/brams_map.v
5977 opt -fast -mux_undef -undriven -fine
5982 techmap -map +/techmap.v -map +/gatemate/arith_map.v
5985 map_io: (skip if '-noiopad')
5986 iopadmap -bits -inpad CC_IBUF Y:I -outpad CC_OBUF A:O -toutpad CC_TOBUF ~T:A:O -tinoutpad CC_IOBUF ~T:Y:A:IO
5991 dfflegalize -cell $_DFFE_????_ x -cell $_DLATCH_???_ x
5992 techmap -map +/gatemate/reg_map.v
5998 muxcover -mux4 -mux8
6000 techmap -map +/gatemate/mux_map.v
6007 techmap -map +/gatemate/lut_map.v
6010 map_bufg: (skip if '-noclkbuf')
6011 clkbufmap -buf CC_BUFG O:I
6018 blackbox =A:whitebox
6022 write_verilog -noattr <file-name>
6025 write_json <file-name>
6028 \section{synth\_gowin -- synthesis for Gowin FPGAs}
6029 \label{cmd:synth_gowin}
6030 \begin{lstlisting}[numbers=left,frame=single]
6031 synth_gowin [options]
6033 This command runs synthesis for Gowin FPGAs. This work is experimental.
6036 use the specified module as top module (default='top')
6039 write the design to the specified Verilog netlist file. writing of an
6040 output file is omitted if this parameter is not specified.
6043 write the design to the specified JSON netlist file. writing of an
6044 output file is omitted if this parameter is not specified.
6045 This disables features not yet supported by nexpnr-gowin.
6047 -run <from_label>:<to_label>
6048 only run the commands between the labels (see below). an empty
6049 from label is synonymous to 'begin', and empty to label is
6050 synonymous to the end of the command list.
6053 do not use flipflops with CE in output netlist
6056 do not use BRAM cells in output netlist
6059 do not use distributed RAM cells in output netlist
6062 do not flatten design before synthesis
6065 run 'abc' with '-dff -D 1' options
6068 do not use muxes to implement LUTs larger than LUT4s
6071 do not emit IOB at top level ports
6074 do not use ALU cells
6077 use new ABC9 flow (EXPERIMENTAL)
6080 The following commands are executed by this synthesis command:
6083 read_verilog -specify -lib +/gowin/cells_sim.v
6084 hierarchy -check -top <top>
6086 flatten: (unless -noflatten)
6095 map_bram: (skip if -nobram)
6096 memory_bram -rules +/gowin/brams.txt
6097 techmap -map +/gowin/brams_map.v
6099 map_lutram: (skip if -nolutram)
6100 memory_bram -rules +/gowin/lutrams.txt
6101 techmap -map +/gowin/lutrams_map.v
6102 setundef -params -zero t:RAM16S4
6105 opt -fast -mux_undef -undriven -fine
6110 techmap -map +/techmap.v -map +/gowin/arith_map.v
6112 abc -dff -D 1 (only if -retime)
6113 iopadmap -bits -inpad IBUF O:I -outpad OBUF I:O -toutpad TBUF ~OEN:I:O -tinoutpad IOBUF ~OEN:O:I:IO (unless -noiopads)
6117 dfflegalize -cell $_DFF_?_ 0 -cell $_DFFE_?P_ 0 -cell $_SDFF_?P?_ r -cell $_SDFFE_?P?P_ r -cell $_DFF_?P?_ r -cell $_DFFE_?P?P_ r
6118 techmap -map +/gowin/cells_map.v
6127 techmap -map +/gowin/cells_map.v
6128 opt_lut_ins -tech gowin
6129 setundef -undriven -params -zero
6130 hilomap -singleton -hicell VCC V -locell GND G
6131 splitnets -ports (only if -vout used)
6139 blackbox =A:whitebox
6142 write_verilog -simple-lhs -decimal -attr2comment -defparam -renameprefix gen <file-name>
6143 write_json <file-name>
6146 \section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs}
6147 \label{cmd:synth_greenpak4}
6148 \begin{lstlisting}[numbers=left,frame=single]
6149 synth_greenpak4 [options]
6151 This command runs synthesis for GreenPAK4 FPGAs. This work is experimental.
6152 It is intended to be used with https://github.com/azonenberg/openfpga as the
6156 use the specified module as top module (default='top')
6159 synthesize for the specified part. Valid values are SLG46140V,
6160 SLG46620V, and SLG46621V (default).
6163 write the design to the specified JSON file. writing of an output file
6164 is omitted if this parameter is not specified.
6166 -run <from_label>:<to_label>
6167 only run the commands between the labels (see below). an empty
6168 from label is synonymous to 'begin', and empty to label is
6169 synonymous to the end of the command list.
6172 do not flatten design before synthesis
6175 run 'abc' with '-dff -D 1' options
6178 The following commands are executed by this synthesis command:
6181 read_verilog -lib +/greenpak4/cells_sim.v
6182 hierarchy -check -top <top>
6184 flatten: (unless -noflatten)
6193 extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14
6195 opt -fast -mux_undef -undriven -fine
6198 techmap -map +/techmap.v -map +/greenpak4/cells_latch.v
6199 dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib
6200 opt -fast -noclkinv -noff
6201 abc -dff -D 1 (only if -retime)
6204 nlutmap -assert -luts 0,6,8,2 (for -part SLG46140V)
6205 nlutmap -assert -luts 2,8,16,2 (for -part SLG46620V)
6206 nlutmap -assert -luts 2,8,16,2 (for -part SLG46621V)
6210 shregmap -tech greenpak4
6211 dfflibmap -liberty +/greenpak4/gp_dff.lib
6212 dffinit -ff GP_DFF Q INIT
6213 dffinit -ff GP_DFFR Q INIT
6214 dffinit -ff GP_DFFS Q INIT
6215 dffinit -ff GP_DFFSR Q INIT
6216 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
6217 attrmvcp -attr src -attr LOC t:GP_OBUF t:GP_OBUFT t:GP_IOBUF n:*
6218 attrmvcp -attr src -attr LOC -driven t:GP_IBUF n:*
6219 techmap -map +/greenpak4/cells_map.v
6227 blackbox =A:whitebox
6230 write_json <file-name>
6233 \section{synth\_ice40 -- synthesis for iCE40 FPGAs}
6234 \label{cmd:synth_ice40}
6235 \begin{lstlisting}[numbers=left,frame=single]
6236 synth_ice40 [options]
6238 This command runs synthesis for iCE40 FPGAs.
6240 -device < hx | lp | u >
6241 relevant only for '-abc9' flow, optimise timing for the specified device.
6245 use the specified module as top module
6248 write the design to the specified BLIF file. writing of an output file
6249 is omitted if this parameter is not specified.
6252 write the design to the specified EDIF file. writing of an output file
6253 is omitted if this parameter is not specified.
6256 write the design to the specified JSON file. writing of an output file
6257 is omitted if this parameter is not specified.
6259 -run <from_label>:<to_label>
6260 only run the commands between the labels (see below). an empty
6261 from label is synonymous to 'begin', and empty to label is
6262 synonymous to the end of the command list.
6265 do not flatten design before synthesis
6268 run 'abc'/'abc9' with -dff option
6271 run 'abc' with '-dff -D 1' options
6274 do not use SB_CARRY cells in output netlist
6277 do not use SB_DFFE* cells in output netlist
6279 -dffe_min_ce_use <min_ce_use>
6280 do not use SB_DFFE* cells if the resulting CE line would go to less
6281 than min_ce_use SB_DFFE* in output netlist
6284 do not use SB_RAM40_4K* cells in output netlist
6287 use iCE40 UltraPlus DSP cells for large arithmetic
6290 use built-in Yosys LUT techmapping instead of abc
6293 run two passes of 'abc' for slightly improved logic density
6296 generate an output netlist (and BLIF file) suitable for VPR
6297 (this feature is experimental and incomplete)
6300 use new ABC9 flow (EXPERIMENTAL)
6303 use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)
6306 The following commands are executed by this synthesis command:
6309 read_verilog -D ICE40_HX -lib -specify +/ice40/cells_sim.v
6310 hierarchy -check -top <top>
6313 flatten: (unless -noflatten)
6329 techmap -map +/cmp2lut.v -D LUT_WIDTH=4
6334 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)
6335 select a:mul2dsp (if -dsp)
6336 setattr -unset mul2dsp (if -dsp)
6337 opt_expr -fine (if -dsp)
6339 select -clear (if -dsp)
6341 chtype -set $mul t:$__soft_mul (if -dsp)
6347 map_bram: (skip if -nobram)
6348 memory_bram -rules +/ice40/brams.txt
6349 techmap -map +/ice40/brams_map.v
6353 opt -fast -mux_undef -undriven -fine
6354 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
6359 techmap -map +/techmap.v -map +/ice40/arith_map.v
6361 abc -dff -D 1 (only if -retime)
6365 dfflegalize -cell $_DFF_?_ 0 -cell $_DFFE_?P_ 0 -cell $_DFF_?P?_ 0 -cell $_DFFE_?P?P_ 0 -cell $_SDFF_?P?_ 0 -cell $_SDFFCE_?P?P_ 0 -cell $_DLATCH_?_ x -mince -1
6366 techmap -map +/ice40/ff_map.v
6373 ice40_opt (only if -abc2)
6374 techmap -map +/ice40/latches_map.v
6375 simplemap (if -noabc or -flowmap)
6376 techmap -map +/gate2lut.v -D LUT_WIDTH=4 (only if -noabc)
6377 flowmap -maxlut 4 (only if -flowmap)
6378 abc -dress -lut 4 (skip if -noabc)
6379 ice40_wrapcarry -unwrap
6380 techmap -map +/ice40/ff_map.v
6382 opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3 -dlogic SB_CARRY:CO=3
6385 techmap -map +/ice40/cells_map.v (skip if -vpr)
6393 blackbox =A:whitebox
6396 opt_clean -purge (vpr mode)
6397 write_blif -attr -cname -conn -param <file-name> (vpr mode)
6398 write_blif -gates -attr -param <file-name> (non-vpr mode)
6401 write_edif <file-name>
6404 write_json <file-name>
6407 \section{synth\_intel -- synthesis for Intel (Altera) FPGAs.}
6408 \label{cmd:synth_intel}
6409 \begin{lstlisting}[numbers=left,frame=single]
6410 synth_intel [options]
6412 This command runs synthesis for Intel FPGAs.
6414 -family <max10 | cyclone10lp | cycloneiv | cycloneive>
6415 generate the synthesis netlist for the specified family.
6416 MAX10 is the default target if no family argument specified.
6417 For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use cycloneive.
6418 For Cyclone V and Cyclone 10 GX, use the synth_intel_alm backend instead.
6421 use the specified module as top module (default='top')
6424 write the design to the specified Verilog Quartus Mapping File. Writing of an
6425 output file is omitted if this parameter is not specified.
6426 Note that this backend has not been tested and is likely incompatible
6427 with recent versions of Quartus.
6430 write BLIF files for VPR flow experiments. The synthesized BLIF output file is not
6431 compatible with the Quartus flow. Writing of an
6432 output file is omitted if this parameter is not specified.
6434 -run <from_label>:<to_label>
6435 only run the commands between the labels (see below). an empty
6436 from label is synonymous to 'begin', and empty to label is
6437 synonymous to the end of the command list.
6440 use IO pad cells in output netlist
6443 do not use block RAM cells in output netlist
6446 do not flatten design before synthesis
6449 run 'abc' with '-dff -D 1' options
6451 The following commands are executed by this synthesis command:
6456 read_verilog -sv -lib +/intel/max10/cells_sim.v
6457 read_verilog -sv -lib +/intel/common/m9k_bb.v
6458 read_verilog -sv -lib +/intel/common/altpll_bb.v
6459 hierarchy -check -top <top>
6461 flatten: (unless -noflatten)
6470 map_bram: (skip if -nobram)
6471 memory_bram -rules +/intel/common/brams_m9k.txt (if applicable for family)
6472 techmap -map +/intel/common/brams_map_m9k.v (if applicable for family)
6475 opt -fast -mux_undef -undriven -fine -full
6478 techmap -map +/techmap.v
6481 setundef -undriven -zero
6482 abc -markgroups -dff -D 1 (only if -retime)
6485 dfflegalize -cell $_DFFE_PN0P_ 01
6486 techmap -map +/intel/common/ff_map.v
6493 iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I (if -iopads)
6494 techmap -map +/intel/max10/cells_map.v
6501 blackbox =A:whitebox
6504 write_verilog -attr2comment -defparam -nohex -decimal -renameprefix syn_ <file-name>
6508 write_blif <file-name>
6511 WARNING: THE 'synth_intel' COMMAND IS EXPERIMENTAL.
6514 \section{synth\_intel\_alm -- synthesis for ALM-based Intel (Altera) FPGAs.}
6515 \label{cmd:synth_intel_alm}
6516 \begin{lstlisting}[numbers=left,frame=single]
6517 synth_intel_alm [options]
6519 This command runs synthesis for ALM-based Intel FPGAs.
6522 use the specified module as top module
6526 "cyclonev" - Cyclone V (default)
6527 "arriav" - Arria V (non-GZ) "cyclone10gx" - Cyclone 10GX
6530 write the design to the specified Verilog Quartus Mapping File. Writing of an
6531 output file is omitted if this parameter is not specified. Implies -quartus.
6534 do not flatten design before synthesis; useful for per-module area statistics
6537 output a netlist using Quartus cells instead of MISTRAL_* cells
6540 pass DFFs to ABC to perform sequential logic optimisations (EXPERIMENTAL)
6542 -run <from_label>:<to_label>
6543 only run the commands between the labels (see below). an empty
6544 from label is synonymous to 'begin', and empty to label is
6545 synonymous to the end of the command list.
6548 do not use LUT RAM cells in output netlist
6551 do not use block RAM cells in output netlist
6554 do not map multipliers to MISTRAL_MUL cells
6557 do not instantiate IO buffers
6560 do not insert global clock buffers
6562 The following commands are executed by this synthesis command:
6565 read_verilog -specify -lib -D <family> +/intel_alm/common/alm_sim.v
6566 read_verilog -specify -lib -D <family> +/intel_alm/common/dff_sim.v
6567 read_verilog -specify -lib -D <family> +/intel_alm/common/dsp_sim.v
6568 read_verilog -specify -lib -D <family> +/intel_alm/common/mem_sim.v
6569 read_verilog -specify -lib -D <family> +/intel_alm/common/misc_sim.v
6570 read_verilog -specify -lib -D <family> -icells +/intel_alm/common/abc9_model.v
6571 read_verilog -lib +/intel/common/altpll_bb.v
6572 read_verilog -lib +/intel_alm/common/megafunction_bb.v
6573 hierarchy -check -top <top>
6577 flatten (skip if -noflatten)
6590 techmap -map +/cmp2lut.v -D LUT_WIDTH=6
6593 techmap -map +/mul2dsp.v [...] (unless -nodsp)
6595 iopadmap -bits -outpad MISTRAL_OB I:PAD -inpad MISTRAL_IB O:PAD -toutpad MISTRAL_IO OE:O:PAD -tinoutpad MISTRAL_IO OE:O:I:PAD A:top (unless -noiopad)
6596 techmap -map +/intel_alm/common/arith_alm_map.v -map +/intel_alm/common/dsp_map.v
6601 map_bram: (skip if -nobram)
6602 memory_bram -rules +/intel_alm/common/bram_<bram_type>.txt
6603 techmap -map +/intel_alm/common/bram_<bram_type>_map.v
6605 map_lutram: (skip if -nolutram)
6606 memory_bram -rules +/intel_alm/common/lutram_mlab.txt (for Cyclone V / Cyclone 10GX)
6614 dfflegalize -cell $_DFFE_PN0P_ 0 -cell $_SDFFCE_PP0P_ 0
6615 techmap -map +/intel_alm/common/dff_map.v
6616 opt -full -undriven -mux_undef
6618 clkbufmap -buf MISTRAL_CLKBUF Q:A (unless -noclkbuf)
6621 techmap -map +/intel_alm/common/abc9_map.v
6622 abc9 [-dff] -maxlut 6 -W 600
6623 techmap -map +/intel_alm/common/abc9_unmap.v
6624 techmap -map +/intel_alm/common/alm_map.v
6633 blackbox =A:whitebox
6636 rename -hide w:*[* w:*]*
6638 hilomap -singleton -hicell __MISTRAL_VCC Q -locell __MISTRAL_GND Q
6639 techmap -D <family> -map +/intel_alm/common/quartus_rename.v
6642 write_verilog -attr2comment -defparam -nohex -decimal <file-name>
6645 \section{synth\_machxo2 -- synthesis for MachXO2 FPGAs. This work is experimental.}
6646 \label{cmd:synth_machxo2}
6647 \begin{lstlisting}[numbers=left,frame=single]
6648 synth_machxo2 [options]
6650 This command runs synthesis for MachXO2 FPGAs.
6653 use the specified module as top module
6656 write the design to the specified BLIF file. writing of an output file
6657 is omitted if this parameter is not specified.
6660 write the design to the specified EDIF file. writing of an output file
6661 is omitted if this parameter is not specified.
6664 write the design to the specified JSON file. writing of an output file
6665 is omitted if this parameter is not specified.
6667 -run <from_label>:<to_label>
6668 only run the commands between the labels (see below). an empty
6669 from label is synonymous to 'begin', and empty to label is
6670 synonymous to the end of the command list.
6673 do not flatten design before synthesis
6676 do not insert IO buffers
6679 generate an output netlist (and BLIF file) suitable for VPR
6680 (this feature is experimental and incomplete)
6683 The following commands are executed by this synthesis command:
6686 read_verilog -lib -icells +/machxo2/cells_sim.v
6687 hierarchy -check -top <top>
6689 flatten: (unless -noflatten)
6701 techmap -map +/techmap.v
6704 map_ios: (unless -noiopad)
6705 iopadmap -bits -outpad $__FACADE_OUTPAD I:O -inpad $__FACADE_INPAD O:I -toutpad $__FACADE_TOUTPAD ~T:I:O -tinoutpad $__FACADE_TINOUTPAD ~T:O:I:B A:top
6706 attrmvcp -attr src -attr LOC t:$__FACADE_OUTPAD %x:+[O] t:$__FACADE_TOUTPAD %x:+[O] t:$__FACADE_TINOUTPAD %x:+[B]
6707 attrmvcp -attr src -attr LOC -driven t:$__FACADE_INPAD %x:+[I]
6710 dfflegalize -cell $_DFF_P_ 0
6717 techmap -map +/machxo2/cells_map.v
6723 blackbox =A:whitebox
6726 opt_clean -purge (vpr mode)
6727 write_blif -attr -cname -conn -param <file-name> (vpr mode)
6728 write_blif -gates -attr -param <file-name> (non-vpr mode)
6731 write_edif <file-name>
6734 write_json <file-name>
6737 \section{synth\_nexus -- synthesis for Lattice Nexus FPGAs}
6738 \label{cmd:synth_nexus}
6739 \begin{lstlisting}[numbers=left,frame=single]
6740 synth_nexus [options]
6742 This command runs synthesis for Lattice Nexus FPGAs.
6745 use the specified module as top module
6748 run synthesis for the specified Nexus device
6749 supported values: lifcl, lfd2nx
6752 write the design to the specified JSON file. writing of an output file
6753 is omitted if this parameter is not specified.
6756 write the design to the specified structural Verilog file. writing of
6757 an output file is omitted if this parameter is not specified.
6759 -run <from_label>:<to_label>
6760 only run the commands between the labels (see below). an empty
6761 from label is synonymous to 'begin', and empty to label is
6762 synonymous to the end of the command list.
6765 do not flatten design before synthesis
6768 run 'abc'/'abc9' with -dff option
6771 run 'abc' with '-dff -D 1' options
6774 do not use CCU2 cells in output netlist
6777 do not use flipflops with CE in output netlist
6780 do not use large RAM cells in output netlist
6781 note that large RAM must be explicitly requested with a (* lram *)
6782 attribute on the memory.
6785 do not use block RAM cells in output netlist
6788 do not use LUT RAM cells in output netlist
6791 do not use PFU muxes to implement LUTs larger than LUT4s
6794 do not insert IO buffers
6797 do not infer DSP multipliers
6800 use new ABC9 flow (EXPERIMENTAL)
6802 The following commands are executed by this synthesis command:
6805 read_verilog -lib -specify +/nexus/cells_sim.v +/nexus/cells_xtra.v
6806 hierarchy -check -top <top>
6823 techmap -map +/cmp2lut.v -D LUT_WIDTH=
4
6826 techmap -map +/mul2dsp.v
[...
] (unless -nodsp)
6827 techmap -map +/nexus/dsp_map.v (unless -nodsp)
6833 map_lram: (skip if -nolram)
6834 memory_bram -rules +/nexus/lrams.txt
6835 setundef -zero -params t:$__NX_PDPSC512K
6836 techmap -map +/nexus/lrams_map.v
6838 map_bram: (skip if -nobram)
6839 memory_bram -rules +/nexus/brams.txt
6840 setundef -zero -params t:$__NX_PDP16K
6841 techmap -map +/nexus/brams_map.v
6843 map_lutram: (skip if -nolutram)
6844 memory_bram -rules +/nexus/lutrams.txt
6845 setundef -zero -params t:$__NEXUS_DPR16X4
6846 techmap -map +/nexus/lutrams_map.v
6849 opt -fast -mux_undef -undriven -fine
6850 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
6854 techmap -map +/techmap.v -map +/nexus/arith_map.v
6855 iopadmap -bits -outpad OB I:O -inpad IB O:I -toutpad OBZ ~T:I:O -tinoutpad BB ~T:O:I:B A:top (skip if '-noiopad')
6857 abc -dff -D
1 (only if -retime)
6861 dfflegalize -cell $_DFF_P_
01 -cell $_DFF_PP?_ r -cell $_SDFF_PP?_ r -cell $_DLATCH_?_ x
[-cell $_DFFE_PP_
01 -cell $_DFFE_PP?P_ r -cell $_SDFFE_PP?P_ r
] ($_*DFFE_* only if not -nodffe)
6862 zinit -all w:* t:$_DFF_?_ t:$_DFFE_??_ t:$_SDFF* (only if -abc9 and -dff
6863 techmap -D NO_LUT -map +/nexus/cells_map.v
6864 opt_expr -undriven -mux_undef
6866 attrmvcp -copy -attr syn_useioff
6870 techmap -map +/nexus/latches_map.v
6875 techmap -map +/nexus/cells_map.v
6877 hilomap -singleton -hicell VHI Z -locell VLO Z
6885 blackbox =A:whitebox
6888 write_json <file-name>
6891 write_verilog <file-name>
6894 \section{synth
\_quicklogic -- Synthesis for QuickLogic FPGAs
}
6895 \label{cmd:synth_quicklogic
}
6896 \begin{lstlisting
}[numbers=left,frame=single
]
6897 synth_quicklogic
[options
]
6898 This command runs synthesis for QuickLogic FPGAs
6901 use the specified module as top module
6904 run synthesis for the specified QuickLogic architecture
6905 generate the synthesis netlist for the specified family.
6910 write the design to the specified BLIF file. writing of an output file
6911 is omitted if this parameter is not specified.
6914 write the design to the specified verilog file. writing of an output file
6915 is omitted if this parameter is not specified.
6918 use old ABC flow, which has generally worse mapping results but is less
6919 likely to have bugs.
6921 The following commands are executed by this synthesis command:
6924 read_verilog -lib -specify +/quicklogic/cells_sim.v +/quicklogic/pp3_cells_sim.v
6925 read_verilog -lib -specify +/quicklogic/lut_sim.v
6926 hierarchy -check -top <top>
6943 techmap -map +/cmp2lut.v -D LUT_WIDTH=
4
6953 opt -fast -mux_undef -undriven -fine
6954 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
6960 muxcover -mux8 -mux4
6964 dfflegalize -cell $_DFFSRE_PPPP_
0 -cell $_DLATCH_?_ x
6965 techmap -map +/quicklogic/pp3_cells_map.v -map +/quicklogic/pp3_ffs_map.v
6969 techmap -map +/quicklogic/pp3_latches_map.v
6970 read_verilog -lib -specify -icells +/quicklogic/abc9_model.v
6971 techmap -map +/quicklogic/abc9_map.v
6973 techmap -map +/quicklogic/abc9_unmap.v
6977 techmap -map +/quicklogic/pp3_lut_map.v
6987 clkbufmap -inpad ckpad Q:P
6988 iopadmap -bits -outpad outpad A:P -inpad inpad Q:P -tinoutpad bipad EN:Q:A:P A:top
6991 setundef -zero -params -undriven
6992 hilomap -hicell logic_1 A -locell logic_0 A -singleton A:top
6995 blackbox =A:whitebox
6998 write_blif -attr -param -auto-top
7001 write_verilog -noattr -nohex <file-name>
7004 \section{synth
\_sf2 -- synthesis for SmartFusion2 and IGLOO2 FPGAs
}
7005 \label{cmd:synth_sf2
}
7006 \begin{lstlisting
}[numbers=left,frame=single
]
7009 This command runs synthesis for SmartFusion2 and IGLOO2 FPGAs.
7012 use the specified module as top module
7015 write the design to the specified EDIF file. writing of an output file
7016 is omitted if this parameter is not specified.
7019 write the design to the specified Verilog file. writing of an output file
7020 is omitted if this parameter is not specified.
7023 write the design to the specified JSON file. writing of an output file
7024 is omitted if this parameter is not specified.
7026 -run <from_label>:<to_label>
7027 only run the commands between the labels (see below). an empty
7028 from label is synonymous to 'begin', and empty to label is
7029 synonymous to the end of the command list.
7032 do not flatten design before synthesis
7035 run synthesis in "block mode", i.e. do not insert IO buffers
7038 insert direct PAD->global_net buffers
7041 run 'abc' with '-dff -D
1' options
7044 The following commands are executed by this synthesis command:
7047 read_verilog -lib +/sf2/cells_sim.v
7048 hierarchy -check -top <top>
7050 flatten: (unless -noflatten)
7060 opt -fast -mux_undef -undriven -fine
7063 techmap -map +/techmap.v -map +/sf2/arith_map.v
7065 abc -dff -D
1 (only if -retime)
7068 dfflegalize -cell $_DFFE_PN?P_ x -cell $_SDFFCE_PN?P_ x -cell $_DLATCH_PN?_ x
7069 techmap -D NO_LUT -map +/sf2/cells_map.v
7078 techmap -map +/sf2/cells_map.v
7082 clkbufmap -buf CLKINT Y:A
[-inpad CLKBUF Y:PAD
] (unless -noiobs, -inpad only passed if -clkbuf)
7083 iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD (unless -noiobs
7090 blackbox =A:whitebox
7093 write_edif -gndvccy <file-name>
7096 write_verilog <file-name>
7099 write_json <file-name>
7102 \section{synth
\_xilinx -- synthesis for Xilinx FPGAs
}
7103 \label{cmd:synth_xilinx
}
7104 \begin{lstlisting
}[numbers=left,frame=single
]
7105 synth_xilinx
[options
]
7107 This command runs synthesis for Xilinx FPGAs. This command does not operate on
7108 partly selected designs. At the moment this command creates netlists that are
7109 compatible with
7-Series Xilinx devices.
7112 use the specified module as top module
7115 run synthesis for the specified Xilinx architecture
7116 generate the synthesis netlist for the specified family.
7118 - xcup: Ultrascale Plus
7120 - xc7: Series
7 (default)
7123 - xc5v: Virtex
5 (EXPERIMENTAL)
7124 - xc4v: Virtex
4 (EXPERIMENTAL)
7125 - xc3sda: Spartan
3A DSP (EXPERIMENTAL)
7126 - xc3sa: Spartan
3A (EXPERIMENTAL)
7127 - xc3se: Spartan
3E (EXPERIMENTAL)
7128 - xc3s: Spartan
3 (EXPERIMENTAL)
7129 - xc2vp: Virtex
2 Pro (EXPERIMENTAL)
7130 - xc2v: Virtex
2 (EXPERIMENTAL)
7131 - xcve: Virtex E, Spartan
2E (EXPERIMENTAL)
7132 - xcv: Virtex, Spartan
2 (EXPERIMENTAL)
7135 write the design to the specified edif file. writing of an output file
7136 is omitted if this parameter is not specified.
7139 write the design to the specified BLIF file. writing of an output file
7140 is omitted if this parameter is not specified.
7143 generate an output netlist suitable for ISE
7146 do not use block RAM cells in output netlist
7149 do not use distributed RAM cells in output netlist
7152 do not use distributed SRL cells in output netlist
7155 do not use XORCY/MUXCY/CARRY4 cells in output netlist
7158 do not use MUXF
[5-
9] resources to implement LUTs larger than native for the target
7161 do not use DSP48*s to implement multipliers and associated logic
7164 disable I/O buffer insertion (useful for hierarchical or
7165 out-of-context flows)
7168 disable automatic clock buffer insertion
7171 infer URAM288s for large memories (xcup only)
7174 enable inference of hard multiplexer resources (MUXF
[78]) for muxes at or
7175 above this number of inputs (minimum value
2, recommended value >=
5).
7176 default:
0 (no inference)
7178 -run <from_label>:<to_label>
7179 only run the commands between the labels (see below). an empty
7180 from label is synonymous to 'begin', and empty to label is
7181 synonymous to the end of the command list.
7184 flatten design before synthesis
7187 run 'abc'/'abc9' with -dff option
7190 run 'abc' with '-D
1' option to enable flip-flop retiming.
7194 use new ABC9 flow (EXPERIMENTAL)
7197 The following commands are executed by this synthesis command:
7200 read_verilog -lib -specify +/xilinx/cells_sim.v
7201 read_verilog -lib +/xilinx/cells_xtra.v
7202 hierarchy -check -auto-top
7206 flatten (with '-flatten')
7215 wreduce
[-keepdc
] (option for '-widemux')
7218 muxpack ('-widemux' only)
7219 pmux2shiftx (skip if '-nosrl' and '-widemux=
0')
7220 clean (skip if '-nosrl' and '-widemux=
0')
7222 map_dsp: (skip if '-nodsp')
7224 techmap -map +/mul2dsp.v -map +/xilinx/
{family
}_dsp_map.v
{options
}
7226 setattr -unset mul2dsp
7230 xilinx_dsp -family <family>
7231 chtype -set $mul t:$__soft_mul
7234 techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=
[46]
7241 map_uram: (only if '-uram')
7242 memory_bram -rules +/xilinx/
{family
}_urams.txt
7243 techmap -map +/xilinx/
{family
}_urams_map.v
7245 map_bram: (skip if '-nobram')
7246 memory_bram -rules +/xilinx/
{family
}_brams.txt
7247 techmap -map +/xilinx/
{family
}_brams_map.v
7249 map_lutram: (skip if '-nolutram')
7250 memory_bram -rules +/xilinx/lut
[46]_lutrams.txt
7251 techmap -map +/xilinx/lutrams_map.v
7258 simplemap t:$mux ('-widemux' only)
7259 muxcover <internal options> ('-widemux' only)
7261 xilinx_srl -variable -minlen
3 (skip if '-nosrl')
7262 techmap -map +/techmap.v -D LUT_SIZE=
[46] [-map +/xilinx/mux_map.v
] -map +/xilinx/arith_map.v
7266 iopadmap -bits -outpad OBUF I:O -inpad IBUF O:I -toutpad OBUFT ~T:I:O -tinoutpad IOBUF ~T:O:I:IO A:top (skip if '-noiopad')
7267 techmap -map +/techmap.v -map +/xilinx/cells_map.v
7271 dfflegalize -cell $_DFFE_?P?P_
01 -cell $_SDFFE_?P?P_
01 -cell $_DLATCH_?P?_
01 (for xc6v, xc7, xcu, xcup)
7272 zinit -all w:* t:$_SDFFE_* ('-dff' only)
7273 techmap -map +/xilinx/ff_map.v ('-abc9' only)
7276 opt_expr -mux_undef -noclkinv
7277 abc -luts
2:
2,
3,
6:
5[,
10,
20] [-dff
] [-D
1] (option for '-nowidelut', '-dff', '-retime')
7279 techmap -map +/xilinx/ff_map.v (only if not '-abc9')
7280 xilinx_srl -fixed -minlen
3 (skip if '-nosrl')
7281 techmap -map +/xilinx/lut_map.v -map +/xilinx/cells_map.v -D LUT_WIDTH=
[46]
7282 xilinx_dffopt
[-lut4
]
7283 opt_lut_ins -tech xilinx
7286 clkbufmap -buf BUFG O:I (skip if '-noclkbuf')
7287 extractinv -inv INV O:I (only if '-ise')
7294 blackbox =A:whitebox
7297 write_edif -pvector bra
7303 \section{tcl -- execute a TCL script file
}
7305 \begin{lstlisting
}[numbers=left,frame=single
]
7306 tcl <filename>
[args
]
7308 This command executes the tcl commands in the specified file.
7309 Use 'yosys cmd' to run the yosys command 'cmd' from tcl.
7311 The tcl command 'yosys -import' can be used to import all yosys
7312 commands directly as tcl commands to the tcl shell. Yosys commands
7313 'proc' and 'rename' are wrapped to tcl commands 'procs' and 'renames'
7314 in order to avoid a name collision with the built in commands.
7316 If any arguments are specified, these arguments are provided to the script via
7317 the standard $argc and $argv variables.
7320 \section{techmap -- generic technology mapper
}
7322 \begin{lstlisting
}[numbers=left,frame=single
]
7323 techmap
[-map filename
] [selection
]
7325 This pass implements a very simple technology mapper that replaces cells in
7326 the design with implementations given in form of a Verilog or RTLIL source
7330 the library of cell implementations to be used.
7331 without this parameter a builtin library is used that
7332 transforms the internal RTL cells to the internal gate
7336 like -map above, but with an in-memory design instead of a file.
7339 load the cell implementations as separate modules into the design
7340 instead of inlining them.
7343 only run the specified number of iterations on each module.
7347 instead of the iterative breadth-first algorithm use a recursive
7348 depth-first algorithm. both methods should yield equivalent results,
7349 but may differ in performance.
7352 Automatically call "proc" on implementations that contain processes.
7355 Ignore the 'whitebox' attribute on cell implementations.
7358 this option will cause techmap to exit with an error if it can't map
7359 a selected cell. only cell types that end on an underscore are accepted
7360 as final cell types by this mode.
7362 -D <define>, -I <incdir>
7363 this options are passed as-is to the Verilog frontend for loading the
7364 map file. Note that the Verilog frontend is also called with the
7365 '-nooverwrite' option set.
7367 When a module in the map file has the 'techmap_celltype' attribute set, it will
7368 match cells with a type that match the text value of this attribute. Otherwise
7369 the module name will be used to match the cell. Multiple space-separated cell
7370 types can be listed, and wildcards using
[] will be expanded (ie. "$_DFF_
[PN
]_"
7371 is the same as "$_DFF_P_ $_DFF_N_").
7373 When a module in the map file has the 'techmap_simplemap' attribute set, techmap
7374 will use 'simplemap' (see 'help simplemap') to map cells matching the module.
7376 When a module in the map file has the 'techmap_maccmap' attribute set, techmap
7377 will use 'maccmap' (see 'help maccmap') to map cells matching the module.
7379 When a module in the map file has the 'techmap_wrap' attribute set, techmap
7380 will create a wrapper for the cell and then run the command string that the
7381 attribute is set to on the wrapper module.
7383 When a port on a module in the map file has the 'techmap_autopurge' attribute
7384 set, and that port is not connected in the instantiation that is mapped, then
7385 then a cell port connected only to such wires will be omitted in the mapped
7386 version of the circuit.
7388 All wires in the modules from the map file matching the pattern _TECHMAP_*
7389 or *._TECHMAP_* are special wires that are used to pass instructions from
7390 the mapping module to the techmap command. At the moment the following special
7391 wires are supported:
7394 When this wire is set to a non-zero constant value, techmap will not
7395 use this module and instead try the next module with a matching
7396 'techmap_celltype' attribute.
7398 When such a wire exists but does not have a constant value after all
7399 _TECHMAP_DO_* commands have been executed, an error is generated.
7402 This wires are evaluated in alphabetical order. The constant text value
7403 of this wire is a yosys command (or sequence of commands) that is run
7404 by techmap on the module. A common use case is to run 'proc' on modules
7405 that are written using always-statements.
7407 When such a wire has a non-constant value at the time it is to be
7408 evaluated, an error is produced. That means it is possible for such a
7409 wire to start out as non-constant and evaluate to a constant value
7410 during processing of other _TECHMAP_DO_* commands.
7412 A _TECHMAP_DO_* command may start with the special token 'CONSTMAP; '.
7413 in this case techmap will create a copy for each distinct configuration
7414 of constant inputs and shorted inputs at this point and import the
7415 constant and connected bits into the map module. All further commands
7416 are executed in this copy. This is a very convenient way of creating
7417 optimized specializations of techmap modules without using the special
7418 parameters described below.
7420 A _TECHMAP_DO_* command may start with the special token 'RECURSION; '.
7421 then techmap will recursively replace the cells in the module with their
7422 implementation. This is not affected by the -max_iter option.
7424 It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '.
7426 _TECHMAP_REMOVEINIT_<port-name>_
7427 When this wire is set to a constant value, the init attribute of the wire(s)
7428 connected to this port will be consumed. This wire must have the same
7429 width as the given port, and for every bit that is set to
1 in the value,
7430 the corresponding init attribute bit will be changed to
1'bx. If all
7431 bits of an init attribute are left as x, it will be removed.
7433 In addition to this special wires, techmap also supports special parameters in
7434 modules in the map file:
7437 When a parameter with this name exists, it will be set to the type name
7438 of the cell that matches the module.
7441 When a parameter with this name exists, it will be set to the name
7442 of the cell that matches the module.
7444 _TECHMAP_CONSTMSK_<port-name>_
7445 _TECHMAP_CONSTVAL_<port-name>_
7446 When this pair of parameters is available in a module for a port, then
7447 former has a
1-bit for each constant input bit and the latter has the
7448 value for this bit. The unused bits of the latter are set to undef (x).
7450 _TECHMAP_WIREINIT_<port-name>_
7451 When a parameter with this name exists, it will be set to the initial
7452 value of the wire(s) connected to the given port, as specified by the init
7453 attribute. If the attribute doesn't exist, x will be filled for the
7454 missing bits. To remove the init attribute bits used, use the
7455 _TECHMAP_REMOVEINIT_*_ wires.
7457 _TECHMAP_BITS_CONNMAP_
7458 _TECHMAP_CONNMAP_<port-name>_
7459 For an N-bit port, the _TECHMAP_CONNMAP_<port-name>_ parameter, if it
7460 exists, will be set to an N*_TECHMAP_BITS_CONNMAP_ bit vector containing
7461 N words (of _TECHMAP_BITS_CONNMAP_ bits each) that assign each single
7462 bit driver a unique id. The values
0-
3 are reserved for
0,
1, x, and z.
7463 This can be used to detect shorted inputs.
7465 When a module in the map file has a parameter where the according cell in the
7466 design has a port, the module from the map file is only used if the port in
7467 the design is connected to a constant value. The parameter is then set to the
7470 A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name
7471 and attributes of the cell that is being replaced.
7472 A cell with a name of the form `_TECHMAP_REPLACE_.<suffix>` in the map file will
7473 be named thus but with the `_TECHMAP_REPLACE_' prefix substituted with the name
7474 of the cell being replaced.
7475 Similarly, a wire named in the form `_TECHMAP_REPLACE_.<suffix>` will cause a
7476 new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'
7477 prefix also substituted.
7479 See 'help extract' for a pass that does the opposite thing.
7481 See 'help flatten' for a pass that does flatten the design (which is
7482 essentially techmap but using the design itself as map library).
7485 \section{tee -- redirect command output to file
}
7487 \begin{lstlisting
}[numbers=left,frame=single
]
7488 tee
[-q
] [-o logfile|-a logfile
] cmd
7490 Execute the specified command, optionally writing the commands output to the
7491 specified logfile(s).
7494 Do not print output to the normal destination (console and/or log file).
7497 Write output to this file, truncate if exists.
7500 Write output to this file, append if exists.
7503 Add/subtract INT from the -v setting for this command.
7506 \section{test
\_abcloop -- automatically test handling of loops in abc command
}
7507 \label{cmd:test_abcloop
}
7508 \begin{lstlisting
}[numbers=left,frame=single
]
7509 test_abcloop
[options
]
7511 Test handling of logic loops in ABC.
7514 create this number of circuits and test them (default =
100).
7516 -s
{positive_integer
}
7517 use this value as rng seed value (default = unix time).
7520 \section{test
\_autotb -- generate simple test benches
}
7521 \label{cmd:test_autotb
}
7522 \begin{lstlisting
}[numbers=left,frame=single
]
7523 test_autotb
[options
] [filename
]
7525 Automatically create primitive Verilog test benches for all modules in the
7526 design. The generated testbenches toggle the input pins of the module in
7527 a semi-random manner and dumps the resulting output signals.
7529 This can be used to check the synthesis results for simple circuits by
7530 comparing the testbench output for the input files and the synthesis results.
7532 The backend automatically detects clock signals. Additionally a signal can
7533 be forced to be interpreted as clock signal by setting the attribute
7534 'gentb_clock' on the signal.
7536 The attribute 'gentb_constant' can be used to force a signal to a constant
7537 value after initialization. This can e.g. be used to force a reset signal
7538 low in order to explore more inner states in a state machine.
7540 The attribute 'gentb_skip' can be attached to modules to suppress testbench
7544 number of iterations the test bench should run (default =
1000)
7547 seed used for pseudo-random number generation (default =
0).
7548 a value of
0 will cause an arbitrary seed to be chosen, based on
7549 the current system time.
7552 \section{test
\_cell -- automatically test the implementation of a cell type
}
7553 \label{cmd:test_cell
}
7554 \begin{lstlisting
}[numbers=left,frame=single
]
7555 test_cell
[options
] {cell-types
}
7557 Tests the internal implementation of the given cell type (for example '$add')
7558 by comparing SAT solver, EVAL and TECHMAP implementations of the cell types..
7560 Run with 'all' instead of a cell type to run the test on all supported
7561 cell types. Use for example 'all /$add' for all cell types except $add.
7564 create this number of cell instances and test them (default =
100).
7566 -s
{positive_integer
}
7567 use this value as rng seed value (default = unix time).
7570 don't generate circuits. instead load the specified RTLIL file.
7572 -w
{filename_prefix
}
7573 don't test anything. just generate the circuits and write them
7574 to RTLIL files with the specified prefix
7577 pass this option to techmap.
7580 use "techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter
2 -autoproc"
7583 instead of calling "techmap", call "aigmap"
7586 when creating test benches with dividers, create an additional mux
7587 to mask out the division-by-zero case
7589 -script
{script_file
}
7590 instead of calling "techmap", call "script
{script_file
}".
7593 set some input bits to random constant values
7596 do not check SAT model or run SAT equivalence checking
7599 do not check const-eval models
7602 test cell edges db creator against sat-based implementation
7605 print additional debug information to the console
7608 create a Verilog test bench to test simlib and write_verilog
7611 \section{test
\_pmgen -- test pass for pmgen
}
7612 \label{cmd:test_pmgen
}
7613 \begin{lstlisting
}[numbers=left,frame=single
]
7614 test_pmgen -reduce_chain
[options
] [selection
]
7616 Demo for recursive pmgen patterns. Map chains of AND/OR/XOR to $reduce_*.
7619 test_pmgen -reduce_tree
[options
] [selection
]
7621 Demo for recursive pmgen patterns. Map trees of AND/OR/XOR to $reduce_*.
7624 test_pmgen -eqpmux
[options
] [selection
]
7626 Demo for recursive pmgen patterns. Optimize EQ/NE/PMUX circuits.
7629 test_pmgen -generate
[options
] <pattern_name>
7631 Create modules that match the specified pattern.
7634 \section{torder -- print cells in topological order
}
7636 \begin{lstlisting
}[numbers=left,frame=single
]
7637 torder
[options
] [selection
]
7639 This command prints the selected cells in topological order.
7641 -stop <cell_type> <cell_port>
7642 do not use the specified cell port in topological sorting
7645 by default Q outputs of internal FF cells and memory read port outputs
7646 are not used in topological sorting. this option deactivates that.
7649 \section{trace -- redirect command output to file
}
7651 \begin{lstlisting
}[numbers=left,frame=single
]
7654 Execute the specified command, logging all changes the command performs on
7655 the design in real time.
7658 \section{tribuf -- infer tri-state buffers
}
7660 \begin{lstlisting
}[numbers=left,frame=single
]
7661 tribuf
[options
] [selection
]
7663 This pass transforms $mux cells with 'z' inputs to tristate buffers.
7666 merge multiple tri-state buffers driving the same net
7667 into a single buffer.
7670 convert tri-state buffers that do not drive output ports
7671 to non-tristate logic. this option implies -merge.
7674 convert all tri-state buffers to non-tristate logic and
7675 add a formal assertion that no two buffers are driving the
7676 same net simultaneously. this option implies -merge.
7679 \section{uniquify -- create unique copies of modules
}
7680 \label{cmd:uniquify
}
7681 \begin{lstlisting
}[numbers=left,frame=single
]
7682 uniquify
[selection
]
7684 By default, a module that is instantiated by several other modules is only
7685 kept once in the design. This preserves the original modularity of the design
7686 and reduces the overall size of the design in memory. But it prevents certain
7687 optimizations and other operations on the design. This pass creates unique
7688 modules for all selected cells. The created modules are marked with the
7691 This commands only operates on modules that by themself have the 'unique'
7692 attribute set (the 'top' module is unique implicitly).
7695 \section{verific -- load Verilog and VHDL designs using Verific
}
7697 \begin{lstlisting
}[numbers=left,frame=single
]
7698 verific
{-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv
} <verilog-file>..
7700 Load the specified Verilog/SystemVerilog files into Verific.
7702 All files specified in one call to this command are one compilation unit.
7703 Files passed to different calls to this command are treated as belonging to
7704 different compilation units.
7706 Additional -D<macro>
[=<value>
] options may be added after the option indicating
7707 the language version (and before file names) to set additional verilog defines.
7708 The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly.
7711 verific -formal <verilog-file>..
7713 Like -sv, but define FORMAL instead of SYNTHESIS.
7716 verific
{-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl
} <vhdl-file>..
7718 Load the specified VHDL files into Verific.
7721 verific
{-f|-F
} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal
] <command-file>
7723 Load and execute the specified command file.
7724 Override verilog parsing mode can be set.
7725 The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.
7727 Command file parser supports following commands:
7728 +define - defines macro
7729 -u - upper case all identifier (makes Verilog parser case insensitive)
7730 -v - register library name (file)
7731 -y - register library name (directory)
7732 +incdir - specify include dir
7733 +libext - specify library extension
7734 +liborder - add library in ordered list
7735 +librescan - unresolved modules will be always searched starting with the first
7736 library specified by -y/-v options.
7737 -f/-file - nested -f option
7738 -F - nested -F option
7749 verific
[-work <libname>
] {-sv|-vhdl|...
} <hdl-file>
7751 Load the specified Verilog/SystemVerilog/VHDL file into the specified library.
7752 (default library when -work is not present: "work")
7755 verific
[-L <libname>
] {-sv|-vhdl|...
} <hdl-file>
7757 Look up external definitions in the specified library.
7758 (-L may be used more than once)
7761 verific -vlog-incdir <directory>..
7763 Add Verilog include directories.
7766 verific -vlog-libdir <directory>..
7768 Add Verilog library directories. Verific will search in this directories to
7769 find undefined modules.
7772 verific -vlog-define <macro>
[=<value>
]..
7774 Add Verilog defines.
7777 verific -vlog-undef <macro>..
7779 Remove Verilog defines previously set with -vlog-define.
7782 verific -set-error <msg_id>..
7783 verific -set-warning <msg_id>..
7784 verific -set-info <msg_id>..
7785 verific -set-ignore <msg_id>..
7787 Set message severity. <msg_id> is the string in square brackets when a message
7788 is printed, such as VERI-
1209.
7791 verific -import
[options
] <top-module>..
7793 Elaborate the design for the specified top modules, import to Yosys and
7794 reset the internal state of Verific.
7799 Elaborate all modules, not just the hierarchy below the given top
7800 modules. With this option the list of modules to import is optional.
7803 Create a gate-level netlist.
7806 Flatten the design in Verific before importing.
7809 Resolve references to external nets by adding module ports as needed.
7812 Generate automatic cover statements for all asserts
7815 Keep all register initializations, even those for non-FF registers.
7818 Elaborate the specified top modules (all modules when -all given) using
7819 this parameter value. Modules on which this parameter does not exist will
7820 cause Verific to produce a VERI-
1928 or VHDL-
1676 message. This option
7821 can be specified multiple times to override multiple parameters.
7822 String values must be passed in double quotes (").
7825 Verbose log messages. (-vv is even more verbose than -v.)
7827 The following additional import options are useful for debugging the Verific
7828 bindings (for Yosys and/or Verific developers):
7831 Keep going after an unsupported verific primitive is found. The
7832 unsupported primitive is added as blockbox module to the design.
7833 This will also add all SVA related cells to the design parallel to
7834 the checker logic inferred by it.
7837 Import Verific netlist as-is without translating to Yosys cell types.
7840 Ignore SVA properties, do not infer checker logic.
7843 Maximum number of ctrl bits for SVA checker FSMs (default=
16).
7846 Keep all Verific names on instances and nets. By default only
7847 user-declared names are preserved.
7850 Dump the Verific netlist as a verilog file.
7853 verific
[-work <libname>
] -pp
[options
] <filename>
[<module>
]..
7855 Pretty print design (or just module) to the specified file from the
7856 specified library. (default library when -work is not present: "work")
7858 Pretty print options:
7861 Save output for Verilog/SystemVerilog design modules (default).
7864 Save output for VHDL design units.
7867 verific -app <application>..
7869 Execute YosysHQ formal application on loaded Verilog files.
7871 Application options:
7874 Run formal application only on specified module.
7876 -blacklist <filename
[:lineno
]>
7877 Do not run application on modules from files that match the filename
7878 or filename and line number if provided in such format.
7879 Parameter can also contain comma separated list of file locations.
7882 Do not run application on locations specified in file, they can represent filename
7883 or filename and location in file.
7887 WARNING: Applications only available in commercial build.
7890 verific -template <name> <top_module>..
7892 Generate template for specified top module of loaded design.
7897 Specifies output file for generated template, by default output is stdout
7900 Generate template using this parameter value. Otherwise default parameter
7901 values will be used for templat generate functionality. This option
7902 can be specified multiple times to override multiple parameters.
7903 String values must be passed in double quotes (").
7907 WARNING: Templates only available in commercial build.
7911 verific -cfg
[<name>
[<value>
]]
7913 Get/set Verific runtime flags.
7916 Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.
7917 https://www.yosyshq.com/
7919 Contact office@yosyshq.com for free evaluation
7920 binaries of YosysHQ Tabby CAD Suite.
7923 \section{verilog
\_defaults -- set default options for read
\_verilog}
7924 \label{cmd:verilog_defaults
}
7925 \begin{lstlisting
}[numbers=left,frame=single
]
7926 verilog_defaults -add
[options
]
7928 Add the specified options to the list of default options to read_verilog.
7931 verilog_defaults -clear
7933 Clear the list of Verilog default options.
7936 verilog_defaults -push
7937 verilog_defaults -pop
7939 Push or pop the list of default options to a stack. Note that -push does
7943 \section{verilog
\_defines -- define and undefine verilog defines
}
7944 \label{cmd:verilog_defines
}
7945 \begin{lstlisting
}[numbers=left,frame=single
]
7946 verilog_defines
[options
]
7948 Define and undefine verilog preprocessor macros.
7951 define the preprocessor symbol 'name' and set its optional value
7955 undefine the preprocessor symbol 'name'
7958 clear list of defined preprocessor symbols
7961 list currently defined preprocessor symbols
7964 \section{wbflip -- flip the whitebox attribute
}
7966 \begin{lstlisting
}[numbers=left,frame=single
]
7969 Flip the whitebox attribute on selected cells. I.e. if it's set, unset it, and
7970 vice-versa. Blackbox cells are not effected by this command.
7973 \section{wreduce -- reduce the word size of operations if possible
}
7975 \begin{lstlisting
}[numbers=left,frame=single
]
7976 wreduce
[options
] [selection
]
7978 This command reduces the word size of operations. For example it will replace
7979 the
32 bit adders in the following code with adders of more appropriate widths:
7981 module test(input
[3:
0] a, b, c, output
[7:
0] y);
7982 assign y = a + b + c +
1;
7988 Do not change the width of memory address ports. Use this options in
7989 flows that use the 'memory_memx' pass.
7992 Do not optimize explicit don't-care values.
7995 \section{write
\_aiger -- write design to AIGER file
}
7996 \label{cmd:write_aiger
}
7997 \begin{lstlisting
}[numbers=left,frame=single
]
7998 write_aiger
[options
] [filename
]
8000 Write the current design to an AIGER file. The design must be flattened and
8001 must not contain any cell types except $_AND_, $_NOT_, simple FF types,
8002 $assert and $assume cells, and $initstate cells.
8004 $assert and $assume cells are converted to AIGER bad state properties and
8005 invariant constraints.
8008 write ASCII version of AIGER format
8011 convert FFs to zero-initialized FFs, adding additional inputs for
8015 design outputs are AIGER bad state properties
8018 include a symbol table in the generated AIGER file
8021 write an extra file with port and latch symbols
8024 like -map, but more verbose
8027 make indexes zero based, enable using map files with smt solvers.
8030 If the design contains no input/output/assert/flip-flop then create one
8031 dummy input/output/bad_state-pin or latch to make the tools reading the
8035 \section{write
\_blif -- write design to BLIF file
}
8036 \label{cmd:write_blif
}
8037 \begin{lstlisting
}[numbers=left,frame=single
]
8038 write_blif
[options
] [filename
]
8040 Write the current design to an BLIF file.
8043 set the specified module as design top module
8045 -buf <cell-type> <in-port> <out-port>
8046 use cells of type <cell-type> with the specified port names for buffers
8048 -unbuf <cell-type> <in-port> <out-port>
8049 replace buffer cells with the specified name and port names with
8050 a .names statement that models a buffer
8052 -true <cell-type> <out-port>
8053 -false <cell-type> <out-port>
8054 -undef <cell-type> <out-port>
8055 use the specified cell types to drive nets that are constant
1,
0, or
8056 undefined. when '-' is used as <cell-type>, then <out-port> specifies
8057 the wire name to be used for the constant signal and no cell driving
8058 that wire is generated. when '+' is used as <cell-type>, then <out-port>
8059 specifies the wire name to be used for the constant signal and a .names
8060 statement is generated to drive the wire.
8063 if a net name is aliasing another net name, then by default a net
8064 without fanout is created that is driven by the other net. This option
8065 suppresses the generation of this nets without fanout.
8067 The following options can be useful when the generated file is not going to be
8068 read by a BLIF parser but a custom tool. It is recommended to not name the output
8069 file *.blif when any of this options is used.
8072 do not translate Yosys's internal gates to generic BLIF logic
8073 functions. Instead create .subckt or .gate lines for all cells.
8076 print .gate instead of .subckt lines for all cells that are not
8077 instantiations of other modules from this design.
8080 do not generate buffers for connected wires. instead use the
8081 non-standard .conn statement.
8084 use the non-standard .attr statement to write cell attributes
8087 use the non-standard .param statement to write cell parameters
8090 use the non-standard .cname statement to write cell names
8093 enable -cname and -attr functionality for .names statements
8094 (the .cname and .attr statements will be included in the BLIF
8095 output after the truth table for the .names statement)
8098 write blackbox cells with .blackbox statement.
8101 do not write definitions for the $true, $false and $undef wires.
8104 \section{write
\_btor -- write design to BTOR file
}
8105 \label{cmd:write_btor
}
8106 \begin{lstlisting
}[numbers=left,frame=single
]
8107 write_btor
[options
] [filename
]
8109 Write a BTOR description of the current design.
8112 Add comments and indentation to BTOR output file
8115 Output only a single bad property for all asserts
8118 Output cover properties using 'bad' statements instead of asserts
8121 Create additional info file with auxiliary information
8124 Output symbols for internal netnames (starting with '$')
8127 \section{write
\_cxxrtl -- convert design to C++ RTL simulation
}
8128 \label{cmd:write_cxxrtl
}
8129 \begin{lstlisting
}[numbers=left,frame=single
]
8130 write_cxxrtl
[options
] [filename
]
8132 Write C++ code that simulates the design. The generated code requires a driver
8133 that instantiates the design, toggles its clock, and interacts with its ports.
8135 The following driver may be used as an example for a design with a single clock
8136 driving rising edge triggered flip-flops:
8141 cxxrtl_design::p_top top;
8145 top.p_clk.set(false);
8147 top.p_clk.set(true);
8152 Note that CXXRTL simulations, just like the hardware they are simulating, are
8153 subject to race conditions. If, in the example above, the user logic would run
8154 simultaneously with the rising edge of the clock, the design would malfunction.
8156 This backend supports replacing parts of the design with black boxes implemented
8157 in C++. If a module marked as a CXXRTL black box, its implementation is ignored,
8158 and the generated code consists only of an interface and a factory function.
8159 The driver must implement the factory function that creates an implementation of
8160 the black box, taking into account the parameters it is instantiated with.
8162 For example, the following Verilog code defines a CXXRTL black box interface for
8163 a synchronous debug sink:
8165 (* cxxrtl_blackbox *)
8167 (* cxxrtl_edge = "p" *) input clk;
8170 (* cxxrtl_sync *) output
[7:
0] o_data;
8173 For this HDL interface, this backend will generate the following C++ interface:
8175 struct bb_p_debug : public module
{
8177 bool posedge_p_clk() const
{ /* ... */
}
8182 bool eval() override;
8183 bool commit() override;
8185 static std::unique_ptr<bb_p_debug>
8186 create(std::string name, metadata_map parameters, metadata_map attributes);
8189 The `create' function must be implemented by the driver. For example, it could
8190 always provide an implementation logging the values to standard error stream:
8192 namespace cxxrtl_design
{
8194 struct stderr_debug : public bb_p_debug
{
8195 bool eval() override
{
8196 if (posedge_p_clk() && p_en)
8197 fprintf(stderr, "debug:
%02x\n", p_i_data.data[0]);
8198 p_o_data.next = p_i_data;
8199 return bb_p_debug::eval();
8203 std::unique_ptr<bb_p_debug>
8204 bb_p_debug::create(std::string name, cxxrtl::metadata_map parameters,
8205 cxxrtl::metadata_map attributes)
{
8206 return std::make_unique<stderr_debug>();
8211 For complex applications of black boxes, it is possible to parameterize their
8212 port widths. For example, the following Verilog code defines a CXXRTL black box
8213 interface for a configurable width debug sink:
8215 (* cxxrtl_blackbox, cxxrtl_template = "WIDTH" *)
8217 parameter WIDTH =
8;
8218 (* cxxrtl_edge = "p" *) input clk;
8220 (* cxxrtl_width = "WIDTH" *) input
[WIDTH -
1:
0] i_data;
8221 (* cxxrtl_width = "WIDTH" *) output
[WIDTH -
1:
0] o_data;
8224 For this parametric HDL interface, this backend will generate the following C++
8225 interface (only the differences are shown):
8227 template<size_t WIDTH>
8228 struct bb_p_debug : public module
{
8230 value<WIDTH> p_i_data;
8231 wire<WIDTH> p_o_data;
8233 static std::unique_ptr<bb_p_debug<WIDTH>>
8234 create(std::string name, metadata_map parameters, metadata_map attributes);
8237 The `create' function must be implemented by the driver, specialized for every
8238 possible combination of template parameters. (Specialization is necessary to
8239 enable separate compilation of generated code and black box implementations.)
8241 template<size_t SIZE>
8242 struct stderr_debug : public bb_p_debug<SIZE>
{
8247 std::unique_ptr<bb_p_debug<
8>>
8248 bb_p_debug<
8>::create(std::string name, cxxrtl::metadata_map parameters,
8249 cxxrtl::metadata_map attributes)
{
8250 return std::make_unique<stderr_debug<
8>>();
8253 The following attributes are recognized by this backend:
8256 only valid on modules. if specified, the module contents are ignored,
8257 and the generated code includes only the module interface and a factory
8258 function, which will be called to instantiate the module.
8261 only valid on inputs of black boxes. must be one of "p", "n", "a".
8262 if specified on signal `clk`, the generated code includes edge detectors
8263 `posedge_p_clk()` (if "p"), `negedge_p_clk()` (if "n"), or both (if
8264 "a"), simplifying implementation of clocked black boxes.
8267 only valid on black boxes. must contain a space separated sequence of
8268 identifiers that have a corresponding black box parameters. for each
8269 of them, the generated code includes a `size_t` template parameter.
8272 only valid on ports of black boxes. must be a constant expression, which
8273 is directly inserted into generated code.
8275 cxxrtl_comb, cxxrtl_sync
8276 only valid on outputs of black boxes. if specified, indicates that every
8277 bit of the output port is driven, correspondingly, by combinatorial or
8278 synchronous logic. this knowledge is used for scheduling optimizations.
8279 if neither is specified, the output will be pessimistically treated as
8280 driven by both combinatorial and synchronous logic.
8282 The following options are supported by this backend:
8284 -print-wire-types, -print-debug-wire-types
8285 enable additional debug logging, for pass developers.
8288 generate separate interface (.h) and implementation (.cc) files.
8289 if specified, the backend must be called with a filename, and filename
8290 of the interface is derived from filename of the implementation.
8291 otherwise, interface and implementation are generated together.
8293 -namespace <ns-name>
8294 place the generated code into namespace <ns-name>. if not specified,
8295 "cxxrtl_design" is used.
8298 use design hierarchy as-is. in most designs, a top module should be
8299 present as it is exposed through the C API and has unbuffered outputs
8300 for improved performance; it will be determined automatically if absent.
8303 don't flatten the design. fully flattened designs can evaluate within
8304 one delta cycle if they have no combinatorial feedback.
8305 note that the debug interface and waveform dumps use full hierarchical
8306 names for all wires even in flattened designs.
8309 don't convert processes to netlists. in most designs, converting
8310 processes significantly improves evaluation performance at the cost of
8311 slight increase in compilation time.
8314 set the optimization level. the default is -O6. higher optimization
8315 levels dramatically decrease compile and run time, and highest level
8316 possible for a design should be used.
8322 unbuffer internal wires if possible.
8325 like -O1, and localize internal wires if possible.
8328 like -O2, and inline internal wires if possible.
8331 like -O3, and unbuffer public wires not marked
(*keep*) if possible.
8334 like -O4, and localize public wires not marked
(*keep*) if possible.
8337 like -O5, and inline public wires not marked
(*keep*) if possible.
8340 set the debug level. the default is -g4. higher debug levels provide
8341 more visibility and generate more code, but do not pessimize evaluation.
8344 no debug information. the C API is disabled.
8347 include bare minimum of debug information necessary to access all design
8348 state. the C API is enabled.
8351 like -g1, but include debug information for all public wires that are
8352 directly accessible through the C++ interface.
8355 like -g2, and include debug information for public wires that are tied
8356 to a constant or another public wire.
8359 like -g3, and compute debug information on demand for all public wires
8360 that were optimized out.
8363 \section{write
\_edif -- write design to EDIF netlist file
}
8364 \label{cmd:write_edif
}
8365 \begin{lstlisting
}[numbers=left,frame=single
]
8366 write_edif
[options
] [filename
]
8368 Write the current design to an EDIF netlist file.
8371 set the specified module as design top module
8374 do not create "GND" and "VCC" cells. (this will produce an error
8375 if the design contains constant nets. use "hilomap" to map to custom
8376 constant drivers first)
8379 create "GND" and "VCC" cells with "Y" outputs. (the default is "G"
8380 for "GND" and "P" for "VCC".)
8383 create EDIF properties for cell attributes
8386 create extra KEEP nets by allowing a cell to drive multiple nets.
8388 -pvector
{par|bra|ang
}
8389 sets the delimiting character for module port rename clauses to
8390 parentheses, square brackets, or angle brackets.
8392 Unfortunately there are different "flavors" of the EDIF file format. This
8393 command generates EDIF files for the Xilinx place&route tools. It might be
8394 necessary to make small modifications to this command when a different tool
8398 \section{write
\_file -- write a text to a file
}
8399 \label{cmd:write_file
}
8400 \begin{lstlisting
}[numbers=left,frame=single
]
8401 write_file
[options
] output_file
[input_file
]
8403 Write the text from the input file to the output file.
8406 Append to output file (instead of overwriting)
8409 Inside a script the input file can also can a here-
document:
8411 write_file hello.txt <<EOT
8416 \section{write
\_firrtl -- write design to a FIRRTL file
}
8417 \label{cmd:write_firrtl
}
8418 \begin{lstlisting
}[numbers=left,frame=single
]
8419 write_firrtl
[options
] [filename
]
8421 Write a FIRRTL netlist of the current design.
8422 The following commands are executed by this command:
8428 \section{write
\_ilang -- (deprecated) alias of write
\_rtlil}
8429 \label{cmd:write_ilang
}
8430 \begin{lstlisting
}[numbers=left,frame=single
]
8431 See `help write_rtlil`.
8434 \section{write
\_intersynth -- write design to InterSynth netlist file
}
8435 \label{cmd:write_intersynth
}
8436 \begin{lstlisting
}[numbers=left,frame=single
]
8437 write_intersynth
[options
] [filename
]
8439 Write the current design to an 'intersynth' netlist file. InterSynth is
8440 a tool for Coarse-Grain Example-Driven Interconnect Synthesis.
8443 do not generate celltypes and conntypes commands. i.e. just output
8444 the netlists. this is used for postsilicon synthesis.
8446 -lib <verilog_or_rtlil_file>
8447 Use the specified library file for determining whether cell ports are
8448 inputs or outputs. This option can be used multiple times to specify
8449 more than one library.
8452 only write selected modules. modules must be selected entirely or
8455 http://bygone.clairexen.net/intersynth/
8458 \section{write
\_jny -- generate design metadata
}
8459 \label{cmd:write_jny
}
8460 \begin{lstlisting
}[numbers=left,frame=single
]
8461 jny
[options
] [selection
]
8464 Don't include connection information in the netlist output.
8467 Don't include attributed information in the netlist output.
8470 Don't include property information in the netlist output.
8472 Write a JSON metadata for the current design
8475 \section{write
\_json -- write design to a JSON file
}
8476 \label{cmd:write_json
}
8477 \begin{lstlisting
}[numbers=left,frame=single
]
8478 write_json
[options
] [filename
]
8480 Write a JSON netlist of the current design.
8483 include AIG models for the different gate types
8486 emit
32-bit or smaller fully-defined parameter values directly
8487 as JSON numbers (for compatibility with old parsers)
8490 The general syntax of the JSON output created by this command is as follows:
8493 "creator": "Yosys <version info>",
8497 <attribute_name>: <attribute_value>,
8500 "parameter_default_values":
{
8501 <parameter_name>: <parameter_value>,
8505 <port_name>: <port_details>,
8509 <cell_name>: <cell_details>,
8513 <memory_name>: <memory_details>,
8517 <net_name>: <net_details>,
8527 Where <port_details> is:
8530 "direction": <"input" | "output" | "inout">,
8531 "bits": <bit_vector>
8532 "offset": <the lowest bit index in use, if non-
0>
8533 "upto": <
1 if the port bit indexing is MSB-first>
8534 "signed": <
1 if the port is signed>
8537 The "offset" and "upto" fields are skipped if their value would be
0.They don't affect connection semantics, and are only used to preserve originalHDL bit indexing.And <cell_details> is:
8540 "hide_name": <
1 |
0>,
8541 "type": <cell_type>,
8542 "model": <AIG model name, if -aig option used>,
8544 <parameter_name>: <parameter_value>,
8548 <attribute_name>: <attribute_value>,
8551 "port_directions":
{
8552 <port_name>: <"input" | "output" | "inout">,
8556 <port_name>: <bit_vector>,
8561 And <memory_details> is:
8564 "hide_name": <
1 |
0>,
8566 <attribute_name>: <attribute_value>,
8569 "width": <memory width>
8570 "start_offset": <the lowest valid memory address>
8571 "size": <memory size>
8574 And <net_details> is:
8577 "hide_name": <
1 |
0>,
8578 "bits": <bit_vector>
8579 "offset": <the lowest bit index in use, if non-
0>
8580 "upto": <
1 if the port bit indexing is MSB-first>
8581 "signed": <
1 if the port is signed>
8584 The "hide_name" fields are set to
1 when the name of this cell or net is
8585 automatically created and is likely not of interest for a regular user.
8587 The "port_directions" section is only included for cells for which the
8590 Module and cell ports and nets can be single bit wide or vectors of multiple
8591 bits. Each individual signal bit is assigned a unique integer. The <bit_vector>
8592 values referenced above are vectors of this integers. Signal bits that are
8593 connected to a constant driver are denoted as string "
0", "
1", "x", or
8594 "z" instead of a number.
8596 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
]* */.
8598 For example the following Verilog code:
8600 module test(input x, y);
8601 (* keep *) foo #(.P(
42), .Q(
1337))
8602 foo_inst (.A(
{x, y
}), .B(
{y, x
}), .C(
{4'd10,
{4{x
}}}));
8605 Translates to the following JSON output:
8608 "creator": "Yosys
0.9+
2406 (git sha1 fb1168d8, clang
9.0.1 -fPIC -Os)",
8612 "cells_not_processed": "
00000000000000000000000000000001",
8613 "src": "test.v:
1.1-
4.10"
8617 "direction": "input",
8621 "direction": "input",
8630 "P": "
00000000000000000000000000101010",
8631 "Q": "
00000000000000000000010100111001"
8634 "keep": "
00000000000000000000000000000001",
8635 "module_not_derived": "
00000000000000000000000000000001",
8636 "src": "test.v:
3.1-
3.55"
8641 "C":
[ 2,
2,
2,
2, "
0", "
1", "
0", "
1"
]
8650 "src": "test.v:
1.19-
1.20"
8657 "src": "test.v:
1.22-
1.23"
8665 The models are given as And-Inverter-Graphs (AIGs) in the following form:
8669 /*
0 */
[ <node-spec>
],
8670 /*
1 */
[ <node-spec>
],
8671 /*
2 */
[ <node-spec>
],
8677 The following node-types may be used:
8679 [ "port", <portname>, <bitindex>, <out-list>
]
8680 - the value of the specified input port bit
8682 [ "nport", <portname>, <bitindex>, <out-list>
]
8683 - the inverted value of the specified input port bit
8685 [ "and", <node-index>, <node-index>, <out-list>
]
8686 - the ANDed value of the specified nodes
8688 [ "nand", <node-index>, <node-index>, <out-list>
]
8689 - the inverted ANDed value of the specified nodes
8691 [ "true", <out-list>
]
8692 - the constant value
1
8694 [ "false", <out-list>
]
8695 - the constant value
0
8697 All nodes appear in topological order. I.e. only nodes with smaller indices
8698 are referenced by "and" and "nand" nodes.
8700 The optional <out-list> at the end of a node specification is a list of
8701 output portname and bitindex pairs, specifying the outputs driven by this node.
8703 For example, the following is the model for a
3-input
3-output $reduce_and cell
8704 inferred by the following code:
8706 module test(input
[2:
0] in, output
[2:
0] out);
8710 "$reduce_and:
3U:
3":
[
8711 /*
0 */
[ "port", "A",
0 ],
8712 /*
1 */
[ "port", "A",
1 ],
8713 /*
2 */
[ "and",
0,
1 ],
8714 /*
3 */
[ "port", "A",
2 ],
8715 /*
4 */
[ "and",
2,
3, "Y",
0 ],
8716 /*
5 */
[ "false", "Y",
1, "Y",
2 ]
8719 Future version of Yosys might add support for additional fields in the JSON
8720 format. A program processing this format must ignore all unknown fields.
8723 \section{write
\_rtlil -- write design to RTLIL file
}
8724 \label{cmd:write_rtlil
}
8725 \begin{lstlisting
}[numbers=left,frame=single
]
8726 write_rtlil
[filename
]
8728 Write the current design to an RTLIL file. (RTLIL is a text representation
8729 of a design in yosys's internal format.)
8732 only write selected parts of the design.
8735 \section{write
\_simplec -- convert design to simple C code
}
8736 \label{cmd:write_simplec
}
8737 \begin{lstlisting
}[numbers=left,frame=single
]
8738 write_simplec
[options
] [filename
]
8740 Write simple C code for simulating the design. The C code written can be used to
8741 simulate the design in a C environment, but the purpose of this command is to
8742 generate code that works well with C-based formal verification.
8745 this will print the recursive walk used to export the modules.
8747 -i8, -i16, -i32, -i64
8748 set the maximum integer bit width to use in the generated code.
8750 THIS COMMAND IS UNDER CONSTRUCTION
8753 \section{write
\_smt2 -- write design to SMT-LIBv2 file
}
8754 \label{cmd:write_smt2
}
8755 \begin{lstlisting
}[numbers=left,frame=single
]
8756 write_smt2
[options
] [filename
]
8758 Write a SMT-LIBv2
[1] description of the current design. For a module with name
8759 '<mod>' this will declare the sort '<mod>_s' (state of the module) and will
8760 define and declare functions operating on that state.
8762 The following SMT2 functions are generated for a module with name '<mod>'.
8763 Some declarations/definitions are printed with a special comment. A prover
8764 using the SMT2 files can use those comments to collect all relevant metadata
8767 ; yosys-smt2-module <mod>
8768 (declare-sort |<mod>_s|
0)
8769 The sort representing a state of module <mod>.
8771 (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))
8772 This function must be asserted for each state to establish the
8775 ; yosys-smt2-input <wirename> <width>
8776 ; yosys-smt2-output <wirename> <width>
8777 ; yosys-smt2-register <wirename> <width>
8778 ; yosys-smt2-wire <wirename> <width>
8779 (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))
8780 (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)
8781 For each port, register, and wire with the 'keep' attribute set an
8782 accessor function is generated. Single-bit wires are returned as Bool,
8783 multi-bit wires as BitVec.
8785 ; yosys-smt2-cell <submod> <instancename>
8786 (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)
8787 There is a function like that for each hierarchical instance. It
8788 returns the sort that represents the state of the sub-module that
8789 implements the instance.
8791 (declare-fun |<mod>_is| (|<mod>_s|) Bool)
8792 This function must be asserted 'true' for initial states, and 'false'
8795 (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))
8796 This function must be asserted 'true' for initial states. For
8797 non-initial states it must be left unconstrained.
8799 (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))
8800 This function evaluates to 'true' if the states 'state' and
8801 'next_state' form a valid state transition.
8803 (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))
8804 This function evaluates to 'true' if all assertions hold in the state.
8806 (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))
8807 This function evaluates to 'true' if all assumptions hold in the state.
8809 ; yosys-smt2-assert <id> <filename:linenum>
8810 (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))
8811 Each $assert cell is converted into one of this functions. The function
8812 evaluates to 'true' if the assert statement holds in the state.
8814 ; yosys-smt2-assume <id> <filename:linenum>
8815 (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))
8816 Each $assume cell is converted into one of this functions. The function
8817 evaluates to 'true' if the assume statement holds in the state.
8819 ; yosys-smt2-cover <id> <filename:linenum>
8820 (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))
8821 Each $cover cell is converted into one of this functions. The function
8822 evaluates to 'true' if the cover statement is activated in the state.
8827 this will print the recursive walk used to export the modules.
8830 Use a BitVec sort to represent a state instead of an uninterpreted
8831 sort. As a side-effect this will prevent use of arrays to model
8835 Use SMT-LIB
2.6 style datatypes to represent a state instead of an
8839 disable support for BitVec (FixedSizeBitVectors theory). without this
8840 option multi-bit wires are represented using the BitVec sort and
8841 support for coarse grain cells (incl. arithmetic) is enabled.
8844 disable support for memories (via ArraysEx theory). this option is
8845 implied by -nobv. only $mem cells without merged registers in
8846 read ports are supported. call "memory" with -nordff to make sure
8847 that no registers are merged into $mem read ports. '<mod>_m' functions
8848 will be generated for accessing the arrays that are used to represent
8852 create '<mod>_n' functions for all public wires. by default only ports,
8853 registers, and wires with the 'keep' attribute are exported.
8855 -tpl <template_file>
8856 use the given template file. the line containing only the token '
%%'
8857 is replaced with the regular output of this command.
8859 -solver-option <option> <value>
8860 emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write
8861 the given option as a `(set-option ...)` command in the SMT-LIBv2.
8863 [1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David
8864 R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf
8866 ---------------------------------------------------------------------------
8870 Consider the following module (test.v). We want to prove that the output can
8871 never transition from a non-zero value to a zero value.
8873 module test(input clk, output reg
[3:
0] y);
8874 always @(posedge clk)
8878 For this proof we create the following template (test.tpl).
8880 ; we need QF_UFBV for this proof
8883 ; insert the auto-generated code here
8886 ; declare two state variables s1 and s2
8887 (declare-fun s1 () test_s)
8888 (declare-fun s2 () test_s)
8890 ; state s2 is the successor of state s1
8891 (assert (test_t s1 s2))
8893 ; we are looking for a model with y non-zero in s1
8894 (assert (distinct (|test_n y| s1) #b0000))
8896 ; we are looking for a model with y zero in s2
8897 (assert (= (|test_n y| s2) #b0000))
8899 ; is there such a model?
8902 The following yosys script will create a 'test.smt2' file for our proof:
8905 hierarchy -check; proc; opt; check -assert
8906 write_smt2 -bv -tpl test.tpl test.smt2
8908 Running 'cvc4 test.smt2' will print 'unsat' because y can never transition
8909 from non-zero to zero in the test design.
8912 \section{write
\_smv -- write design to SMV file
}
8913 \label{cmd:write_smv
}
8914 \begin{lstlisting
}[numbers=left,frame=single
]
8915 write_smv
[options
] [filename
]
8917 Write an SMV description of the current design.
8920 this will print the recursive walk used to export the modules.
8922 -tpl <template_file>
8923 use the given template file. the line containing only the token '
%%'
8924 is replaced with the regular output of this command.
8926 THIS COMMAND IS UNDER CONSTRUCTION
8929 \section{write
\_spice -- write design to SPICE netlist file
}
8930 \label{cmd:write_spice
}
8931 \begin{lstlisting
}[numbers=left,frame=single
]
8932 write_spice
[options
] [filename
]
8934 Write the current design to an SPICE netlist file.
8937 generate multi-bit ports in MSB first order
8938 (default is LSB first)
8941 set the net name for constant
0 (default: Vss)
8944 set the net name for constant
1 (default: Vdd)
8947 set the name for jumper element (default: DC)
8948 (used to connect different nets)
8951 prefix for not-connected nets (default: _NC)
8954 include names of internal ($-prefixed) nets in outputs
8955 (default is to use net numbers instead)
8958 set the specified module as design top module
8961 \section{write
\_table -- write design as connectivity table
}
8962 \label{cmd:write_table
}
8963 \begin{lstlisting
}[numbers=left,frame=single
]
8964 write_table
[options
] [filename
]
8966 Write the current design as connectivity table. The output is a tab-separated
8967 ASCII table with the following columns:
8976 module inputs and outputs are output using cell type and port '-' and with
8977 'pi' (primary input) or 'po' (primary output) or 'pio' as direction.
8980 \section{write
\_verilog -- write design to Verilog file
}
8981 \label{cmd:write_verilog
}
8982 \begin{lstlisting
}[numbers=left,frame=single
]
8983 write_verilog
[options
] [filename
]
8985 Write the current design to a Verilog file.
8988 with this option, SystemVerilog constructs like always_comb are used
8991 without this option all internal object names (the ones with a dollar
8992 instead of a backslash prefix) are changed to short names in the
8993 format '_<number>_'.
8995 -renameprefix <prefix>
8996 insert this prefix in front of auto-generated instance names
8999 with this option no attributes are included in the output
9002 with this option attributes are included as comments in the output
9005 without this option all internal cells are converted to Verilog
9009 add initial statements with hierarchical refs to initialize FFs when
9013 32-bit constant values are by default dumped as decimal numbers,
9014 not bit pattern. This option deactivates this feature and instead
9015 will write out all constants in binary.
9018 dump
32-bit constants in decimal and without size and radix
9021 constant values that are compatible with hex output are usually
9022 dumped as hex values. This option deactivates this feature and
9023 instead will write out all constants in binary.
9026 Parameters and attributes that are specified as strings in the
9027 original input will be output as strings by this back-end. This
9028 deactivates this feature and instead will write string constants
9032 Connection assignments with simple left hand side without concatenations.
9035 instead of initializing memories using assignments to individual
9036 elements, use the '$readmemh' function to read initialization data
9037 from a file. This data is written to a file named by appending
9038 a sequential index to the Verilog filename and replacing the extension
9039 with '.mem', e.g. 'write_verilog -extmem foo.v' writes 'foo-
1.mem',
9040 'foo-
2.mem' and so on.
9043 use 'defparam' statements instead of the Verilog-
2001 syntax for
9047 usually modules with the 'blackbox' attribute are ignored. with
9048 this option set only the modules with the 'blackbox' attribute
9049 are written to the output file.
9052 only write selected modules. modules must be selected entirely or
9056 verbose output (print new names of all renamed wires and cells)
9058 Note that RTLIL processes can't always be mapped directly to Verilog
9059 always blocks. This frontend should only be used to export an RTLIL
9060 netlist, i.e. after the "proc" pass has been used to convert all
9061 processes to logic networks and registers. A warning is generated when
9062 this command is called on a design with RTLIL processes.
9065 \section{write
\_xaiger -- write design to XAIGER file
}
9066 \label{cmd:write_xaiger
}
9067 \begin{lstlisting
}[numbers=left,frame=single
]
9068 write_xaiger
[options
] [filename
]
9070 Write the top module (according to the
(* top *) attribute or if only one module
9071 is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, (optionally
9072 $_DFF_N_, $_DFF_P_), or non
(* abc9_box *) cells will be converted into psuedo-
9073 inputs and pseudo-outputs. Whitebox contents will be taken from the equivalent
9074 module in the '$abc9_holes' design, if it exists.
9077 write ASCII version of AIGER format
9080 write an extra file with port and box symbols
9083 write $_DFF_
[NP
]_ cells
9086 \section{xilinx
\_dffopt -- Xilinx: optimize FF control signal usage
}
9087 \label{cmd:xilinx_dffopt
}
9088 \begin{lstlisting
}[numbers=left,frame=single
]
9089 xilinx_dffopt
[options
] [selection
]
9091 Converts hardware clock enable and set/reset signals on FFs to emulation
9092 using LUTs, if doing so would improve area. Operates on post-techmap Xilinx
9096 Assume a LUT4-based device (instead of a LUT6-based device).
9099 \section{xilinx
\_dsp -- Xilinx: pack resources into DSPs
}
9100 \label{cmd:xilinx_dsp
}
9101 \begin{lstlisting
}[numbers=left,frame=single
]
9102 xilinx_dsp
[options
] [selection
]
9104 Pack input registers (A2, A1, B2, B1, C, D, AD; with optional enable/reset),
9105 pipeline registers (M; with optional enable/reset), output registers (P; with
9106 optional enable/reset), pre-adder and/or post-adder into Xilinx DSP resources.
9108 Multiply-accumulate operations using the post-adder with feedback on the 'C'
9109 input will be folded into the DSP. In this scenario only, the 'C' input can be
9110 used to override the current accumulation result with a new value, which will
9111 be added to the multiplier result to form the next accumulation result.
9113 Use of the dedicated 'PCOUT' -> 'PCIN' cascade path is detected for 'P' -> 'C'
9114 connections (optionally, where 'P' is right-shifted by
17-bits and used as an
9115 input to the post-adder -- a pattern common for summing partial products to
9116 implement wide multipliers). Limited support also exists for similar cascading
9117 for A and B using '
[AB
]COUT' -> '
[AB
]CIN'. Currently, cascade chains are limited
9118 to a maximum length of
20 cells, corresponding to the smallest Xilinx
7 Series
9121 This pass is a no-op if the scratchpad variable 'xilinx_dsp.multonly' is set
9125 Experimental feature: addition/subtractions less than
12 or
24 bits with the
9126 '
(* use_dsp="simd" *)' attribute attached to the output wire or attached to
9127 the add/subtract operator will cause those operations to be implemented using
9128 the 'SIMD' feature of DSPs.
9130 Experimental feature: the presence of a `$ge' cell attached to the registered
9131 P output implementing the operation "(P >= <power-of-
2>)" will be transformed
9132 into using the DSP48E1's pattern detector feature for overflow detection.
9134 -family
{xcup|xcu|xc7|xc6v|xc5v|xc4v|xc6s|xc3sda
}
9135 select the family to target
9139 \section{xilinx
\_srl -- Xilinx shift register extraction
}
9140 \label{cmd:xilinx_srl
}
9141 \begin{lstlisting
}[numbers=left,frame=single
]
9142 xilinx_srl
[options
] [selection
]
9144 This pass converts chains of built-in flops (bit-level: $_DFF_
[NP
]_, $_DFFE_*
9145 and word-level: $dff, $dffe) as well as Xilinx flops (FDRE, FDRE_1) into a
9146 $__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock polarity,
9147 enable, and enable polarity (where relevant).
9148 Flops with resets cannot be mapped to Xilinx devices and will not be inferred.
9150 min length of shift register (default =
3)
9153 infer fixed-length shift registers.
9156 infer variable-length shift registers (i.e. fixed-length shifts where
9157 each element also fans-out to a $shiftx cell).
9160 \section{zinit -- add inverters so all FF are zero-initialized
}
9162 \begin{lstlisting
}[numbers=left,frame=single
]
9163 zinit
[options
] [selection
]
9165 Add inverters as needed to make all FFs zero-initialized.
9168 also add zero initialization to uninitialized FFs