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