source: vis_dev/vis-2.3/share/help/compute_reachCmd.txt @ 31

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

vis2.3

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