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

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

vis2.3
File size: 7.7 KB
RevLine 
[14]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.