source: vis_dev/vis-2.1/share/help/flatten_hierarchyCmd.txt @ 14

Last change on this file since 14 was 11, checked in by cecile, 13 years ago

Add vis
File size: 4.3 KB
Line 
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
Note: See TracBrowser for help on using the repository browser.