1 | |
---|
2 | dynamic_var_ordering - control the application of dynamic variable ordering |
---|
3 | _________________________________________________________________ |
---|
4 | |
---|
5 | dynamic_var_ordering [-d] [-e <method>] [-f <method>] [-h] |
---|
6 | |
---|
7 | Control the application of dynamic variable ordering to the flattened |
---|
8 | network. Dynamic ordering is a technique to reorder the MDD variables to |
---|
9 | reduce the size of the existing MDDs. When no options are specified, the |
---|
10 | current status of dynamic ordering is displayed. At most one of the options |
---|
11 | -e, -f, and -d should be specified. The commands flatten_hierarchy and |
---|
12 | static_order must be invoked before this command. |
---|
13 | |
---|
14 | Dynamic ordering may be time consuming, but can often reduce the size of the |
---|
15 | MDDs dramatically. The good points to invoke dynamic ordering explicitly |
---|
16 | (using the -f option) are after the commands build_partition_mdds and |
---|
17 | print_img_info. If dynamic ordering finds a good ordering, then you may wish |
---|
18 | to save this ordering (using write_order) and reuse it (using static_order |
---|
19 | -s) in the future. A common sequence used to get a good ordering is the |
---|
20 | following: |
---|
21 | |
---|
22 | init_verify |
---|
23 | print_img_info |
---|
24 | dynamic_var_ordering -f sift |
---|
25 | write_order |
---|
26 | flatten_hierarchy |
---|
27 | static_order -s input_and_latch -f |
---|
28 | build_partition_mdds |
---|
29 | print_img_info |
---|
30 | dynamic_var_ordering -f sift |
---|
31 | |
---|
32 | |
---|
33 | For many large examples, there is no single best variable order, or that |
---|
34 | order is hard to find. For example, the best ordering during partitioning of |
---|
35 | the network may be different from the best ordering during a model check. In |
---|
36 | that case you can use automatic reordering, using the -e option. This will |
---|
37 | trigger reordering whenever the total size of the MDD increases by a certain |
---|
38 | factor. Often, the init command is replaced by the following sequence: |
---|
39 | flatten_hierarchy |
---|
40 | static_order |
---|
41 | dynamic_var_ordering -e sift |
---|
42 | build_partition_mdds |
---|
43 | |
---|
44 | |
---|
45 | Command options: |
---|
46 | |
---|
47 | -d |
---|
48 | Disable dynamic ordering from triggering automatically. |
---|
49 | |
---|
50 | -e <method> |
---|
51 | Enable dynamic ordering to trigger automatically whenever a certain |
---|
52 | threshold on the overall MDD size is reached. "Method" must be one of |
---|
53 | the following: |
---|
54 | |
---|
55 | window: Permutes the variables within windows of three adjacent |
---|
56 | variables so as to minimize the overall MDD size. This process is |
---|
57 | repeated until no more reduction in size occurs. |
---|
58 | |
---|
59 | sift: Moves each variable throughout the order to find an optimal |
---|
60 | position for that variable (assuming all other variables are fixed). |
---|
61 | This generally achieves greater size reductions than the window |
---|
62 | method, but is slower. |
---|
63 | |
---|
64 | The following methods are only available if VIS has been linked with |
---|
65 | the Bdd package from the University of Colorado (cuBdd). |
---|
66 | |
---|
67 | random: Pairs of variables are randomly chosen, and swapped in the |
---|
68 | order. The swap is performed by a series of swaps of adjacent |
---|
69 | variables. The best order among those obtained by the series of swaps |
---|
70 | is retained. The number of pairs chosen for swapping equals the |
---|
71 | number of variables in the diagram. |
---|
72 | |
---|
73 | random_pivot: Same as random, but the two variables are chosen so |
---|
74 | that the first is above the variable with the largest number of |
---|
75 | nodes, and the second is below that variable. In case there are |
---|
76 | several variables tied for the maximum number of nodes, the one |
---|
77 | closest to the root is used. |
---|
78 | |
---|
79 | sift_converge: The sift method is iterated until no further |
---|
80 | improvement is obtained. |
---|
81 | |
---|
82 | symmetry_sift: This method is an implementation of symmetric sifting. |
---|
83 | It is similar to sifting, with one addition: Variables that become |
---|
84 | adjacent during sifting are tested for symmetry. If they are |
---|
85 | symmetric, they are linked in a group. Sifting then continues with a |
---|
86 | group being moved, instead of a single variable. |
---|
87 | |
---|
88 | symmetry_sift_converge: The symmetry_sift method is iterated until no |
---|
89 | further improvement is obtained. |
---|
90 | |
---|
91 | window{2,3,4}: Permutes the variables within windows of n adjacent |
---|
92 | variables, where "n" can be either 2, 3 or 4, so as to minimize the |
---|
93 | overall MDD size. |
---|
94 | |
---|
95 | window{2,3,4}_converge: The window{2,3,4} method is iterated until no |
---|
96 | further improvement is obtained. |
---|
97 | |
---|
98 | group_sift: This method is similar to symmetry_sift, but uses more |
---|
99 | general criteria to create groups. |
---|
100 | |
---|
101 | group_sift_converge: The group_sift method is iterated until no |
---|
102 | further improvement is obtained. |
---|
103 | |
---|
104 | lazy_sift: This method is similar to group_sift, but the creation of |
---|
105 | groups takes into account the pairing of present and next state |
---|
106 | variables. |
---|
107 | |
---|
108 | annealing: This method is an implementation of simulated annealing |
---|
109 | for variable ordering. This method is potentially very slow. |
---|
110 | |
---|
111 | genetic: This method is an implementation of a genetic algorithm for |
---|
112 | variable ordering. This method is potentially very slow. |
---|
113 | |
---|
114 | -f <method> |
---|
115 | Force dynamic ordering to be invoked immediately. The values for |
---|
116 | method are the same as in option -e. |
---|
117 | |
---|
118 | -h |
---|
119 | Print the command usage. |
---|
120 | |
---|
121 | -v <#> |
---|
122 | Verbosity level. Default is 0. For values greater than 0, statistics |
---|
123 | pertaining to reordering will be printed whenever reordering occurs. |
---|
124 | _________________________________________________________________ |
---|
125 | |
---|
126 | Last updated on 20100410 00h02 |
---|