 
   July 1, 1994                                                        SIS(1)
 
   env_verify_fsm [-v n] [-V] fsm.blif env.blif
 
     Verify the equivalence of two synchronous networks in a given environ-
     ment. The current network is compared with fsm.blif under the environ-
     ment defined by the env.blif 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 fsm.blif network are substituable for one
     another when used in the context of the env.blif network.
 
     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.
 
     -v allows specification of the verbosity level of the output.
 
     By default, the command returns an error status if the verification
     fails.  When option -V is used, it returns an error status if the verif-
     ication succeeds.
 
                                                                            1
