[14] | 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 |
---|