equiv_opt - prove equivalence for optimized circuit

    equiv_opt [options] [command]

This command checks 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.

    -assert
        produce an error if the circuits are not equivalent.

    -undef
        enable modelling of undef states during equiv_induct.

The following commands are executed by this verification command:

    run_pass:
        hierarchy -auto-top
        design -save preopt
        [command]
        design -stash postopt

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

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

    prove:
        equiv_make gold gate equiv
        equiv_induct [-undef] equiv
        equiv_status [-assert] equiv

    restore:
        design -load preopt