equiv_opt - prove equivalence for optimized circuit
equiv_opt [options] [command]
This command checks circuit equivalence before and after an optimization pass.
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.
expand the modules in this file before proving equivalence. this is
useful for handling architecture-specific primitives.
produce an error if the circuits are not equivalent.
enable modelling of undef states during equiv_induct.
The following commands are executed by this verification command:
design -save preopt
design -stash postopt
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> ...
equiv_make gold gate equiv
equiv_induct [-undef] equiv
equiv_status [-assert] equiv
design -load preopt