[14] | 1 | |
---|
| 2 | res_verify - Verifies a combinational circuit using residue arithmetic. |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | res_verify [-b] [-d <n>] [-h] -i <filename> [-m <filename>] [-n <filename>] |
---|
| 6 | {-o <filename> | -O} [-s <filename>] [-t <timeOut>] |
---|
| 7 | |
---|
| 8 | This command performs residue verification between two networks. The method |
---|
| 9 | used is based on residue arithmetic and the Chinese Remainder theorem; it is |
---|
| 10 | described in [1] ftp://vlsi.colorado.edu/pub/fmcad96.ps. Verification is |
---|
| 11 | performed by interpreting the outputs of the circuits as integers and |
---|
| 12 | verifying the residues of the outputs with respect to a set of moduli. The |
---|
| 13 | choice of moduli is directed by the Chinese Remainder Theorem in order to |
---|
| 14 | prove equivalence of the two circuits. This method works well with |
---|
| 15 | multipliers and possibly other arithmetic circuits (due to its dependence on |
---|
| 16 | residue arithmetic). For the same reason, it is necessary to specify an |
---|
| 17 | output order which determines how the outputs are interpreted as integers. |
---|
| 18 | Discretion should be exercised in applying this method to general |
---|
| 19 | combinational circuits. |
---|
| 20 | |
---|
| 21 | Residue verification is available only if vis is linked with the cu BDD |
---|
| 22 | package. (This is the default.) It reads both blif and blif-mv files. |
---|
| 23 | However, it does NOT support multi-valued variables. Residue verification is |
---|
| 24 | primarily for combinational verification, but may be applied to sequential |
---|
| 25 | circuits with the same state encoding. The latch outputs are then considered |
---|
| 26 | to be combinational inputs of the circuits and the latch inputs and reset |
---|
| 27 | are considered to be combinational outputs of the circuits. |
---|
| 28 | |
---|
| 29 | There are two ways to perform residue verification in this package. As a |
---|
| 30 | first option, two files describing two networks, the specification and the |
---|
| 31 | implementation, (in the same format, blif or blif-mv, see option -b) are |
---|
| 32 | given in the command line; the procedure tries to verify the equivalence of |
---|
| 33 | the combinational outputs as functions of the combinational inputs. |
---|
| 34 | |
---|
| 35 | vis> res_verify -o network.order -i network1.blif -s network2.blif |
---|
| 36 | |
---|
| 37 | In this case both networks are read in, flattened and the verification is |
---|
| 38 | performed between the combinational outputs of both networks. The -i option |
---|
| 39 | denotes the implementation file and the -s option denotes the specification |
---|
| 40 | file. The -o option specifies the order of outputs for the circuits (See |
---|
| 41 | Command Options below for detailed explanation). |
---|
| 42 | |
---|
| 43 | A second way to perform the verification is as follows. The specification |
---|
| 44 | network is taken from a hierarchy already read into VIS. Then the res_verify |
---|
| 45 | command compares that specification against an implementation network |
---|
| 46 | obtained from the file in the command line. Any previous verification, |
---|
| 47 | performed with the specification, can be used towards the next verification |
---|
| 48 | task only if the same implementation circuit is being verified against and |
---|
| 49 | the same number of outputs have been directly verified with sucess in the |
---|
| 50 | previous attempt. The typical sequence of commands given to perform such |
---|
| 51 | task would be: |
---|
| 52 | |
---|
| 53 | vis> read_blifmv network1.mv |
---|
| 54 | vis> flatten_hierarchy |
---|
| 55 | vis> res_verify -o network.order -i network2.mv |
---|
| 56 | |
---|
| 57 | If the hierarchy has been read but no flattened network exists at the |
---|
| 58 | current node, the command will return without doing anything. If one of the |
---|
| 59 | networks used is the one in the current node in the hierarchy, then the |
---|
| 60 | information regarding the verification process will be stored in that |
---|
| 61 | network. |
---|
| 62 | |
---|
| 63 | Note: It is important to keep the specification distinct from the |
---|
| 64 | implementation because most parameters specified for the res_verify command |
---|
| 65 | are with respect to the specification. For example, the output order is |
---|
| 66 | specified with respect to the specification. The file that is read in first |
---|
| 67 | in the second format, is considered to be the specification. |
---|
| 68 | |
---|
| 69 | There is an option to directly verify some outputs by building the BDDs for |
---|
| 70 | the corresponding outputs of the 2 circuits. In that case, if the user wants |
---|
| 71 | to use an initial ordering, the only way to do it is the second method and |
---|
| 72 | reading in the network, one may specify the initial order using static |
---|
| 73 | order. |
---|
| 74 | |
---|
| 75 | The command does not repeat residue verification if the same |
---|
| 76 | specification-implementation pair have been verified with success and the |
---|
| 77 | same number of directly verified outputs have been verified in the previous |
---|
| 78 | attempt. |
---|
| 79 | |
---|
| 80 | Relevant flags to be set using the set command: |
---|
| 81 | |
---|
| 82 | residue_verbosity |
---|
| 83 | Default is 0, turns on verbosity to the desired level between 0 and |
---|
| 84 | 5. |
---|
| 85 | |
---|
| 86 | residue_ignore_direct_verified_outputs |
---|
| 87 | Default 0 (FALSE). If 1, then ignores directly verified outputs |
---|
| 88 | during residue verification. |
---|
| 89 | |
---|
| 90 | residue_top_var |
---|
| 91 | Default "msb". The 2 possible values are "msb" and lsb"; this puts |
---|
| 92 | the most/least significant bit near the top or bottom of the residue |
---|
| 93 | decision diagram. |
---|
| 94 | |
---|
| 95 | residue_autodyn_residue_verif |
---|
| 96 | Default 0 (FALSE). If 1, turns on dynamic reordering during residue |
---|
| 97 | verification. |
---|
| 98 | |
---|
| 99 | residue_residue_dyn_method |
---|
| 100 | Default "groupsift". Specifies the method for dynamic reordering |
---|
| 101 | during residue verification. Other methods supported are "same" (same |
---|
| 102 | as before), "none", "random", "randompivot", "sift", "siftconverge", |
---|
| 103 | "symmsiftconverge", "symmsift", "window2", "window3", "window4", |
---|
| 104 | "window2converge","window3converge","window4converge","groupsift", |
---|
| 105 | "groupsiftconverge", "anneal", "genetic", "linear", "linearconverge", |
---|
| 106 | "exact". |
---|
| 107 | |
---|
| 108 | residue_autodyn_direct_verif |
---|
| 109 | Default 0 (FALSE). If 1, turns on dynamic reordering during direct |
---|
| 110 | verification. |
---|
| 111 | |
---|
| 112 | residue_direct_dyn_method |
---|
| 113 | Default "groupsift". Specifies the method for dynamic reordering |
---|
| 114 | during direct verification. Other methods supported are "same" (same |
---|
| 115 | as before), "none", "random", "randompivot", "sift", "siftconverge", |
---|
| 116 | "symmsiftconverge", "symmsift", "window2", "window3", "window4", |
---|
| 117 | "window2converge","window3converge","window4converge","groupsift", |
---|
| 118 | "groupsiftconverge", "anneal", "genetic", "linear", "linearconverge", |
---|
| 119 | "exact". |
---|
| 120 | |
---|
| 121 | residue_layer_schedule |
---|
| 122 | Default "alap". This is a flag to specify the layering strategy of |
---|
| 123 | the networks. The 2 options are "asap" (as soon as possible) and |
---|
| 124 | "alap" (as late as possible). |
---|
| 125 | |
---|
| 126 | residue_layer_size |
---|
| 127 | Default largest layer size in network. Specifies the maximum layer |
---|
| 128 | size that can be composed in (relevant for vector composition only). |
---|
| 129 | |
---|
| 130 | residue_composition_method |
---|
| 131 | Default "vector". Specifies the composition method to be used in |
---|
| 132 | composing the network into the residue ADD. The options are "vector", |
---|
| 133 | "onegate", "preimage" and "superG". |
---|
| 134 | |
---|
| 135 | Command Options: |
---|
| 136 | |
---|
| 137 | -b |
---|
| 138 | If this option is specified, the specification and the implementation |
---|
| 139 | files read are considered to be in blif-mv format. Default is blif |
---|
| 140 | format. |
---|
| 141 | |
---|
| 142 | -d n |
---|
| 143 | This option specifies the number of outputs to be directly verified. |
---|
| 144 | That is, for n least significant outputs of the circuit, this command |
---|
| 145 | performs like comb_verify. The actual outputs are read off the output |
---|
| 146 | order array. Since the output order array is specified starting with |
---|
| 147 | the MSB, the number of directly verified outputs will be a chunk of |
---|
| 148 | the bottom part of the output order array. The option "-d all" sets |
---|
| 149 | the number of directly verified outputs to the number of |
---|
| 150 | combinational outputs in the circuit i.e., all outputs are directly |
---|
| 151 | verified. The direct verification for small BDD sizes is faster and |
---|
| 152 | overall reduces the number of primes to be used in residue |
---|
| 153 | verification. In general, one output is checked at a time against the |
---|
| 154 | corresponding output of the other network and consequently , this |
---|
| 155 | method may be fast and use less memory resources. |
---|
| 156 | IMPORTANT: It is possible to specify an initial order for the direct |
---|
| 157 | verification. This is done by reading in the specification file and |
---|
| 158 | using static_order to specify the initial order. The implementation |
---|
| 159 | will get the same order as the specification. When specifying the |
---|
| 160 | initial order, one must be careful not to specify the -s option in |
---|
| 161 | the res_verify command. The -s option reads in the specification file |
---|
| 162 | again and the initial order is lost. |
---|
| 163 | |
---|
| 164 | -h |
---|
| 165 | Print the command usage. |
---|
| 166 | |
---|
| 167 | -i <filename> |
---|
| 168 | Implementation network to perform verification against. The file must |
---|
| 169 | be in blif format unless -b is specified, in which case the file is |
---|
| 170 | taken to be in blif-mv format. The blif format is the default. |
---|
| 171 | |
---|
| 172 | -m <filename> |
---|
| 173 | Optional file name specifying the matching pair of output names |
---|
| 174 | between the two networks. If not specified, it is assumed that all |
---|
| 175 | outputs have identical names. This option is useful when verifying |
---|
| 176 | two circuits whose output names do not match. The file will give |
---|
| 177 | pairs of the form name1 name2 to be considered as corresponding |
---|
| 178 | outputs in the verification process. In each pair, name1 may belong |
---|
| 179 | to the specification and name2 to the implementation or vice-versa. |
---|
| 180 | The matching procedure is not capable of dealing with some special |
---|
| 181 | situations. For example, when two outputs, one of each network have |
---|
| 182 | the same name, they must correspond to the same output. Partial |
---|
| 183 | orders may not be specified. |
---|
| 184 | |
---|
| 185 | -n <filename> |
---|
| 186 | Optional file name specifying the matching pair of input names |
---|
| 187 | between the two networks. If not specified, it is assumed that all |
---|
| 188 | inputs have identical names. This option is useful when verifying two |
---|
| 189 | circuits whose input names do not match. The file will give pairs of |
---|
| 190 | the form name1 name2 to be considered as corresponding inputs in the |
---|
| 191 | verification process. In each pair, name1 may belong to the |
---|
| 192 | specification and name2 to the implementation or vice-versa. The |
---|
| 193 | matching procedure is not capable of dealing with some special |
---|
| 194 | situations. For example, when two inputs, one of each network have |
---|
| 195 | the same name, they must correspond to the same input. Partial orders |
---|
| 196 | may not be specified. |
---|
| 197 | |
---|
| 198 | -o <filename> |
---|
| 199 | Required file specifying output order, starting with the MSB. The |
---|
| 200 | file must be a list of output names separated by spaces. The list |
---|
| 201 | must belong to the specification network and must contain a full |
---|
| 202 | order i.e., must contain all the combinational output names. It is |
---|
| 203 | advisable to use the -o option as far as possible to specify the |
---|
| 204 | order of the outputs.See also -O option. |
---|
| 205 | |
---|
| 206 | -O |
---|
| 207 | This option specifies whether the res_verify command should generate |
---|
| 208 | a default order for the outputs. If the -o option is not used, this |
---|
| 209 | option must be specified. The default order generated is random and |
---|
| 210 | is NOT the same as the input files. The set of outputs for the output |
---|
| 211 | order may be generated by using the print_network command to write |
---|
| 212 | the network into a file and extract the node name from the lines |
---|
| 213 | containing the word "comb-output". The set of outputs can then be |
---|
| 214 | ordered as required. |
---|
| 215 | It is advisable to use the -o option as far as possible to specify |
---|
| 216 | the order of the outputs. The -o option overrides the -O option. See |
---|
| 217 | also -o option. |
---|
| 218 | |
---|
| 219 | -s <filename> |
---|
| 220 | Specification network. This network will be taken as the |
---|
| 221 | specification of the circuit. The result of the computation will be |
---|
| 222 | stored in this network. If this network is not provided, the current |
---|
| 223 | node of the hierarchy will be taken. The file must contain a blif |
---|
| 224 | description of a circuit unless the option -b is specified, in which |
---|
| 225 | case the file is considered in blif-mv format. If two networks are |
---|
| 226 | specified in the command line, both of them must have the same |
---|
| 227 | format, either blif or blif-mv. The blif format is the default. |
---|
| 228 | |
---|
| 229 | -t <timeOut > |
---|
| 230 | Execution time in seconds allowed for verification before aborting. |
---|
| 231 | The default is no limit. |
---|
| 232 | _________________________________________________________________ |
---|
| 233 | |
---|
| 234 | Last updated on 20100410 00h02 |
---|