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:
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).
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.
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.
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).
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.
>= 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.