source: vis_dev/vis-2.1/share/help/static_orderCmd.txt @ 12

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

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