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 |
---|