Formal verification¶

assertpmux - adds asserts for parallel muxes¶

yosys> help assertpmux¶

assertpmux [options] [selection]¶

This command adds asserts to the design that assert that all parallel muxes
($pmux cells) have a maximum of one of their inputs enable at any time.

-noinit

do not enforce the pmux condition during the init state

-always

usually the $pmux condition is only checked when the $pmux output
is used by the mux tree it drives. this option will deactivate this
additional constraint and check the $pmux condition always.

Note

Help text automatically generated from passes/sat/assertpmux.cc:185

async2sync - convert async FF inputs to sync circuits¶

yosys> help async2sync¶

async2sync [options] [selection]¶

This command replaces async FF inputs with sync circuits emulating the same
behavior for when the async signals are actually synchronized to the clock.

This pass assumes negative hold time for the async FF inputs. For example when
a reset deasserts with the clock edge, then the FF output will still drive the
reset value in the next cycle regardless of the data-in value at the time of
the clock edge.

-nolower

Do not automatically run 'chformal -lower' to lower $check cells.

Note

Help text automatically generated from passes/sat/async2sync.cc:30

chformal - change formal constraints of the design¶

yosys> help chformal¶

chformal [types] [mode] [options] [selection]¶

Make changes to the formal constraints of the design. The [types] options the type of constraint to operate on. If none of the following options are given, the command will operate on all constraint types:

-assert: $assert cells, representing assert(...) constraints
-assume: $assume cells, representing assume(...) constraints
-live: $live cells, representing assert(s_eventually ...)
-fair: $fair cells, representing assume(s_eventually ...)
-cover: $cover cells, representing cover() statements

Additionally chformal will operate on $check cells corresponding to the selected constraint types.

Exactly one of the following modes must be specified:

-remove

remove the cells and thus constraints from the design

-early

bypass FFs that only delay the activation of a constraint. When inputs of the bypassed FFs do not remain stable between clock edges, this may result in unexpected behavior.

-delay <N>

delay activation of the constraint by <N> clock cycles

-skip <N>

ignore activation of the constraint in the first <N> clock cycles

-coverenable

add cover statements for the enable signals of the constraints

Note: For the Verific frontend it is currently not guaranteed that a reachable SVA statement corresponds to an active enable signal.

-assert2assume

-assert2cover

-assume2assert

-live2fair

-fair2live

change the roles of cells as indicated. these options can be combined

-lower

convert each $check cell into an $assert, $assume, $live, $fair or $cover cell. If the $check cell contains a message, also produce a $print cell.

Note

Help text automatically generated from passes/cmds/chformal.cc:74

clk2fflogic - convert clocked FFs to generic $ff cells¶

yosys> help clk2fflogic¶

clk2fflogic [options] [selection]¶

This command replaces clocked flip-flops with generic $ff cells that use the
implicit global clock. This is useful for formal verification of designs with
multiple clocks.

This pass assumes negative hold time for the async FF inputs. For example when
a reset deasserts with the clock edge, then the FF output will still drive the
reset value in the next cycle regardless of the data-in value at the time of
the clock edge.

-nolower

Do not automatically run 'chformal -lower' to lower $check cells.

-nopeepopt

Do not automatically run 'peepopt -formalclk' to rewrite clock patterns
to more formal friendly forms.

Note

Help text automatically generated from passes/sat/clk2fflogic.cc:36

cutpoint - adds formal cut points to the design¶

yosys> help cutpoint¶

cutpoint [options] [selection]¶

This command adds formal cut points to the design.

-undef

set cutpoint nets to undef (x). the default behavior is to create
an $anyseq cell and drive the cutpoint net from that

-noscopeinfo

do not create '$scopeinfo' cells that preserve attributes of cells that
were removed by this pass

cutpoint -blackbox [options]

Replace all instances of blackboxes in the design with a formal cut point.

Note

Help text automatically generated from passes/sat/cutpoint.cc:28

dft_tag - create tagging logic for data flow tracking¶

yosys> help dft_tag¶

