source: vis_dev/vis-2.1/share/help/print_ardc_optionsCmd.txt @ 12

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

Add vis
File size: 7.5 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
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
Note: See TracBrowser for help on using the repository browser.