[14] | 1 | |
---|
| 2 | flatten_hierarchy - create a flattened network |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | flatten_hierarchy [-a <file>] [-b] [-h] [-s] [-v #] |
---|
| 6 | |
---|
| 7 | Creates a flattened network from a hierarchical description. The flattened |
---|
| 8 | network encompasses everything from the current node of the hierarchy |
---|
| 9 | (reached by the command cd), down to and including the leaves. It creates a |
---|
| 10 | view with the hierarchy removed, but retains the multi-level logic |
---|
| 11 | structure. The resulting flattened network is stored with the current node. |
---|
| 12 | Every table in the flattened network is checked whether it is completely |
---|
| 13 | specified and deterministic. This is the starting point for verification |
---|
| 14 | related commands. |
---|
| 15 | |
---|
| 16 | A limited form of abstraction can be done by providing a list of variables |
---|
| 17 | to treat as primary inputs. See the information under <file> below. |
---|
| 18 | |
---|
| 19 | The verification part of VIS requires the functions specified by the BLIF-MV |
---|
| 20 | tables to be completely specified and deterministic. These conditions are |
---|
| 21 | checked during the flattening process; if a table is found that is |
---|
| 22 | incompletely specified or is nondeterministic, then an error message is |
---|
| 23 | written and a flattened network is not created. The exception to this rule |
---|
| 24 | is tables specifying "pseudo inputs"; these are tables with no inputs, and a |
---|
| 25 | single output that can take more than one value. Such tables are generated |
---|
| 26 | by vl2mv to model the "$ND" construct in Verilog. |
---|
| 27 | |
---|
| 28 | If this command is invoked a second time from the same point in the |
---|
| 29 | hierarchy, the previous network is deleted and a new one is created. This is |
---|
| 30 | the tactic to follow if you want to change some aspect of the current |
---|
| 31 | network, such as MDD variable ordering or image_method. |
---|
| 32 | |
---|
| 33 | Command options: |
---|
| 34 | |
---|
| 35 | -a <file> |
---|
| 36 | A file containing names of variables, used to specify which variables |
---|
| 37 | to abstract. The name of a variable is the full hierarchical path |
---|
| 38 | name, starting from just after the current hierarchy node (i.e., if |
---|
| 39 | the current node is foo, and you want to refer to variable x in foo, |
---|
| 40 | then just use x). A variable should appear at most once in the file. |
---|
| 41 | Each variable name should appear at the beginning of a new line, with |
---|
| 42 | no white space preceding it. The end of a variable name is marked by |
---|
| 43 | white space, and any other text on the rest of the line is ignored. |
---|
| 44 | Any line starting with "#" or white space is ignored. A sample file |
---|
| 45 | is shown here. |
---|
| 46 | |
---|
| 47 | # variables to abstract to model check liveness property |
---|
| 48 | choosing0 |
---|
| 49 | p0.pc |
---|
| 50 | |
---|
| 51 | |
---|
| 52 | For each variable x appearing in the file, a new primary input node |
---|
| 53 | named x$ABS is created to drive all the nodes that were previously |
---|
| 54 | driven by x. Hence, the node x will not have any fanouts; however, x |
---|
| 55 | and its transitive fanins will remain in the network. |
---|
| 56 | |
---|
| 57 | Abstracting a net effectively allows it to take any value in its |
---|
| 58 | range, at every clock cycle. This mechanism can be used to perform |
---|
| 59 | manual abstractions. The variables to abstract should not affect the |
---|
| 60 | correctness of the property being checked. This usually simplifies |
---|
| 61 | the network, and permits some verification tasks to complete that |
---|
| 62 | would not otherwise. Note, however, that by increasing the behavior |
---|
| 63 | of the system, false negatives are possible when checking universal |
---|
| 64 | properties, and false positives are possible when checking |
---|
| 65 | existential properties. |
---|
| 66 | |
---|
| 67 | A convenient way of generating the hierarchical variable names is by |
---|
| 68 | using the write_order command. Note that abstracting next state |
---|
| 69 | variables has no effect. |
---|
| 70 | |
---|
| 71 | -b |
---|
| 72 | This option has no effect any longer. |
---|
| 73 | |
---|
| 74 | -h |
---|
| 75 | Print the command usage. |
---|
| 76 | |
---|
| 77 | -s |
---|
| 78 | Do not perform a sweep. |
---|
| 79 | |
---|
| 80 | -v # |
---|
| 81 | Print debug information. |
---|
| 82 | 0: (default) Nothing is printed out. |
---|
| 83 | |
---|
| 84 | >= 2: Prints the variables read from the input file. |
---|
| 85 | _________________________________________________________________ |
---|
| 86 | |
---|
| 87 | Last updated on 20100410 00h02 |
---|