dft_tag [options] [selection]¶

This pass... TODO

-overwrite-only

Only process $overwrite_tag and $original_tag cells.

-tag-public

For each public wire that may carry tagged data, create a new public
wire (named <wirename>:<tagname>) that carries the tag bits. Note
that without this, tagging logic will only be emitted as required
for uses of $get_tag.

Note

Help text automatically generated from passes/cmds/dft_tag.cc:957

fmcombine - combine two instances of a cell into one¶

yosys> help fmcombine¶

fmcombine [options] module_name gold_cell gate_cell¶

This pass takes two cells, which are instances of the same module, and replaces
them with one instance of a special 'combined' module, that effectively
contains two copies of the original module, plus some formal properties.

This is useful for formal test benches that check what differences in behavior
a slight difference in input causes in a module.

-initeq

Insert assumptions that initially all FFs in both circuits have the
same initial values.

-anyeq

Do not duplicate $anyseq/$anyconst cells.

-fwd

Insert forward hint assumptions into the combined module.

-bwd

Insert backward hint assumptions into the combined module.
(Backward hints are logically equivalend to fordward hits, but
some solvers are faster with bwd hints, or even both -bwd and -fwd.)

-nop

Don't insert hint assumptions into the combined module.
(This should not provide any speedup over the original design, but
strangely sometimes it does.)

If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.

Note

Help text automatically generated from passes/sat/fmcombine.cc:240

fminit - set init values/sequences for formal¶

yosys> help fminit¶

fminit [options] <selection>¶

This pass creates init constraints (for example for reset sequences) in a formal
model.

-seq <signal> <sequence>

Set sequence using comma-separated list of values, use 'z for
unconstrained bits. The last value is used for the remainder of the
trace.

-set <signal> <value>

Add constant value constraint

-posedge <signal>

-negedge <signal>

Set clock for init sequences

Note

Help text automatically generated from passes/sat/fminit.cc:28

formalff - prepare FFs for formal¶

yosys> help formalff¶

formalff [options] [selection]¶

This pass transforms clocked flip-flops to prepare a design for formal
verification. If a design contains latches and/or multiple different clocks run
the async2sync or clk2fflogic passes before using this pass.

-clk2ff

Replace all clocked flip-flops with $ff cells that use the implicit
global clock. This assumes, without checking, that the design uses a
single global clock. If that is not the case, the clk2fflogic pass
should be used instead.

-ff2anyinit

Replace uninitialized bits of $ff cells with $anyinit cells. An
$anyinit cell behaves exactly like an $ff cell with an undefined
initialization value. The difference is that $anyinit inhibits
don't-care optimizations and is used to track solver-provided values
in witness traces.

If combined with -clk2ff this also affects newly created $ff cells.

-anyinit2ff

Replaces $anyinit cells with uninitialized $ff cells. This performs the
reverse of -ff2anyinit and can be used, before running a backend pass
(or similar) that is not yet aware of $anyinit cells.

Note that after running -anyinit2ff, in general, performing don't-care
optimizations is not sound in a formal verification setting.

-fine

Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for

-anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.

-setundef

Find FFs with undefined initialization values for which changing the
initialization does not change the observable behavior and initialize
them. For -ff2anyinit, this reduces the number of generated $anyinit
cells that drive wires with private names.

-hierarchy

Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards
through the design hierarchy towards the toplevel inputs. This option
works on the whole design and ignores the selection.

-assume

Add assumptions that constrain wires with the 'replaced_by_gclk'
attribute to the value they would have before an active clock edge.

-declockgate

Detect clock-gating patterns and modify any FFs clocked by the gated
clock to use the ungated clock with the gate signal as clock enable.
This doesn't affect the design's behavior during FV but can enable the
use of formal verification methods that only support a single global
clock.

Note

Help text automatically generated from passes/sat/formalff.cc:489

freduce - perform functional reduction¶

yosys> help freduce¶

freduce [options] [selection]¶

