.\" /*
.\"  * 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
env_verify_fsm [-v n] [-V] fsm.blif env.blif
.PP
Verify the equivalence of two synchronous networks in a given environment. 
The current network is compared with \fBfsm.blif\fR under the
environment defined by the \fBenv.blif\fR network. 
The environment is a sequential circuit that generates the inputs of
the circuits under verification, and possibly takes some inputs from
them. What is verified is that the current network and the
\fBfsm.blif\fR network are substituable for one another when used in
the context of the \fBenv.blif\fR network.
.PP
The input and output variables from the three networks are
matched by 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-v\fR allows specification of the verbosity level of the output.
.PP
By default, the command returns an error status if the verification fails.
When option \fB-V\fR is used, it returns an error status if the verification succeeds.
