.\" /*
.\"  * Revision Control Information
.\"  *
.\"  * $Source: /vol/opua/opua2/sis/sis-1.1/common/src/sis/sis_lib/help/RCS/verify_fsm.1,v $
.\"  * $Author: sis $
.\"  * $Revision: 1.2 $
.\"  * $Date: 1992/05/06 19:04:01 $
.\"  *
.\"
.XX
verify_fsm [-o depth] [-v n] [-m method] filename.blif
.PP
Verify the equivalence of two synchronous networks.
The current network is compared with \fBfilename.blif\fR.
The input and output variables from the two networks are
associated by their names.
It is assumed that all the latches in both designs are clocked
by a single, global clock.
The verification is done by implicitly enumerating all the
states in the product machine, and checking that the outputs
are equivalent for all reachable state pairs starting
from the initial state of the product machine.
.PP
\fB-o depth\fR allows the specification of the depth of search for a good
variable ordering.
A larger value for depth will require more CPU time but determine
a better ordering.
The default value is 2.
.PP
\fB-v\fR allows specification of the verbosity level of the output.
.PP
The \fB-m\fR option specifies \fBmethod\fR for determining
the reachable states.
\fBconsistency\fR builds the entire transition relation
and uses it to determine the reached states.
\fBbull\fR does output cofactoring to find the reachable
states.
The \fBproduct\fR method is similar to the \fBconsistency\fR method but
input variables are smoothed as soon as possible as the characteristic
function is being built.
This makes the size of the resulting BDD representing the
characteristic function of the transition relation smaller.
The default method is \fBproduct\fR.