This pass performs functional reduction in the circuit. I.e. if two nodes are
equivalent, they are merged to one node and one of the redundant drivers is
disconnected. A subsequent call to 'clean' will remove the redundant drivers.

-v, -vv

enable verbose or very verbose output

-inv

enable explicit handling of inverted signals

-stop <n>

stop after <n> reduction operations. this is mostly used for
debugging the freduce command itself.

-dump <prefix>

dump the design to <prefix>_<module>_<num>.il after each reduction
operation. this is mostly used for debugging the freduce command.

This pass is undef-aware, i.e. it considers don't-care values for detecting
equivalent nodes.

All selected wires are considered for rewiring. The selected cells cover the
circuit that is analyzed.

Note

Help text automatically generated from passes/sat/freduce.cc:758

future - resolve future sampled value functions¶

yosys> help future¶

future [options] [selection]¶

Note

Help text automatically generated from passes/cmds/future.cc:113

glift - create GLIFT models and optimization problems¶

yosys> help glift¶

glift <command> [options] [selection]¶

Augments the current or specified module with gate-level information flow
tracking (GLIFT) logic using the "constructive mapping" approach. Also can set
up QBF-SAT optimization problems in order to optimize GLIFT models or trade off
precision and complexity.

Commands:

-create-precise-model

Replaces the current or specified module with one that has corresponding
"taint" inputs, outputs, and internal nets along with precise taint
tracking logic. For example, precise taint tracking logic for an AND gate
is:

y_t = a & b_t | b & a_t | a_t & b_t

-create-imprecise-model

Replaces the current or specified module with one that has corresponding
"taint" inputs, outputs, and internal nets along with imprecise "All OR"
taint tracking logic:

y_t = a_t | b_t

-create-instrumented-model

Replaces the current or specified module with one that has corresponding
"taint" inputs, outputs, and internal nets along with 4 varying-precision
versions of taint tracking logic. Which version of taint tracking logic is
used for a given gate is determined by a MUX selected by an $anyconst cell.
By default, unless the `-no-cost-model` option is provided, an additional
wire named `__glift_weight` with the `keep` and `minimize` attributes is
added to the module along with pmuxes and adders to calculate a rough
estimate of the number of logic gates in the GLIFT model given an assignment
for the $anyconst cells. The four versions of taint tracking logic for an
AND gate are:
y_t = a & b_t | b & a_t | a_t & b_t       (like `-create-precise-model`)
y_t = a_t | a & b_t
y_t = b_t | b & a_t
y_t = a_t | b_t                           (like `-create-imprecise-model`)

Options:

-taint-constants

Constant values in the design are labeled as tainted.
(default: label constants as un-tainted)

-keep-outputs

Do not remove module outputs. Taint tracking outputs will appear in the
module ports alongside the orignal outputs.
(default: original module outputs are removed)

-simple-cost-model

Do not model logic area. Instead model the number of non-zero assignments to
$anyconsts. Taint tracking logic versions vary in their size, but all
reduced-precision versions are significantly smaller than the fully-precise
version. A non-zero $anyconst assignment means that reduced-precision taint
tracking logic was chosen for some gate. Only applicable in combination with
`-create-instrumented-model`. (default: use a complex model and give that
wire the "keep" and "minimize" attributes)

-no-cost-model

Do not model taint tracking logic area and do not create a `__glift_weight`
wire. Only applicable in combination with `-create-instrumented-model`.
(default: model area and give that wire the "keep" and "minimize"
attributes)

-instrument-more

Allow choice from more versions of (even simpler) taint tracking logic. A
total of 8 versions of taint tracking logic will be added per gate,
including the 4 versions from `-create-instrumented-model` and these
additional versions:

y_t = a_t
y_t = b_t
y_t = 1
y_t = 0

