source: vis_dev/vis-2.1/share/help/compute_reachCmd.txt @ 15

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

Add vis
File size: 8.2 KB
Line 
1
2  compute_reach - compute the set of reachable states of the FSM
3     _________________________________________________________________
4
5   compute_reach  [-d  <depthValue>]  [-f]  [-g  <file>]  [-h]  [-i]  [-r
6   <thresholdValue>]  [-s  <printStep>] [-t <timeOut>] [-v #] [-A #] [-D]
7   [-F]
8
9   Compute  the  set  of  reachable states of the FSM associated with the
10   flattened  network.  The command build_partition_mdds (or init_verify)
11   must  have  already been invoked on the flattened network, before this
12   command is called. On subsequent calls to compute_reach, the reachable
13   states will not be recomputed, but statistics can be printed using -v.
14   To  force recomputation with a different set of options, for example a
15   depth value with -d, use -F option.
16
17   The method used for image computation is displayed by the option -v 1.
18   To   change   the  image  computation  method,  use  the  command  set
19   image_method, and then start again with the command flatten_hierarchy.
20   The reachability computation makes extensive use of image computation.
21   There are several user-settable options that can be used to affect the
22   performance  of  image  computation. See the documentation for the set
23   command for these options.
24
25   Command options:
26
27   -d <depthValue>
28          Perform  reachability  for  depthValue steps only - this option
29          specifies the number of unit operations (image computations) to
30          be  performed  in  the reachability computation. The depthValue
31          used  in successive calls proceeds from the previous state. For
32          example, compute_reach -d 3; compute_reach -d 4; will perform 7
33          steps   of   reachability   in   total,   the  second  call  to
34          compute_reach  proceeding  from  the result of the first. While
35          using only -A 0 option (default), this additionally corresponds
36          to  the  depth  in  the  state graph, starting from the initial
37          state.  For  the  -A  1 option, the above may not be true. This
38          option is not compatible with -A 2.
39
40   -f
41          Store  the set of new states (onion rings) reached at each step
42          of   reachability.   If   this  flag  is  specified,  then  the
43          computation proceeds with the previously set of onion rings, if
44          any exist (not any prior computation without onion rings). This
45          option  is  likely  to  use  more  memory  during  reachability
46          analysis. This is not compatible with -A 2.
47
48   -g <hints_file>
49          Use  guided  search.  The  file hints_file contains a series of
50          hints.  A  hint is a formula that does not contain any temporal
51          operators,  so  hints_file  has  the  same  syntax as a file of
52          invariants  used for check_invariant. The hints are used in the
53          order  given  to change the transition relation. The transition
54          relation   is   conjoined   with   the   hint   to   yield   an
55          underapproximation of the transition relation. If the hints are
56          cleverly   chosen,   this   may   speed   up   the  computation
57          considerably,  because  a  search  with  the changed transition
58          relation  may  be  much  simpler  than  one  with  the original
59          transition  relation,  and  results  obtained can be reused, so
60          that  we  may  never  have  to  do an expensive search with the
61          original  relation.  See  also:  Ravi  and  Somenzi,  Hints  to
62          accelerate  symbolic  traversal.  CHARME'99;  Bloem,  Ravi, and
63          Somenzi,  Efficient  Decision  Procedures for Model Checking of
64          Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi,
65          Symbolic  Guided  Search  for  CTL  Model Checking, DAC'00. Not
66          allowed  with  -A  2  or  -i, and will only work with iwls95 or
67          monolithic  image  methods. The description of some options for
68          guided   search   can   be   found   in   the   help  page  for
69          print_guided_search_options.
70
71   -h
72          Print the command usage.
73
74   -i
75          This  option  is  useful  when  it's  not possible to build the
76          complete transition relation. Using this option, the transition
77          relation  is  rebuilt  at  every  itereation  using the current
78          reached  set  of  states  as  the  care set. This option is not
79          compatible  with  the  -A > 0 options, the -D option and the -g
80          option.
81
82   -r <thresholdValue>
83          Dynamic  reordering (with method sift) is invoked once when the
84          size of the reachable state set reaches the threshold value.
85
86   -s <printStep>
87          At  every  printStep of the reachability computation, print the
88          total  number  of  states reached thus far, and the size of the
89          MDD representing this set.
90
91   -t <timeOut>
92          Time  allowed  to perform reachability (in seconds). Default is
93          infinity.
94
95   -v #
96          Print debug information.
97          0: (default) Nothing is printed out.
98
99          1:   Print   a   summary  of  reachability  analysis  and  some
100          information   about   the   image   computation   method   (see
101          print_img_info) and summarizes results of reachability:
102
103          FSM depth: the farthest reachable state
104          reachable states: the number of reachable states
105          MDD size: the size of the MDD representing the reachable states
106          analysis  time:  number  of  CPU  seconds  taken to compute the
107          reachable states
108
109          2: Prints the detailed information about reachability analysis.
110          For  each  printStep,  it  prints the MDD size of the reachable
111          state set and the number of states in the set.
112
113   -A #
114          This  option  allows  specification of approximate reachability
115          computation.
116
117          0:  (default) Breadth First Search. No approximate reachability
118          computation.
119
120          1:  High Density Reachability Analysis (HD). Computes reachable
121          states  in  a manner that keeps BDD sizes under control. May be
122          faster than BFS in some cases. For larger circuits, this option
123          should  compute  more reachable states. For help on controlling
124          options  for  HD, look up help on the command: print_hd_options
125          [1]print_hd_options.  Refer  to Ravi and Somenzi, ICCAD95. This
126          option  is  available  only  when  VIS  is linked with the CUDD
127          package.
128
129          2.   Approximate   Reachability   Don't  Cares(ARDC).  Computes
130          over-approximate  reachable  states.  For  help  on controlling
131          options    for   ARDC,   look   up   help   on   the   command:
132          print_ardc_options  [2]print_ardc_options.  Refer Moon's paper,
133          ICCAD98  and 2 papers by Cho et al, December TCAD96: one is for
134          State  Space Decomposition and the other is for Approximate FSM
135          Traversal.  The  options  -d, -g and -f are not compatible with
136          this option.
137
138   -D
139          First  compute  an  overapproximation  to the reachable states.
140          Minimize transition relation using this approximation, and then
141          compute   the   set  of  reachable  states  exactly.  This  may
142          accelerate reachability analysis. Refer to the paper by Moon et
143          al,  ICCAD98.  The BDD minimizing method can be chosen by using
144          "set   image_minimize_method   "   [3]set.   This   option   is
145          incompatible with -i.
146
147   -F
148          Force to recompute reachable states.
149
150   Related "set" options:
151
152   rch_simulate <#>
153          The  set  option  can  be used to set this flag rch_simulate to
154          specify  the  number of random vectors to be simulated. Default
155          value for this number is 0.
156            __________________________________________________________
157
158          Last updated on 20050519 10h16
159
160References
161
162   1. file://localhost/projects/development/hsv/vis/common/doc/html/print_hd_optionsCmd.html
163   2. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html
164   3. file://localhost/projects/development/hsv/vis/common/doc/html/setCmd.html
Note: See TracBrowser for help on using the repository browser.