compute_reach [-d <depthValue>] [-f] [-g <file>] [-h] [-i] [-r <thresholdValue>] [-s <printStep>] [-t <timeOut>] [-v #] [-A #] [-D] [-F]Compute the set of reachable states of the FSM associated with the flattened network. The command build_partition_mdds (or init_verify) must have already been invoked on the flattened network, before this command is called. On subsequent calls to compute_reach, the reachable states will not be recomputed, but statistics can be printed using -v. To force recomputation with a different set of options, for example a depth value with -d, use -F option.
The method used for image computation is displayed by the option -v 1. To change the image computation method, use the command set image_method, and then start again with the command flatten_hierarchy. The reachability computation makes extensive use of image computation. There are several user-settable options that can be used to affect the performance of image computation. See the documentation for the set command for these options.
Command options:
hints_file> hints_file contains a series of hints. A hint is
a formula that does not contain any temporal operators, so
hints_file has the same syntax as a file of invariants
used for check_invariant. The hints are used in the order given to
change the transition relation. The transition relation is
conjoined with the hint to yield an underapproximation of the
transition relation. If the hints are cleverly chosen, this may
speed up the computation considerably, because a search with the
changed transition relation may be much simpler than one with the
original transition relation, and results obtained can be reused, so
that we may never have to do an expensive search with the original
relation. See also: Ravi and Somenzi, Hints to accelerate symbolic
traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision
Procedures for Model Checking of Linear Time Logic Properties,
CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL
Model Checking, DAC'00. Not allowed with -A 2 or -i, and will only
work with iwls95 or monolithic image methods. The description of
some options for guided search can be found in the help page for
print_guided_search_options.
1: Print a summary of reachability analysis and some information about the image computation method (see print_img_info) and summarizes results of reachability:
2: Prints the detailed information about reachability analysis. For each printStep, it prints the MDD size of the reachable state set and the number of states in the set.
0: (default) Breadth First Search. No approximate reachability computation.
1: High Density Reachability Analysis (HD). Computes reachable
states in a manner that keeps BDD sizes under control. May be faster
than BFS in some cases. For larger circuits, this option should
compute more reachable states. For help on controlling options for
HD, look up help on the command: print_hd_options . Refer to Ravi and Somenzi,
ICCAD95. This option is available only when VIS is linked with the CUDD
package.
2. Approximate Reachability Don't Cares(ARDC). Computes
over-approximate reachable states. For help on controlling options
for ARDC, look up help on the command: print_ardc_options . Refer Moon's paper, ICCAD98 and
2 papers by Cho et al, December TCAD96: one is for State Space
Decomposition and the other is for Approximate FSM Traversal. The
options -d, -g and -f are not compatible with this option.
Last updated on 20050519 00h50