Equivalence checking¶

equiv_add - add a $equiv cell¶

yosys> help equiv_add¶

equiv_add [-try] gold_sig gate_sig¶

This command adds an $equiv cell for the specified signals.

equiv_add [-try] -cell gold_cell gate_cell¶

This command adds $equiv cells for the ports of the specified cells.

Note

Help text automatically generated from passes/equiv/equiv_add.cc:27

equiv_induct - proving $equiv cells using temporal induction¶

yosys> help equiv_induct¶

equiv_induct [options] [selection]¶

Uses a version of temporal induction to prove $equiv cells.

Only selected $equiv cells are proven and only selected cells are used to
perform the proof.

-undef

enable modelling of undef states

-seq <N>

the max. number of time steps to be considered (default = 4)

-set-assumes

set all assumptions provided via $assume cells

This command is very effective in proving complex sequential circuits, when
the internal state of the circuit quickly propagates to $equiv cells.

However, this command uses a weak definition of 'equivalence': This command
proves that the two circuits will not diverge after they produce equal
outputs (observable points via $equiv) for at least <N> cycles (the <N>
specified via -seq).

Combined with simulation this is very powerful because simulation can give
you confidence that the circuits start out synced for at least <N> cycles
after reset.

Note

Help text automatically generated from passes/equiv/equiv_induct.cc:180

equiv_make - prepare a circuit for equivalence checking¶

yosys> help equiv_make¶

equiv_make [options] gold_module gate_module equiv_module¶

This creates a module annotated with $equiv cells from two presumably
equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'
to work with the created equivalent checking module.

-inames

Also match cells and wires with $... names.

-blacklist <file>

Do not match cells or signals that match the names in the file.

-encfile <file>

Match FSM encodings using the description from the file.
See 'help fsm_recode' for details.

-make_assert

Check equivalence with $assert cells instead of $equiv.
$eqx (===) is used to compare signals.

Note: The circuit created by this command is not a miter (with something like
a trigger output), but instead uses $equiv cells to encode the equivalence
checking problem. Use 'miter -equiv' if you want to create a miter circuit.

Note

Help text automatically generated from passes/equiv/equiv_make.cc:428

equiv_mark - mark equivalence checking regions¶

yosys> help equiv_mark¶

equiv_mark [options] [selection]¶

This command marks the regions in an equivalence checking module. Region 0 is
the proven part of the circuit. Regions with higher numbers are connected
unproven subcricuits. The integer attribute 'equiv_region' is set on all
wires and cells.

Note

Help text automatically generated from passes/equiv/equiv_mark.cc:206

equiv_miter - extract miter from equiv circuit¶

yosys> help equiv_miter¶

equiv_miter [options] miter_module [selection]¶

This creates a miter module for further analysis of the selected $equiv cells.

-trigger

Create a trigger output

-cmp

Create cmp_* outputs for individual unproven $equiv cells

-assert

Create a $assert cell for each unproven $equiv cell

-undef

Create compare logic that handles undefs correctly

Note

Help text automatically generated from passes/equiv/equiv_miter.cc:263

equiv_opt - prove equivalence for optimized circuit¶

yosys> help equiv_opt¶

equiv_opt [options] [command]¶

This command uses temporal induction to check circuit equivalence before and
after an optimization pass.

-run <from_label>:<to_label>

only run the commands between the labels (see below). an empty
from label is synonymous to the start of the command list, and empty to
label is synonymous to the end of the command list.

-map <filename>

expand the modules in this file before proving equivalence. this is
useful for handling architecture-specific primitives.

-blacklist <file>

Do not match cells or signals that match the names in the file
(passed to equiv_make).

-assert

produce an error if the circuits are not equivalent.

-multiclock

run clk2fflogic before equivalence checking.

-async2sync

run async2sync before equivalence checking.

-undef

enable modelling of undef states during equiv_induct.

-nocheck

disable running check before and after the command under test.

The following commands are executed by this verification command:

    run_pass:
        hierarchy -auto-top
        design -save preopt
        check -assert    (unless -nocheck)
        [command]
        check -assert    (unless -nocheck)
        design -stash postopt

    prepare:
        design -copy-from preopt  -as gold A:top
        design -copy-from postopt -as gate A:top

    techmap:    (only with -map)
        techmap -wb -D EQUIV -autoproc -map <filename> ...

    prove:
        clk2fflogic    (only with -multiclock)
        async2sync     (only with -async2sync)
        equiv_make -blacklist <filename> ... gold gate equiv
        equiv_induct [-undef] equiv
        equiv_status [-assert] equiv

    restore:
        design -load preopt

Note

Help text automatically generated from passes/equiv/equiv_opt.cc:27

equiv_purge - purge equivalence checking module¶

yosys> help equiv_purge¶

equiv_purge [options] [selection]¶

This command removes the proven part of an equivalence checking module, leaving
only the unproven segments in the design. This will also remove and add module
ports as needed.

Note

Help text automatically generated from passes/equiv/equiv_purge.cc:178

equiv_remove - remove $equiv cells¶

yosys> help equiv_remove¶

equiv_remove [options] [selection]¶

This command removes the selected $equiv cells. If neither -gold nor -gate is
used then only proven cells are removed.

-gold

keep gold circuit

-gate

keep gate circuit

Note

Help text automatically generated from passes/equiv/equiv_remove.cc:26

equiv_simple - try proving simple $equiv instances¶

yosys> help equiv_simple¶

equiv_simple [options] [selection]¶

This command tries to prove $equiv cells using a simple direct SAT approach.

-v

verbose output

-undef

enable modelling of undef states

-short

create shorter input cones that stop at shared nodes. This yields
simpler SAT problems but sometimes fails to prove equivalence.

-nogroup

disabling grouping of $equiv cells by output wire

-seq <N>

the max. number of time steps to be considered (default = 1)

-set-assumes

set all assumptions provided via $assume cells

Note

Help text automatically generated from passes/equiv/equiv_simple.cc:408

equiv_status - print status of equivalent checking module¶

yosys> help equiv_status¶

equiv_status [options] [selection]¶

This command prints status information for all selected $equiv cells.

-assert

produce an error if any unproven $equiv cell is found

Note

Help text automatically generated from passes/equiv/equiv_status.cc:26

equiv_struct - structural equivalence checking¶

yosys> help equiv_struct¶

equiv_struct [options] [selection]¶

This command adds additional $equiv cells based on the assumption that the
gold and gate circuit are structurally equivalent. Note that this can introduce
bad $equiv cells in cases where the netlists are not structurally equivalent,
for example when analyzing circuits with cells with commutative inputs. This
command will also de-duplicate gates.

-fwd

by default this command performans forward sweeps until nothing can
be merged by forwards sweeps, then backward sweeps until forward
sweeps are effective again. with this option set only forward sweeps
are performed.

-fwonly <cell_type>

add the specified cell type to the list of cell types that are only
merged in forward sweeps and never in backward sweeps. $equiv is in
this list automatically.

-icells

by default, the internal RTL and gate cell types are ignored. add
this option to also process those cell types with this command.

-maxiter <N>

maximum number of iterations to run before aborting

Note

Help text automatically generated from passes/equiv/equiv_struct.cc:285