[11] | 1 | |
---|
| 2 | print_ardc_options - print information about the ARDC options currently in |
---|
| 3 | use |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | print_ardc_options [-h] [-H] |
---|
| 7 | |
---|
| 8 | Prints information about the current ARDC options. |
---|
| 9 | |
---|
| 10 | Command options: |
---|
| 11 | |
---|
| 12 | -h |
---|
| 13 | Print the command usage. |
---|
| 14 | |
---|
| 15 | -H |
---|
| 16 | Print the ARDC set command usage. |
---|
| 17 | |
---|
| 18 | Set parameters: The ARDC options are specified with the set command. |
---|
| 19 | |
---|
| 20 | ardc_traversal_method <method> |
---|
| 21 | Specify a method for approximate FSM traversal. |
---|
| 22 | |
---|
| 23 | method must be one of the following: |
---|
| 24 | |
---|
| 25 | 0 : MBM (machine by machine). |
---|
| 26 | |
---|
| 27 | 1 : RFBF(reached frame by frame). |
---|
| 28 | |
---|
| 29 | 2 : TFBF(to frame by frame). |
---|
| 30 | |
---|
| 31 | 3 : TMBM(combination of MBM and TFBF). |
---|
| 32 | |
---|
| 33 | 4 : LMBM(least fixpoint MBM, default). |
---|
| 34 | |
---|
| 35 | 5 : TLMBM(combination of LMBM and TFBF). |
---|
| 36 | |
---|
| 37 | ardc_group_size <size> |
---|
| 38 | Specify the number of latches per group for ARDCS. |
---|
| 39 | |
---|
| 40 | size must be a positive integer (default = 8). |
---|
| 41 | |
---|
| 42 | ardc_affinity_factor <affinity> |
---|
| 43 | Specify affinity factor to make a group for ARDCs. The |
---|
| 44 | available factor is from 0.0(use only correlation) to 1.0(use |
---|
| 45 | only dependency). |
---|
| 46 | |
---|
| 47 | affinity must be a positive real (default = 0.5). |
---|
| 48 | |
---|
| 49 | ardc_max_iteration <iteration> |
---|
| 50 | Specify the maximum iteration count during approximate FSM |
---|
| 51 | traversal. Default is 0 which means infinite. |
---|
| 52 | |
---|
| 53 | iteration must be a positive integer or zero. |
---|
| 54 | |
---|
| 55 | ardc_constrain_target <target> |
---|
| 56 | Specify where image constraining will be applied to. |
---|
| 57 | |
---|
| 58 | target must be one of the following: |
---|
| 59 | |
---|
| 60 | 0 : constrain transition relation (default). |
---|
| 61 | |
---|
| 62 | 1 : constrain initial states. |
---|
| 63 | |
---|
| 64 | 2 : constrain both. |
---|
| 65 | |
---|
| 66 | ardc_constrain_method <method> |
---|
| 67 | Specify an image constraining method to compute ARDCs. |
---|
| 68 | |
---|
| 69 | method must be one of the following: |
---|
| 70 | |
---|
| 71 | 0 : restrict (default). |
---|
| 72 | |
---|
| 73 | 1 : constrain |
---|
| 74 | |
---|
| 75 | 2 : compact (currently supported by only CUDD) |
---|
| 76 | |
---|
| 77 | 3 : squeeze (currently supported by only CUDD) |
---|
| 78 | |
---|
| 79 | ardc_constrain_reorder <method> |
---|
| 80 | Specify whether to enable variable reorderings during |
---|
| 81 | consecutive image constraining operations. |
---|
| 82 | |
---|
| 83 | method must be one of the following: |
---|
| 84 | |
---|
| 85 | yes : allow variable reorderings during consecutive image |
---|
| 86 | constraining operations (default) |
---|
| 87 | |
---|
| 88 | no : don't allow variable reorderings during consecutive image |
---|
| 89 | constraining operations |
---|
| 90 | |
---|
| 91 | ardc_abstract_pseudo_input <method> |
---|
| 92 | Specify when to abstract pseudo primary input variables out |
---|
| 93 | from transition relation. |
---|
| 94 | |
---|
| 95 | method must be one of the following: |
---|
| 96 | |
---|
| 97 | 0 : do not abstract pseudo input variables |
---|
| 98 | |
---|
| 99 | 1 : abstract pseudo inputs before image computation (default) |
---|
| 100 | |
---|
| 101 | 2 : abstract pseudo inputs at every end of image computation |
---|
| 102 | |
---|
| 103 | 3 : abstract pseudo inputs at the end of approximate traversal |
---|
| 104 | |
---|
| 105 | ardc_decompose_flag <method> |
---|
| 106 | Specify whether to use decomposed approximate reachable states |
---|
| 107 | or single conjuncted reachable states. |
---|
| 108 | |
---|
| 109 | method must be one of the following: |
---|
| 110 | |
---|
| 111 | yes : keep decomposed reachable stateses (default) |
---|
| 112 | |
---|
| 113 | no : make a conjunction of reachable states of all submachines |
---|
| 114 | |
---|
| 115 | ardc_projected_initial_flag <method> |
---|
| 116 | Specify which initial states is going to be used. |
---|
| 117 | |
---|
| 118 | method must be one of the following: |
---|
| 119 | |
---|
| 120 | yes : use projected initial states for submachine (default) |
---|
| 121 | |
---|
| 122 | no : use original initial states for submachine |
---|
| 123 | |
---|
| 124 | ardc_image_method <method> |
---|
| 125 | Specify image_mathod during computing reachable states of |
---|
| 126 | submachines. |
---|
| 127 | |
---|
| 128 | method must be one of the following: |
---|
| 129 | |
---|
| 130 | monolithic : use monolithic image computation |
---|
| 131 | |
---|
| 132 | iwls95 : use iwls95 image computation (default) |
---|
| 133 | |
---|
| 134 | mlp : use mlp image computation |
---|
| 135 | |
---|
| 136 | tfm : use tfm image computation |
---|
| 137 | |
---|
| 138 | hybrid : use hybrid image computation |
---|
| 139 | |
---|
| 140 | ardc_use_high_density <method> |
---|
| 141 | Specify whether to use high density in computing reachable |
---|
| 142 | states of submachines. |
---|
| 143 | |
---|
| 144 | method must be one of the following: |
---|
| 145 | |
---|
| 146 | yes : use High Density for reachable states of submachines |
---|
| 147 | |
---|
| 148 | no : use BFS for reachable states of submachines (default) |
---|
| 149 | |
---|
| 150 | ardc_reorder_ptr <method> |
---|
| 151 | Specify whether to reorder partitioned transition relation |
---|
| 152 | after constraining fanin submachines. |
---|
| 153 | |
---|
| 154 | method must be one of the following: |
---|
| 155 | |
---|
| 156 | yes : whenever partitioned transition relation changes, |
---|
| 157 | reorders partitioned transition relation |
---|
| 158 | |
---|
| 159 | no : no reordering of partitioned transition relation (default) |
---|
| 160 | |
---|
| 161 | ardc_fanin_constrain_mode <method> |
---|
| 162 | Specify which method will be used in constraining fanin |
---|
| 163 | submachines. |
---|
| 164 | |
---|
| 165 | method must be one of the following: |
---|
| 166 | |
---|
| 167 | 0 : constrain w.r.t. the reachable states of fanin submachines |
---|
| 168 | (default) |
---|
| 169 | |
---|
| 170 | 1 : constrain w.r.t. the reachable states of both fanin |
---|
| 171 | submachines and itself |
---|
| 172 | |
---|
| 173 | ardc_create_pseudo_var_mode <method> |
---|
| 174 | Specify which method will be used to create pseudo input |
---|
| 175 | variables of submachines. |
---|
| 176 | |
---|
| 177 | method must be one of the following: |
---|
| 178 | |
---|
| 179 | 0 : makes pseudo input variables with exact support (default) |
---|
| 180 | |
---|
| 181 | 1 : makes pseudo input variables from all state variables of |
---|
| 182 | the other submachines |
---|
| 183 | |
---|
| 184 | 2 : makes pseudo input variables from all state variables of |
---|
| 185 | fanin submachines |
---|
| 186 | |
---|
| 187 | ardc_lmbm_initial_mode <method> |
---|
| 188 | Specify which method will be used as initial states in LMBM |
---|
| 189 | computation. |
---|
| 190 | |
---|
| 191 | method must be one of the following: |
---|
| 192 | |
---|
| 193 | 0 : use given initial states all the time |
---|
| 194 | |
---|
| 195 | 1 : use current reached states as initial states (default) |
---|
| 196 | |
---|
| 197 | 2 : use current frontier as initial states |
---|
| 198 | |
---|
| 199 | set ardc_mbm_reuse_tr <method> |
---|
| 200 | Specify whether to reuse already constrained transition |
---|
| 201 | relation for next iteratrion in MBM. |
---|
| 202 | |
---|
| 203 | method must be one of the following: |
---|
| 204 | |
---|
| 205 | yes : use constrained transition relation for next iteration |
---|
| 206 | |
---|
| 207 | no : use original transition relation for next iteration |
---|
| 208 | (default) |
---|
| 209 | |
---|
| 210 | ardc_read_group <filename> |
---|
| 211 | Specify a filename containing grouping information |
---|
| 212 | |
---|
| 213 | filename containing grouping information |
---|
| 214 | |
---|
| 215 | ardc_write_group <filename> |
---|
| 216 | Specify a filename to write grouping information |
---|
| 217 | |
---|
| 218 | filename to write grouping information |
---|
| 219 | |
---|
| 220 | ardc_verbosity <verbosity> |
---|
| 221 | Specify the level of printing information during computing |
---|
| 222 | ARDCs. |
---|
| 223 | |
---|
| 224 | verbosity must be 0 - 3 (default = 0). |
---|
| 225 | |
---|
| 226 | The default settings correspond to the fast variants of LMBM and MBM. |
---|
| 227 | MBM never produces a more accurate approximation than LMBM for the |
---|
| 228 | same state-space decomposition. However, the corresponding statement |
---|
| 229 | does not hold for the fast versions. (That is, FastMBM will |
---|
| 230 | occasionally outperform FastLMBM.) To get the slower, but more |
---|
| 231 | accurate versions of LMBM and MBM use the following settings: |
---|
| 232 | * set ardc_constrain_method 1 |
---|
| 233 | * set ardc_constrain_reorder no |
---|
| 234 | * set ardc_abstract_pseudo_input 0 |
---|
| 235 | _________________________________________________________________ |
---|
| 236 | |
---|
| 237 | Last updated on 20050519 10h16 |
---|