[14] | 1 | |
---|
| 2 | comb_verify - verify the combinational equivalence of two flattened networks |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | comb_verify [-b] [-f <filename>] [-h] [-o <ordering method>] [-t <timeOut>] |
---|
| 6 | [-1 <partition method>] [-2 <partition method>] [-i] <filename1> |
---|
| 7 | [<filename2>] |
---|
| 8 | |
---|
| 9 | This command verifies the combinational equivalence of two flattened |
---|
| 10 | networks. In particular, any set of functions (the roots), defined over any |
---|
| 11 | set of intermediate variables (the leaves), can be checked for equivalence |
---|
| 12 | between the two networks. Roots and leaves are subsets of the nodes of a |
---|
| 13 | network, with the restriction that the leaves should form a complete support |
---|
| 14 | for the roots. The correspondence between the roots and the leaves in the |
---|
| 15 | two networks is specified in a file given by the option -f . The default |
---|
| 16 | option assumes that the roots are the combinational outputs and the leaves |
---|
| 17 | are the combinational inputs. |
---|
| 18 | |
---|
| 19 | When there is a pseudo input in the set of leaves, the range of values it |
---|
| 20 | can take should be the same as that of the multi-valued variable |
---|
| 21 | corresponding to it, for comb_verify to function correctly. This restriction |
---|
| 22 | will be removed in future. |
---|
| 23 | |
---|
| 24 | There are two ways to do combinational verification. In the first mode, two |
---|
| 25 | BLIF-MV files are given as arguments to the command, e.g. |
---|
| 26 | |
---|
| 27 | vis> comb_verify foo.mv bar.mv |
---|
| 28 | |
---|
| 29 | |
---|
| 30 | Verification is done for the flattened networks at the root nodes of the two |
---|
| 31 | BLIF-MV hierarchies. In any error messages printed, "network1" refers to the |
---|
| 32 | first file, and "network2" refers to the second. Both of these networks are |
---|
| 33 | freed at the end of the command. This mode is totally independent from any |
---|
| 34 | existing hierarchy previously read in. In the second mode, it is assumed |
---|
| 35 | that a hierarchy has already been read in. Then, comb_verify can be called |
---|
| 36 | with a single BLIF-MV file, and this will do the comparison between the |
---|
| 37 | network present at the current node ("network1") and the network |
---|
| 38 | corresponding to the root node of the hierarchy in the BLIF-MV |
---|
| 39 | file("network2"). A typical sequence of commands is: |
---|
| 40 | |
---|
| 41 | vis> read_blifmv foo.mv |
---|
| 42 | vis> init_verify |
---|
| 43 | vis> comb_verify bar.mv |
---|
| 44 | |
---|
| 45 | |
---|
| 46 | If a hierarchy has been read in but a flattened network does not exist at |
---|
| 47 | the current node (flatten_hierarchy has not been invoked), the command does |
---|
| 48 | nothing. If a network exists at the current node, but the variables haven't |
---|
| 49 | been ordered, then the variables are ordered and a partition created. This |
---|
| 50 | partition is freed at the end. A side-effect is that the variables are |
---|
| 51 | ordered. If a partition exists, then it is used if the vertices |
---|
| 52 | corresponding to the roots specified are present in it, otherwise a new |
---|
| 53 | partition is created with the current ordering. The partition created for |
---|
| 54 | the new network read in is always freed at the end. |
---|
| 55 | |
---|
| 56 | Command options: |
---|
| 57 | |
---|
| 58 | -b |
---|
| 59 | Specifies that the files are BLIF files and not BLIF-MV files. |
---|
| 60 | |
---|
| 61 | -f <filename> |
---|
| 62 | Provides the correspondence between the leaves and roots of network1 |
---|
| 63 | and network2. If this option is not used, it is assumed that the |
---|
| 64 | correspondence is by name, except that two latch inputs match if |
---|
| 65 | either they have the same name or the corresponding latch outputs |
---|
| 66 | have the same name. Leaves are the combinational inputs, and roots |
---|
| 67 | are the combinational outputs. |
---|
| 68 | |
---|
| 69 | -h |
---|
| 70 | Print the command usage. |
---|
| 71 | |
---|
| 72 | -t <timeOut> |
---|
| 73 | Time in seconds allowed to perform equivalence checking. The default |
---|
| 74 | is infinity. |
---|
| 75 | |
---|
| 76 | -o <ordering method> |
---|
| 77 | Specifies the ordering method to be used for assigning a common |
---|
| 78 | ordering to the leaves of network1 and network2. If this option is |
---|
| 79 | not used, ordering is done using a default method. Currently, only |
---|
| 80 | the default method is available. |
---|
| 81 | |
---|
| 82 | -1 <partition method> |
---|
| 83 | Specifies the partitioning method to be used for network1. Supported |
---|
| 84 | methods are "total", "partial", and "inout" (see the command |
---|
| 85 | build_partition_mdds for more information). If this option is not |
---|
| 86 | specified, then the default method "inout" is used. |
---|
| 87 | |
---|
| 88 | -2 <partition method> |
---|
| 89 | Specifies the partitioning method to be used for network2. Supported |
---|
| 90 | methods are "total", "partial", and "inout" (see the command |
---|
| 91 | build_partition_mdds for more information). If this option is not |
---|
| 92 | specified, then default method "inout" is used. |
---|
| 93 | |
---|
| 94 | -i |
---|
| 95 | Print Bdd statistics. |
---|
| 96 | _________________________________________________________________ |
---|
| 97 | |
---|
| 98 | Last updated on 20100410 00h02 |
---|