Combinational verification : Two sets of distinguished nodes, roots and leaves, are specified for each network. The leaves should form a complete support for the roots in both networks. The correspondence between the roots and leaves of the two networks can be specified in an input file. The format of the input file is as follows-
.roots
<name1> <name2>
.
.
.leaves
<name1> <name2> .
.
Here, name1 is a node name in the first network and name2 a node name in the second network.
If no input file is given, the combinational outputs are assumed to be roots and the combinational inputs are assumed to be leaves. comb_verify checks for each pair of corresponding roots whether the two are equivalent as logical functions of corresponding leaf variables. This is done by constructing BDD's for the roots in terms of the leaf variables. For each pair in which the two roots are not equivalent, a minterm where they are not equal is written out. Note that pseudo inputs are treated no differently from any other inputs.
Sequential verification : Two inputs and an option for partitioning form the input for this command. A set of distinguished nodes called roots is specified for each network. The correspondence between the two sets can be specified in an input file as described above. If no input file is given, the primary outputs are assumed to be roots. seq_verify checks for each pair of corresponding roots whether the two roots have different values in a reachable state of the product machine of the networks for any input. For each pair that this happens, an error trace is written out.
The method used in sequential verification i.e. product machine cannot handle non-determinism. Therefore, the two networks shouldn't have any pseudo inputs.