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

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

Add vis
File size: 8.2 KB
Line 
1
2  print_hd_options - print information about the HD options currently in use
3     _________________________________________________________________
4
5   print_hd_options [-h]
6
7   Prints  information  about the current HD options. The HD method is an
8   alternate  method to compute a least fixpoint and is provided with the
9   compute_reach and check_invariant commands. The method is described in
10   Ravi  and Somenzi, ICCAD95. The command can be used only when compiled
11   with the CUDD package.
12
13   Command options:
14
15   -h
16   Print the command usage.
17
18   Set parameters: The HD options are specified with the set command.
19
20   hd_frontier_approx_method <method>
21          This  option  specifes  the  method to approximate the frontier
22          set.
23
24          Methods:
25
26          remap_ua  :  (Default)  The  BDD  approximation method of DAC98
27          Ravi, Shiple, McMillan, Somenzi.
28
29          biased_rua : Approximation method similar to remap_ua, but uses
30          a  bias  function.  The bias function is set appropriate to the
31          context.
32
33          under_approx : The BDD approximation method of Shiple's thesis.
34
35          heavy_branch  :  The  BDD approximation method of ICCAD95 Ravi,
36          Somenzi.
37
38          short_paths  :  The  BDD  approximation method of ICCAD95 Ravi,
39          Somenzi.
40
41          compress  : An approximation method that runs short_paths first
42          and then remap_ua.
43
44   hd_frontier_approx_threshold <number>
45          This  option  specifes  the size of the frontier to be used for
46          image  computation.  The  threshold  for the various methods is
47          approximate  (not  strictly  adhered  to). For the remap_ua and
48          biased_rua  method,  this  threshold  is  a lower bound and the
49          default  is 3500. For the short_paths and heavy_branch methods,
50          this  threshold is an upper bound. Therefore, a default of 2000
51          is set to obtain a meaningful result. Any value lower than 2000
52          is  corrected  to this default. This value is also relevant for
53          dead-end  computations.  In  a dead-end, the threshold for each
54          image  computation (of a disjunct of Reached) is five times the
55          frontier    approximation    threshold.   When   the   frontier
56          approximation  threshold  is 0, the threshold for each dead-end
57          image computation is 5000.
58
59   hd_approx_quality <double>
60          This  option  specifies the quality factor for the under_approx
61          and  remap_ua  methods.  Default value is 1.0. The range is any
62          double  value  greater  than 0. Smaller quality factors produce
63          smaller results. Meaningful values are between 1 and 2.
64
65   hd_approx_bias_quality <double>
66          This  option  specifies  the  quality factor for the biased_rua
67          method.  Default  value  is  0.5. The range is any double value
68          greater   than  0.  Smaller  quality  factors  produce  smaller
69          results. Meaningful values are between 0 and 1.
70
71   hd_dead_end <method>
72          This option specifies the method used for dead-end computation.
73          A  "dead-end" is characterized by an empty frontier. A dead-end
74          computation  involves  generating  new  states from the reached
75          set.
76
77          Methods:
78
79          brute_force : Computes the image of the entire reached set. May
80          be fatal if the reached set is very large.
81
82          conjuncts   :  (Default)  Computes  the  image  of  reached  by
83          decomposing into parts.
84
85          hybrid  :  Computes the image of a subset of reached. If no new
86          states, then the reaminder is decomposed in parts.
87
88   hd_dead_end_approx_method <method>
89          This  option  allows  the  specification  of  the approximation
90          method to use to compute the subset of Reached at the dead-end.
91          The threshold used is the same as hd_frontier_approx_threshold.
92
93          For  methods,  refer hd_frontier_approx_method methods. Default
94          is remap_ua.
95
96   hd_no_scrap_states
97          This  allows the option of not adding the "scrap" states. Scrap
98          states are residues from the approximation of the frontier set.
99          Default is to add the scrap states.
100
101   hd_new_only
102          This allows the option of adding considering only new states of
103          each  iteration for image computation. The default is to take a
104          set in the interval of the new states and the reached set.
105
106   hd_only_partial_image
107          This  allows  the  option  of HD with partial image computation
108          only  (no  approximation  of  the  frontier set). Default is to
109          allow  both  partial  images  and approximation of the frontier
110          set.
111
112   Partial Image options:
113
114   hd_partial_image_method <method>
115          This  option  allows  the  image computation to approximate the
116          image with the specified method.
117
118          Methods:
119
120          approx    :    (Default)    Computes   a   partial   image   by
121          under-approximating   the   intermediate   products   of  image
122          computation.
123
124          clipping  : Computes a partial image by "clipping" the depth of
125          recursion   of   the  and-abstract  computations  during  image
126          computation.
127
128   hd_partial_image_threshold <number>
129          This  options allows the specification of a threshold (in terms
130          of bdd node size of the intermediate product) that will trigger
131          approximation  of  the intermediate product. Default is 200000.
132          This    option   has   to   be   used   in   conjunction   with
133          hd_partial_image_size. If the value of hd_partial_image_size is
134          larger   than  this  option,  then  the  approximation  of  the
135          intermediate size will be as large as the hd_partial_image_size
136          number.
137
138   hd_partial_image_size <number>
139          This  options  allows  the specification of a size (in terms of
140          bdd  node  size of the intermediate product) that is the target
141          size  of  the  approximated  intermediate  product.  Default is
142          100000.  For the short_paths and heavy_branch methods, the size
143          of  the  approximation  is  corrected  to  10000  if  the  size
144          specified  is  lower.  This  is  because  the  short_paths  and
145          heavy_branch  methods  consider  this size as an upper bound on
146          the  approximation.  This  option has to be used in conjunction
147          with    hd_partial_image_threshold.    If    the    value    of
148          hd_partial_image_threshold  is  much  larger  than this option,
149          then the desired size will not be obtained as approximation may
150          not be triggered.
151
152   hd_partial_image_approx <method>
153          This  options allows the specification of the method to be used
154          to approximate the intermediate product.
155
156          For  methods,  refer hd_frontier_approx_method methods. Default
157          is remap_ua.
158
159   hd_partial_image_approx_quality <double>
160          This  option  specifies the quality factor for the under_approx
161          and  remap_ua  methods  for  partial image computation. Default
162          value  is  1.0.  Range  of values is any double greater than 0.
163          Smaller  quality  factors  produce  smaller results. Meaningful
164          values are between 1 and 2.
165
166   hd_partial_image_approx_bias_quality <double>
167          This  option  specifies  the  quality factor for the biased_rua
168          method  for  partial  image  computation. Default value is 0.5.
169          Range  of  values is any double greater than 0. Smaller quality
170          factors  produce smaller results. Meaningful values are between
171          0 and 1.
172
173   hd_partial_image_clipping_depth <double>
174          This  option allows the specification of the depth at which the
175          recursion  can  be  clipped  when  _hd_partial_image_method_ is
176          clipping.  Range  of  values  is  between 0 and 1. The clipping
177          depth  is  then  calculated  as  the  specified fraction of the
178          number of variables. Default is 0.4.
179     _________________________________________________________________
180
181   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.