
  static_order - order the MDD variables of the flattened network
     _________________________________________________________________

   static_order [-a] [-h] [-n <method>] [-o <type>] [-r <method>] -s <type> [-t
   <timeOut>] [-v #] <file>

   Order the MDD variables of the flattened network. MDD variables must be
   created before MDDs can be built. Networks with combinational cycles cannot
   be  ordered. If the MDD variables have already been ordered, then this
   command does nothing. To undo the current ordering, reinvoke the command
   flatten_hierarchy.

   Command options:

   -a
          Order each next state variable immediately following the variables in
          the support of the corresponding next state function. By default,
          each  next  state variable is placed immeadiately following the
          corresponding  present  state  variable.  It  has been observed
          experimentally that ordering the NS variable after the PS variable is
          almost always better; however, as a last b resort, you might want to
          try this option.

          Unless the -a flag is set, the PS and NS variables corresponding to
          latches are grouped together and cannot be separated by dynamic
          reordering. (This is done even when the ordering is read from a file
          - adjacent PS/NS vars in the file are grouped).

   -h
          Print the command usage.

   -n <method>
          Specify which node ordering method to use. Node ordering is the
          process of computing a total ordering on all the network nodes. This
          ordering is then projected onto the set of nodes specified by -o
          type. In the complexity measures below, n is the number of network
          nodes, E is the number of network edges, and k is the number of
          latches. "Method" must be one of the following:

          interleave: (default) Uses Algorithm 2 of Fujii et al., "Interleaving
          Based  Variable  Ordering  Methods  for OBDDs", ICCAD 1993. The
          complexity is O(E+nlog(n)).

          append: Uses the algorithm of Malik, et al. "Logic Verification using
          Binary Decision Diagrams in a Logic Synthesis Environment," ICCAD,
          1988. Nodes are visited in DFS order, and appended to a global order
          list in the order they are visited. The fanins of a node are visited
          in order of decreasing depth. The roots of the DFS are visited in the
          order determined by the -r method. The complexity is O(E+nlog(n)).

          merge_left:  Uses  an  algorithm  alluded  to  in Fujii et al.,
          "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993.
          Nodes are visited in DFS order. At a given node g, its fanins are
          visited in order of decreasing depth. For each fanin fi, a total
          order is computed for all the nodes in the transitive fanin (TFI) of
          fi, including fi itself. This ordering is merged into the combined
          ordering from fanins of higher priority. After processing all of the
          fanins,  the  result is a total ordering on all TFI nodes of g.
          Finally,  g is appended to the end of this ordering, yielding a
          topological ordering. For example if the ordering for f1 is list1 =
          (a,b,d,f1) and for f2 is list2=(c,d,e,f2), and f1 has greater depth
          than f2, then the ordering for g is (c,a,b,d,e,f2,f1,g). The merge is
          done by inserting into list1 those nodes in list2 not already in
          list1, in such a way that the inserted nodes remain as close as
          possible to their left neighbors in list2 ("insert as far left as
          possible"). The roots of the DFS are merged in the order determined
          by -r method. The complexity is O(n^2) (currently, there is a bug
          which causes more memory to be consumed than necessary).

          merge_right: Same as merge_left, except that the merge is done in
          such a way that the inserted nodes remain as close as possible to
          their right neighbors in list2 ("insert as far right as possible").
          For the example above, the ordering for g is (a,b,c,d,f1,e,f2,g). It
          has  been  observed  experimentally that neither merge_left nor
          merge_right  is  superior  to  the other; there are cases where
          verification times out with merge_left but not merge_right, and vice
          versa.

   -o <type>
          Specify the network nodes for which MDD variables should be created.
          Type can be one of the following:

          all: Order all the nodes of the network. This is normally not used.

          input_and_latch: (default) Order the primary inputs, pseudo inputs,
          latches, and next state variables. This is the minimum set of nodes
          that need to be ordered to perform operations on FSMs (e.g. model
          checking, reachability). For purely combinational circuits, just the
          primary and pseudo inputs are ordered.

   -r <method>
          Specify which root ordering method to use. The "roots" of a network
          refer to the roots of the cones of logic driving the combinational
          outputs (data latch inputs, initial state latch inputs, and primary
          outputs) of a network. Root ordering is used to determine in which
          order to visit the roots of the network for the DFS carried out in
          node ordering (see -n). "Method" must be one of the following:

          depth: (default for 30 or more latches) Roots are ordered based on
          logic depth (i.e. longest path to a combinational input). Greater
          depth roots appear earlier in the ordering. All data latch inputs
          appear before all other combinational outputs. The complexity is
          O(E+nlog(n)).  It has been observed experimentally that mincomm
          produces superior orderings to depth. However, the complexity of the
          mincomm  algorithm is such that it cannot produce orderings for
          designs  with more than a hundred or so latches. Hence, for big
          designs, use depth, followed optionally by dynamic_var_ordering.

          mincomm: (default for less than 30 latches) Uses the algorithm of
          Aziz, et al. "BDD Variable Ordering for Interacting Finite State
          Machines," DAC, 1994. First, the latches are ordered to decrease a
          communication  complexity  bound (where backward edges are more
          expensive than forward edges) on the latch communication graph. This
          directly gives an ordering for the data latch inputs. The remaining
          combinational outputs are ordered after the data latch inputs, in
          decreasing  order  of  their  depth.  The  total  complexity is
          O(nlog(n)+E+k^3).

   -s <type>
          Used in conjunction with <file> to specify which nodes are supplied
          in the ordering file. Type can be one of the following (there is no
          default):

          all: The ordering file supplies all the nodes of the network. The
          ordering generated is the supplied order, projected onto the set of
          nodes specified by -o.

          input_and_latch: The ordering file supplies the primary inputs,
          pseudo  inputs, latches, and next state variables. The ordering
          generated  is  exactly  what  is  supplied  (in  the case of -o
          input_and_latch). -o all is incompatible with -s input_and_latch.

          next_state_node: The ordering file supplies next state variables.
          During the ordering algorithm, the next state functions are visited
          in the order in which their corresponding next state variables appear
          in the file. The order of the next state variables in the ordering
          generated is not necessarily maintained.

          partial: The ordering file supplies an arbitrary subset of nodes of
          the network. The ordering algorithm works by finding a total ordering
          on all the nodes (independent of the ordering supplied), then merging
          the computed order into the supplied order (maintaining the relative
          order of the supplied order), and then projecting the resulting
          ordering onto the set of nodes specified by -o.

   -t <timeOut>
          Time in seconds allowed to perform static ordering. If the flattened
          network has more than a couple hundred latches and you are using
          option -r mincomm, then you might want to set a timeOut to limit the
          allowed time. The default is no limit.

   -v #
          Print debug information.
          0 Nothing is printed out. This is the default.

          >=  1 Prints the nodes read from the input file (satisfying the
          supplied order type); prints the root order used for exploring the
          network.

          >= 2 Prints the depth of nodes.

          >= 3 Prints the ordering computed at each node.

   <file>
          A file containing names of network nodes, used to specify a variable
          ordering. The name of a node is the full hierarchical path name,
          starting from the current hierarchical node. A node should appear at
          most once in the file. Each node name should appear at the beginning
          of a new line, with no white space preceeding it. The end of a node
          name is marked by white space, and any other text on the rest of the
          line  is  ignored. Any line starting with "#" or white space is
          ignored. See write_order for a sample file. Note that the variable
          ordering  cannot  be specified at the bit-level; it can only be
          specified at the multi-valued variable level.
     _________________________________________________________________

   Last updated on 20100410 00h02
