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