source: vis_dev/vis-2.3/share/help/static_orderCmd.txt @ 101

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

vis2.3
File size: 9.6 KB
Line 
1
2  static_order - order the MDD variables of the flattened network
3     _________________________________________________________________
4
5   static_order [-a] [-h] [-n <method>] [-o <type>] [-r <method>] -s <type> [-t
6   <timeOut>] [-v #] <file>
7
8   Order the MDD variables of the flattened network. MDD variables must be
9   created before MDDs can be built. Networks with combinational cycles cannot
10   be  ordered. If the MDD variables have already been ordered, then this
11   command does nothing. To undo the current ordering, reinvoke the command
12   flatten_hierarchy.
13
14   Command options:
15
16   -a
17          Order each next state variable immediately following the variables in
18          the support of the corresponding next state function. By default,
19          each  next  state variable is placed immeadiately following the
20          corresponding  present  state  variable.  It  has been observed
21          experimentally that ordering the NS variable after the PS variable is
22          almost always better; however, as a last b resort, you might want to
23          try this option.
24
25          Unless the -a flag is set, the PS and NS variables corresponding to
26          latches are grouped together and cannot be separated by dynamic
27          reordering. (This is done even when the ordering is read from a file
28          - adjacent PS/NS vars in the file are grouped).
29
30   -h
31          Print the command usage.
32
33   -n <method>
34          Specify which node ordering method to use. Node ordering is the
35          process of computing a total ordering on all the network nodes. This
36          ordering is then projected onto the set of nodes specified by -o
37          type. In the complexity measures below, n is the number of network
38          nodes, E is the number of network edges, and k is the number of
39          latches. "Method" must be one of the following:
40
41          interleave: (default) Uses Algorithm 2 of Fujii et al., "Interleaving
42          Based  Variable  Ordering  Methods  for OBDDs", ICCAD 1993. The
43          complexity is O(E+nlog(n)).
44
45          append: Uses the algorithm of Malik, et al. "Logic Verification using
46          Binary Decision Diagrams in a Logic Synthesis Environment," ICCAD,
47          1988. Nodes are visited in DFS order, and appended to a global order
48          list in the order they are visited. The fanins of a node are visited
49          in order of decreasing depth. The roots of the DFS are visited in the
50          order determined by the -r method. The complexity is O(E+nlog(n)).
51
52          merge_left:  Uses  an  algorithm  alluded  to  in Fujii et al.,
53          "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993.
54          Nodes are visited in DFS order. At a given node g, its fanins are
55          visited in order of decreasing depth. For each fanin fi, a total
56          order is computed for all the nodes in the transitive fanin (TFI) of
57          fi, including fi itself. This ordering is merged into the combined
58          ordering from fanins of higher priority. After processing all of the
59          fanins,  the  result is a total ordering on all TFI nodes of g.
60          Finally,  g is appended to the end of this ordering, yielding a
61          topological ordering. For example if the ordering for f1 is list1 =
62          (a,b,d,f1) and for f2 is list2=(c,d,e,f2), and f1 has greater depth
63          than f2, then the ordering for g is (c,a,b,d,e,f2,f1,g). The merge is
64          done by inserting into list1 those nodes in list2 not already in
65          list1, in such a way that the inserted nodes remain as close as
66          possible to their left neighbors in list2 ("insert as far left as
67          possible"). The roots of the DFS are merged in the order determined
68          by -r method. The complexity is O(n^2) (currently, there is a bug
69          which causes more memory to be consumed than necessary).
70
71          merge_right: Same as merge_left, except that the merge is done in
72          such a way that the inserted nodes remain as close as possible to
73          their right neighbors in list2 ("insert as far right as possible").
74          For the example above, the ordering for g is (a,b,c,d,f1,e,f2,g). It
75          has  been  observed  experimentally that neither merge_left nor
76          merge_right  is  superior  to  the other; there are cases where
77          verification times out with merge_left but not merge_right, and vice
78          versa.
79
80   -o <type>
81          Specify the network nodes for which MDD variables should be created.
82          Type can be one of the following:
83
84          all: Order all the nodes of the network. This is normally not used.
85
86          input_and_latch: (default) Order the primary inputs, pseudo inputs,
87          latches, and next state variables. This is the minimum set of nodes
88          that need to be ordered to perform operations on FSMs (e.g. model
89          checking, reachability). For purely combinational circuits, just the
90          primary and pseudo inputs are ordered.
91
92   -r <method>
93          Specify which root ordering method to use. The "roots" of a network
94          refer to the roots of the cones of logic driving the combinational
95          outputs (data latch inputs, initial state latch inputs, and primary
96          outputs) of a network. Root ordering is used to determine in which
97          order to visit the roots of the network for the DFS carried out in
98          node ordering (see -n). "Method" must be one of the following:
99
100          depth: (default for 30 or more latches) Roots are ordered based on
101          logic depth (i.e. longest path to a combinational input). Greater
102          depth roots appear earlier in the ordering. All data latch inputs
103          appear before all other combinational outputs. The complexity is
104          O(E+nlog(n)).  It has been observed experimentally that mincomm
105          produces superior orderings to depth. However, the complexity of the
106          mincomm  algorithm is such that it cannot produce orderings for
107          designs  with more than a hundred or so latches. Hence, for big
108          designs, use depth, followed optionally by dynamic_var_ordering.
109
110          mincomm: (default for less than 30 latches) Uses the algorithm of
111          Aziz, et al. "BDD Variable Ordering for Interacting Finite State
112          Machines," DAC, 1994. First, the latches are ordered to decrease a
113          communication  complexity  bound (where backward edges are more
114          expensive than forward edges) on the latch communication graph. This
115          directly gives an ordering for the data latch inputs. The remaining
116          combinational outputs are ordered after the data latch inputs, in
117          decreasing  order  of  their  depth.  The  total  complexity is
118          O(nlog(n)+E+k^3).
119
120   -s <type>
121          Used in conjunction with <file> to specify which nodes are supplied
122          in the ordering file. Type can be one of the following (there is no
123          default):
124
125          all: The ordering file supplies all the nodes of the network. The
126          ordering generated is the supplied order, projected onto the set of
127          nodes specified by -o.
128
129          input_and_latch: The ordering file supplies the primary inputs,
130          pseudo  inputs, latches, and next state variables. The ordering
131          generated  is  exactly  what  is  supplied  (in  the case of -o
132          input_and_latch). -o all is incompatible with -s input_and_latch.
133
134          next_state_node: The ordering file supplies next state variables.
135          During the ordering algorithm, the next state functions are visited
136          in the order in which their corresponding next state variables appear
137          in the file. The order of the next state variables in the ordering
138          generated is not necessarily maintained.
139
140          partial: The ordering file supplies an arbitrary subset of nodes of
141          the network. The ordering algorithm works by finding a total ordering
142          on all the nodes (independent of the ordering supplied), then merging
143          the computed order into the supplied order (maintaining the relative
144          order of the supplied order), and then projecting the resulting
145          ordering onto the set of nodes specified by -o.
146
147   -t <timeOut>
148          Time in seconds allowed to perform static ordering. If the flattened
149          network has more than a couple hundred latches and you are using
150          option -r mincomm, then you might want to set a timeOut to limit the
151          allowed time. The default is no limit.
152
153   -v #
154          Print debug information.
155          0 Nothing is printed out. This is the default.
156
157          >=  1 Prints the nodes read from the input file (satisfying the
158          supplied order type); prints the root order used for exploring the
159          network.
160
161          >= 2 Prints the depth of nodes.
162
163          >= 3 Prints the ordering computed at each node.
164
165   <file>
166          A file containing names of network nodes, used to specify a variable
167          ordering. The name of a node is the full hierarchical path name,
168          starting from the current hierarchical node. A node should appear at
169          most once in the file. Each node name should appear at the beginning
170          of a new line, with no white space preceeding it. The end of a node
171          name is marked by white space, and any other text on the rest of the
172          line  is  ignored. Any line starting with "#" or white space is
173          ignored. See write_order for a sample file. Note that the variable
174          ordering  cannot  be specified at the bit-level; it can only be
175          specified at the multi-valued variable level.
176     _________________________________________________________________
177
178   Last updated on 20100410 00h02
Note: See TracBrowser for help on using the repository browser.