[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 | |
---|
| 150 | References |
---|
| 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 |
---|