[14] | 1 | |
---|
| 2 | seq_verify - verify the sequential equivalence of two flattened networks |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | seq_verify [-b] [-f <filename>] [-h] [-p <partition method>] [-t <timeOut>] |
---|
| 6 | [-B] [-i] [-r] <filename> [<filename>] |
---|
| 7 | |
---|
| 8 | Please read the documentation for the command comb_verify before reading on. |
---|
| 9 | The concepts of roots and leaves in this command are the same as for |
---|
| 10 | comb_verify, except for an added constraint: the set of leaves has to be the |
---|
| 11 | set of all primary inputs. This obviously produces the constraint that both |
---|
| 12 | networks have the same number of primary inputs. Moreover, no pseudo inputs |
---|
| 13 | should be present in the two networks being compared. The set of roots can |
---|
| 14 | be an arbitrary subset of nodes. |
---|
| 15 | |
---|
| 16 | The command verifies whether any state, where the values of two |
---|
| 17 | corresponding roots differ, can be reached from the set of initial states of |
---|
| 18 | the product machine. If this happens, a debug trace is provided. |
---|
| 19 | |
---|
| 20 | The sequential verification is done by building the product finite state |
---|
| 21 | machine. |
---|
| 22 | |
---|
| 23 | The command has two execution modes, just as for comb_verify. In the first |
---|
| 24 | mode, two BLIF-MV files are given as arguments to the command: |
---|
| 25 | |
---|
| 26 | vis> seq_verify foo.mv bar.mv |
---|
| 27 | |
---|
| 28 | |
---|
| 29 | In the second mode, a single BLIF-MV file is taken. This is network2. It is |
---|
| 30 | assumed that network1 is from a hierarchy that has already been read in. If |
---|
| 31 | a network is present at the current node (i.e. flatten_hierarchy has been |
---|
| 32 | executed), it is used for verification; otherwise the command does nothing. |
---|
| 33 | |
---|
| 34 | vis> read_blifmv foo.mv |
---|
| 35 | vis> flatten_hierarchy |
---|
| 36 | vis> seq_verify bar.mv |
---|
| 37 | |
---|
| 38 | |
---|
| 39 | Command options: |
---|
| 40 | |
---|
| 41 | -b |
---|
| 42 | Specifies that the input files are BLIF files. |
---|
| 43 | |
---|
| 44 | -f <filename> |
---|
| 45 | Provides the correspondence between the leaves and roots of network1 |
---|
| 46 | and network2. leaves has to be the set of primary inputs of the |
---|
| 47 | networks. roots can be any subset of nodes. If this option is not |
---|
| 48 | used, it is assumed that the correspondence is by name, and that the |
---|
| 49 | roots are the combinational outputs. |
---|
| 50 | |
---|
| 51 | -h |
---|
| 52 | Print the command usage. |
---|
| 53 | |
---|
| 54 | -p <partition method> |
---|
| 55 | Specifies the partitioning method for the product machine. Supported |
---|
| 56 | methods are "total", "partial", and "inout" (see the command |
---|
| 57 | build_partition_mdds for more information). If this option is not |
---|
| 58 | specified, then the default method "inout" is used. |
---|
| 59 | |
---|
| 60 | -t <timeOut> |
---|
| 61 | Time in seconds allowed to perform equivalence checking. The default |
---|
| 62 | is infinity. |
---|
| 63 | |
---|
| 64 | -B |
---|
| 65 | Use backward image computation to traverse the state space of the |
---|
| 66 | product machine. By default, forward image computaion is used. |
---|
| 67 | |
---|
| 68 | -i |
---|
| 69 | Print BDD statistics. This is the only way to see BDD stastics during |
---|
| 70 | this command. print_bdd_stats after this command doesn't show |
---|
| 71 | information related to this command. |
---|
| 72 | |
---|
| 73 | -r |
---|
| 74 | Enable BDD reordering during the equivalence check. Note that |
---|
| 75 | dynamic_var_ordering has no effect on whether reordering is enabled |
---|
| 76 | during the execution of seq_verify. |
---|
| 77 | _________________________________________________________________ |
---|
| 78 | |
---|
| 79 | Last updated on 20100410 00h02 |
---|