Only applicable in combination with `-create-instrumented-model`.
(default: do not add more versions of taint tracking logic.

Note

Help text automatically generated from passes/cmds/glift.cc:425

miter - automatically create a miter circuit¶

yosys> help miter¶

miter -equiv [options] gold_name gate_name miter_name¶

Creates a miter circuit for equivalence checking. The gold- and gate- modules
must have the same interfaces. The miter circuit will have all inputs of the
two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'
output that goes high if an output mismatch between the two source modules is
detected.

-ignore_gold_x

a undef (x) bit in the gold module output will match any value in
the gate module output.

-make_outputs

also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs
on the miter circuit.

-make_outcmp

also create a cmp_* output for each gold/gate output pair.

-make_assert

also create an 'assert' cell that checks if trigger is always low.

-make_cover

also create a 'cover' cell for each gold/gate output pair.

-flatten

call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.

-cross

allow output ports on the gold module to match input ports on the
gate module. This is useful when the gold module contains additional
logic to drive some of the gate module inputs.

miter -assert [options] module [miter_name]¶

Creates a miter circuit for property checking. All input ports are kept,
output ports are discarded. An additional output 'trigger' is created that
goes high when an assert is violated. Without a miter_name, the existing
module is modified.

-make_outputs

keep module output ports.

-flatten

call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.

Note

Help text automatically generated from passes/sat/miter.cc:396

mutate - generate or apply design mutations¶

yosys> help mutate¶

mutate -list N [options] [selection]¶

Create a list of N mutations using an even sampling.

-o filename

Write list to this file instead of console output

-s filename

Write a list of all src tags found in the design to the specified file

-seed N

RNG seed for selecting mutations

-none

Include a "none" mutation in the output

-ctrl name width value

Add -ctrl options to the output. Use 'value' for first mutation, then
simply count up from there.

-mode name

-module name

-cell name

-port name

-portbit int

-ctrlbit int

-wire name

-wirebit int

-src string

Filter list of mutation candidates to those matching
the given parameters.

-cfg option int

Set a configuration option. Options available:
weight_pq_w weight_pq_b weight_pq_c weight_pq_s
weight_pq_mw weight_pq_mb weight_pq_mc weight_pq_ms
weight_cover pick_cover_prcnt

mutate -mode MODE [options]¶

Apply the given mutation.

-ctrl name width value

Add a control signal with the given name and width. The mutation is
activated if the control signal equals the given value.

-module name

-cell name

-port name

-portbit int

-ctrlbit int

Mutation parameters, as generated by 'mutate -list N'.

-wire name

-wirebit int

-src string

Ignored. (They are generated by -list for documentation purposes.)

Note

Help text automatically generated from passes/sat/mutate.cc:731

qbfsat - solve a 2QBF-SAT problem in the circuit¶

yosys> help qbfsat¶

qbfsat [options] [selection]¶

This command solves an "exists-forall" 2QBF-SAT problem defined over the
currently selected module. Existentially-quantified variables are declared by
assigning a wire "$anyconst". Universally-quantified variables may be
explicitly declared by assigning a wire "$allconst", but module inputs will be
treated as universally-quantified variables by default.

-nocleanup

Do not delete temporary files and directories. Useful for debugging.

-dump-final-smt2 <file>

Pass the --dump-smt2 option to yosys-smtbmc.

-assume-outputs

Add an "$assume" cell for the conjunction of all one-bit module output
wires.

-assume-negative-polarity

When adding $assume cells for one-bit module output wires, assume they
are negative polarity signals and should always be low, for example like
the miters created with the `miter` command.

-nooptimize

Ignore "\minimize" and "\maximize" attributes, do not emit
"(maximize)" or "(minimize)" in the SMT-LIBv2, and generally make no
attempt to optimize anything.

-nobisection

If a wire is marked with the "\minimize" or "\maximize" attribute,
do not attempt to optimize that value with the default iterated solving
and threshold bisection approach. Instead, have yosys-smtbmc emit a
"(minimize)" or "(maximize)" command in the SMT-LIBv2 output and
hope that the solver supports optimizing quantified bitvector problems.

-solver <solver>

Use a particular solver. Choose one of: "z3", "yices", "cvc4"
and "cvc5". (default: yices)

-solver-option <name> <value>

Set the specified solver option in the SMT-LIBv2 problem file.

-timeout <value>

Set the per-iteration timeout in seconds.
(default: no timeout)

-O0, -O1, -O2

Control the use of ABC to simplify the QBF-SAT problem before solving.

-sat

Generate an error if the solver does not return "sat".

-unsat

Generate an error if the solver does not return "unsat".

-show-smtbmc

Print the output from yosys-smtbmc.

-specialize

If the problem is satisfiable, replace each "$anyconst" cell with its
corresponding constant value from the model produced by the solver.

-specialize-from-file <solution file>

Do not run the solver, but instead only attempt to replace each
"$anyconst" cell in the current module with a constant value provided
by the specified file.

-write-solution <solution file>

If the problem is satisfiable, write the corresponding constant value
for each "$anyconst" cell from the model produced by the solver to the
specified file.

Note

Help text automatically generated from passes/sat/qbfsat.cc:507

sat - solve a SAT problem in the circuit¶

yosys> help sat¶

sat [options] [selection]¶

This command solves a SAT problem defined over the currently selected circuit
and additional constraints passed as parameters.

-all

show all solutions to the problem (this can grow exponentially, use

-max <N> instead to get <N> solutions)

-max <N>

like -all, but limit number of solutions to <N>

-enable_undef

enable modeling of undef value (aka 'x-bits')
this option is implied by -set-def, -set-undef et. cetera

-max_undef

maximize the number of undef bits in solutions, giving a better
picture of which input bits are actually vital to the solution.

-set <signal> <value>

set the specified signal to the specified value.

-set-def <signal>

add a constraint that all bits of the given signal must be defined

-set-any-undef <signal>

add a constraint that at least one bit of the given signal is undefined

-set-all-undef <signal>

add a constraint that all bits of the given signal are undefined

-set-def-inputs

add -set-def constraints for all module inputs

-set-def-formal

add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells

-show <signal>

show the model for the specified signal. if no -show option is
passed then a set of signals to be shown is automatically selected.

-show-inputs, -show-outputs, -show-ports

add all module (input/output) ports to the list of shown signals

-show-regs, -show-public, -show-all

show all registers, show signals with 'public' names, show all signals

-ignore_div_by_zero

ignore all solutions that involve a division by zero

-ignore_unknown_cells

ignore all cells that can not be matched to a SAT model

The following options can be used to set up a sequential problem:

-seq <N>

set up a sequential problem with <N> time steps. The steps will
be numbered from 1 to N.

note: for large <N> it can be significantly faster to use

-tempinduct-baseonly -maxsteps <N> instead of -seq <N>.

-set-at <N> <signal> <value>

-unset-at <N> <signal>

set or unset the specified signal to the specified value in the
given timestep. this has priority over a -set for the same signal.

-set-assumes

set all assumptions provided via $assume cells

-set-def-at <N> <signal>

-set-any-undef-at <N> <signal>

-set-all-undef-at <N> <signal>

add undef constraints in the given timestep.

-set-init <signal> <value>

set the initial value for the register driving the signal to the value

-set-init-undef

set all initial states (not set using -set-init) to undef

-set-init-def

do not force a value for the initial state but do not allow undef

-set-init-zero

set all initial states (not set using -set-init) to zero

-dump_vcd <vcd-file-name>

dump SAT model (counter example in proof) to VCD file

-dump_json <json-file-name>

dump SAT model (counter example in proof) to a WaveJSON file.

-dump_cnf <cnf-file-name>

dump CNF of SAT problem (in DIMACS format). in temporal induction
proofs this is the CNF of the first induction step.

The following additional options can be used to set up a proof. If also -seq
is passed, a temporal induction proof is performed.

-tempinduct

Perform a temporal induction proof. In a temporal induction proof it is
proven that the condition holds forever after the number of time steps
specified using -seq.

-tempinduct-def

Perform a temporal induction proof. Assume an initial state with all
registers set to defined values for the induction step.

-tempinduct-baseonly

Run only the basecase half of temporal induction (requires -maxsteps)

-tempinduct-inductonly

Run only the induction half of temporal induction

-tempinduct-skip <N>

Skip the first <N> steps of the induction proof.

note: this will assume that the base case holds for <N> steps.
this must be proven independently with "-tempinduct-baseonly

-maxsteps <N>". Use -initsteps if you just want to set a

minimal induction length.

-prove <signal> <value>

Attempt to proof that <signal> is always <value>.

-prove-x <signal> <value>

Like -prove, but an undef (x) bit in the lhs matches any value on
the right hand side. Useful for equivalence checking.

-prove-asserts

Prove that all asserts in the design hold.

-prove-skip <N>

Do not enforce the prove-condition for the first <N> time steps.

-maxsteps <N>

Set a maximum length for the induction.

-initsteps <N>

Set initial length for the induction.
This will speed up the search of the right induction length
for deep induction proofs.

-stepsize <N>

Increase the size of the induction proof in steps of <N>.
This will speed up the search of the right induction length
for deep induction proofs.

-timeout <N>

Maximum number of seconds a single SAT instance may take.

-verify

Return an error and stop the synthesis script if the proof fails.

-verify-no-timeout

Like -verify but do not return an error for timeouts.

-falsify

Return an error and stop the synthesis script if the proof succeeds.

-falsify-no-timeout

Like -falsify but do not return an error for timeouts.

Note

Help text automatically generated from passes/sat/sat.cc:906

supercover - add hi/lo cover cells for each wire bit¶

yosys> help supercover¶

supercover [options] [selection]¶

This command adds two cover cells for each bit of each selected wire, one
checking for a hi signal level and one checking for lo level.

Note

Help text automatically generated from passes/sat/supercover.cc:28

synthprop - synthesize SVA properties¶

yosys> help synthprop¶

synthprop [options]¶

This creates synthesizable properties for the selected module.

-name <portname>

name of the output port for assertions (default: assertions).

-map <filename>

write the port mapping for synthesizable properties into the given file.

-or_outputs

Or all outputs together to create a single output that goes high when
any property is violated, instead of generating individual output bits.

-reset <portname>

name of the top-level reset input. Latch a high state on the generated
outputs until an asynchronous top-level reset input is activated.

-resetn <portname>

like above but with inverse polarity

Note

Help text automatically generated from passes/sat/synthprop.cc:182

xprop - formal x propagation¶

yosys> help xprop¶

xprop [options] [selection]¶

This pass transforms the circuit into an equivalent circuit that explicitly
encodes the propagation of x values using purely 2-valued logic. On the
interface between xprop-transformed and non-transformed parts of the design,
appropriate conversions are inserted automatically.

-split-inputs

-split-outputs

-split-ports

Replace each input/output/port with two new ports, one carrying the
defined values (named <portname>_d) and one carrying the mask of which
bits are x (named <portname>_x). When a bit in the <portname>_x is set
the corresponding bit in <portname>_d is ignored for inputs and
guaranteed to be 0 for outputs.

-split-public

Replace each public non-port wire with two new wires, one carrying the
defined values (named <wirename>_d) and one carrying the mask of which
bits are x (named <wirename>_x). When a bit in the <portname>_x is set
the corresponding bit in <wirename>_d is guaranteed to be 0 for
outputs.

-assume-encoding

Add encoding invariants as assumptions. This can speed up formal
verification tasks.

-assert-encoding

Add encoding invariants as assertions. Used for testing the xprop
pass itself.

-assume-def-inputs

Assume all inputs are fully defined. This adds corresponding
assumptions to the design and uses these assumptions to optimize the
xprop encoding.

-required

Produce a runtime error if any encountered cell could not be encoded.

-formal

Produce a runtime error if any encoded cell uses a signal that is

neither known to be non-x nor driven by another encoded cell.

-debug-asserts

Add assertions checking that the encoding used by this pass never
produces x values within the encoded signals.

Note

Help text automatically generated from passes/cmds/xprop.cc:1103