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.
Command options:
0: Do not group.
1: Do group (default).
# name type mddId vals levs system.choosing0 primary-input 31 2 (61) system.p0.pc latch 32 11 (62, 63, 64, 65)The first column gives the full hierarchical path name of the node, starting from the current hierarchical node. The second column gives the type of the node in the flattened network (see the command print_network). The third column gives the MDD id of the node; this can be thought of as just another name for the node. The fourth column gives the number of values that the multi-valued variable at the output of the node can assume. The last column gives the levels of the BDD variables that encode the multi-valued variable (0 is the topmost level of the BDD).
The bits of a multi-valued variable need not appear consecutively (due to dynamic variable ordering). Each node appears at most once in the output file. The nodes in the file appear in ascending order of the lowest level bit in the encoding of the node's multi-valued variable (e.g. a node with levels (12, 73) will appear before a node with levels (17, 21, 25)).
To specify a variable ordering for static_order, a convenient tactic is to write out the current ordering, edit the file to rearrange the ordering (or comment out some nodes, using "#"), and then read the file back in using static_order. Note that everything after the first column is ignored when the file is read in.
Command options:
all: Write out all the nodes of the network. This option is allowed only if all variables have been ordered.
input_and_latch: (default) Write out the primary inputs, pseudo inputs, latches, and next state variables.
next_state_node: Write out the next state variables (node type is "shadow"). This file can be modified and read back in using the static_order -s next_state_node command.
Dynamic ordering may be time consuming, but can often reduce the size of the MDDs dramatically. The good points to invoke dynamic ordering explicitly (using the -f option) are after the commands build_partition_mdds and print_img_info. If dynamic ordering finds a good ordering, then you may wish to save this ordering (using write_order) and reuse it (using static_order -s) in the future. A common sequence used to get a good ordering is the following:
init_verify print_img_info dynamic_var_ordering -f sift write_orderflatten_hierarchy static_order -s input_and_latch -f build_partition_mdds print_img_info dynamic_var_ordering -f sift
For many large examples, there is no single best variable order, or that order is hard to find. For example, the best ordering during partitioning of the network may be different from the best ordering during a model check. In that case you can use automatic reordering, using the -e option. This will trigger reordering whenever the total size of the MDD increases by a certain factor. Often, the init command is replaced by the following sequence:
flatten_hierarchy static_order dynamic_var_ordering -e sift build_partition_mddsCommand options:
window: Permutes the variables within windows of three adjacent variables so as to minimize the overall MDD size. This process is repeated until no more reduction in size occurs.
sift: Moves each variable throughout the order to find an optimal position for that variable (assuming all other variables are fixed). This generally achieves greater size reductions than the window method, but is slower.
The following methods are only available if VIS has been linked with the Bdd package from the University of Colorado (cuBdd).
random: Pairs of variables are randomly chosen, and swapped in the order. The swap is performed by a series of swaps of adjacent variables. The best order among those obtained by the series of swaps is retained. The number of pairs chosen for swapping equals the number of variables in the diagram.
random_pivot: Same as random, but the two variables are chosen so that the first is above the variable with the largest number of nodes, and the second is below that variable. In case there are several variables tied for the maximum number of nodes, the one closest to the root is used.
sift_converge: The sift method is iterated until no further improvement is obtained.
symmetry_sift: This method is an implementation of symmetric sifting. It is similar to sifting, with one addition: Variables that become adjacent during sifting are tested for symmetry. If they are symmetric, they are linked in a group. Sifting then continues with a group being moved, instead of a single variable.
symmetry_sift_converge: The symmetry_sift method is iterated until no further improvement is obtained.
window{2,3,4}: Permutes the variables within windows of n adjacent variables, where "n" can be either 2, 3 or 4, so as to minimize the overall MDD size.
window{2,3,4}_converge: The window{2,3,4} method is iterated until no further improvement is obtained.
group_sift: This method is similar to symmetry_sift, but uses more general criteria to create groups.
group_sift_converge: The group_sift method is iterated until no further improvement is obtained.
lazy_sift: This method is similar to group_sift, but the creation of groups takes into account the pairing of present and next state variables.
annealing: This method is an implementation of simulated annealing for variable ordering. This method is potentially very slow.
genetic: This method is an implementation of a genetic algorithm for variable ordering. This method is potentially very slow.
Command options: