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