[11] | 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 | |
---|
| 160 | References |
---|
| 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 |
---|