source: vis_dev/vis-2.3/share/help/print_ardc_optionsCmd.txt @ 14

Last change on this file since 14 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 7.2 KB
Line 
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
Note: See TracBrowser for help on using the repository browser.