[11] | 1 | |
---|
| 2 | check_invariant - check all states reachable in flattened network satisfy |
---|
| 3 | specified invariants |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | check_invariant [-c] [-d <dbg_level>] [-g <hints_file>] [-f] [-h] [-i] |
---|
| 7 | [-m] [-r] [-t <time_out_period>] [-v <verbosity_level>] [-A |
---|
| 8 | <reachability_analysis_type>] [-D] <invar_file> |
---|
| 9 | |
---|
| 10 | Performs invariant checking on a flattened network. Before calling |
---|
| 11 | this command, the user should have initialized the design by calling |
---|
| 12 | the command [1]init_verify. |
---|
| 13 | |
---|
| 14 | If the option -A3 (abstraction refinement method GRAB) is used, the |
---|
| 15 | command [2]build_partition_maigs should also have been executed. |
---|
| 16 | However, in this case, the default BDD manager and network partition |
---|
| 17 | are not mandatory, though they will be used if available. (In other |
---|
| 18 | words, the user must run the commands [3]flatten_hierarchy and |
---|
| 19 | [4]build_partition_maigs, but doesn't have to run the commands |
---|
| 20 | [5]static_order and [6]build_partition_mdds before calling this |
---|
| 21 | command.) For extremely large networks, it is actually favorable not |
---|
| 22 | to build them for the entire concrete model, but let this procedure |
---|
| 23 | assign bdd ids and construct the partition incrementally. |
---|
| 24 | |
---|
| 25 | Option -A4 means abstraction refinement approach using puresat |
---|
| 26 | algorithm, which is entirely based on SAT solver. |
---|
| 27 | |
---|
| 28 | An invariant is a set of states. Checking the invariant is the process |
---|
| 29 | of determining that all states reachable from the initial states lie |
---|
| 30 | in the invariant. |
---|
| 31 | |
---|
| 32 | One way of defining an invariant is through a CTL formula which has no |
---|
| 33 | path operators. Such formulas should be specified in the file |
---|
| 34 | invar_file. Note that the support of any wire referred to in a formula |
---|
| 35 | should consist only of latches. For the precise syntax of CTL |
---|
| 36 | formulas, see the [7]VIS CTL and LTL syntax manual. |
---|
| 37 | |
---|
| 38 | check_invariant ignores all fairness conditions associated with the |
---|
| 39 | FSM. |
---|
| 40 | |
---|
| 41 | check_invariant involves reachability analysis where at every step of |
---|
| 42 | the reachability computation all the specified invariants are checked |
---|
| 43 | in the reachable states computed thus far. If some invariant does not |
---|
| 44 | hold, a proof of failure is demonstrated. This consists of a path |
---|
| 45 | starting from an initial state to a state lying outside the invariant. |
---|
| 46 | This path is made as short as possible. For the -A 0 option or default |
---|
| 47 | -A option, it is the shortest path leading to a state outside the |
---|
| 48 | invariant. If a set of invariants is specified, the failed formulas |
---|
| 49 | are reported as soon as they are detected. The check is continued with |
---|
| 50 | the remaining invariants. |
---|
| 51 | |
---|
| 52 | Command options: |
---|
| 53 | |
---|
| 54 | -d <dbg_level> |
---|
| 55 | Specify the amount of debugging performed when the system fails |
---|
| 56 | a formula being checked. |
---|
| 57 | |
---|
| 58 | dbg_level must be one of the following: |
---|
| 59 | |
---|
| 60 | 0 : No debugging performed. This is the default. |
---|
| 61 | |
---|
| 62 | 1 : Generate a path from an initial state to a state lying |
---|
| 63 | outside the invariant. This option stores the onion rings just |
---|
| 64 | as specifying -f would have. Therefore, it may take more time |
---|
| 65 | and memory if the formula passes. This option is incompatible |
---|
| 66 | with -A 2 option. |
---|
| 67 | |
---|
| 68 | -f |
---|
| 69 | Store the set of new states (onion rings) reached at each step |
---|
| 70 | of invariant. This option is likely to use more memory but |
---|
| 71 | possibly faster results for invariants that fail. Therefore, |
---|
| 72 | the debug information for a failed invariant, if requested, may |
---|
| 73 | be provided faster. This option is not compatible with -A 2 |
---|
| 74 | options. |
---|
| 75 | |
---|
| 76 | -g <hints_file> |
---|
| 77 | Use guided search. The file hints_file contains a series of |
---|
| 78 | hints. A hint is a formula that does not contain any temporal |
---|
| 79 | operators, so hints_file has the same syntax as a file of |
---|
| 80 | invariants used for check_invariant. The hints are used in the |
---|
| 81 | order given to change the transition relation. The transition |
---|
| 82 | relation is conjoined with the hint to yield an |
---|
| 83 | underapproximation of the transition relation. If the hints are |
---|
| 84 | cleverly chosen, this may speed up the computation |
---|
| 85 | considerably, because a search with the changed transition |
---|
| 86 | relation may be much simpler than one with the original |
---|
| 87 | transition relation, and results obtained can be reused, so |
---|
| 88 | that we may never have to do an expensive search with the |
---|
| 89 | original relation. See also: Ravi and Somenzi, Hints to |
---|
| 90 | accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and |
---|
| 91 | Somenzi, Efficient Decision Procedures for Model Checking of |
---|
| 92 | Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, |
---|
| 93 | Symbolic Guided Search for CTL Model Checking, DAC'00. This |
---|
| 94 | option is not compatible with -A 2 option. The description of |
---|
| 95 | some options for guided search can be found in the help page |
---|
| 96 | for print_guided_search_options. |
---|
| 97 | |
---|
| 98 | -h |
---|
| 99 | Print the command usage. |
---|
| 100 | |
---|
| 101 | -c |
---|
| 102 | Use the formula tree so that subformulae are not shared among |
---|
| 103 | the CTL formulae in the input file. This option is useful in |
---|
| 104 | the following scenario - formulae A, B and C are being checked |
---|
| 105 | in order and there is sub-formula sharing between A and C. If |
---|
| 106 | the BDDs corresponding to the shared sub-formula is huge then |
---|
| 107 | computation for B might not be able to finish without using |
---|
| 108 | this option. |
---|
| 109 | |
---|
| 110 | -i |
---|
| 111 | Print input values causing transitions between states during |
---|
| 112 | debugging. Both primary and pseudo inputs are printed. |
---|
| 113 | |
---|
| 114 | -m |
---|
| 115 | Pipe debugger output through the UNIX utility more. |
---|
| 116 | |
---|
| 117 | -r |
---|
| 118 | Reduce the FSM derived from the flattened network with respect |
---|
| 119 | to each of the invariants in the input file. By default, the |
---|
| 120 | FSM is reduced with respect to the conjunction of the |
---|
| 121 | invariants in the input file. If this option is used and don't |
---|
| 122 | cares are being used for simplification, then subformula |
---|
| 123 | sharing is disabled (result might be incorrect otherwise). |
---|
| 124 | |
---|
| 125 | The truth of an invariant may be independant of parts of the |
---|
| 126 | network (such as when wires have been abstracted; see |
---|
| 127 | [8]flatten_hierarchy). These parts are effectively removed when |
---|
| 128 | this option is invoked; this may result in more efficient |
---|
| 129 | invariant checking. |
---|
| 130 | |
---|
| 131 | -t <timeOutPeriod> |
---|
| 132 | Specify the time out period (in seconds) after which the |
---|
| 133 | command aborts. By default this option is set to infinity. |
---|
| 134 | |
---|
| 135 | -v <verbosity_level> |
---|
| 136 | Specify verbosity level. This sets the amount of feedback on |
---|
| 137 | CPU usage and code status. |
---|
| 138 | |
---|
| 139 | verbosity_level must be one of the following: |
---|
| 140 | |
---|
| 141 | 0 : No feedback provided. This is the default. |
---|
| 142 | |
---|
| 143 | 1 : Feedback on code location. |
---|
| 144 | |
---|
| 145 | 2 : Feedback on code location and CPU usage. |
---|
| 146 | |
---|
| 147 | -A <reachability_analysis_type> |
---|
| 148 | This option allows specification of the type of reachability |
---|
| 149 | computation. |
---|
| 150 | |
---|
| 151 | 0: (default) Breadth First Search. No approximate reachability |
---|
| 152 | computation. |
---|
| 153 | |
---|
| 154 | 1: High Density Reachability Analysis (HD). Computes reachable |
---|
| 155 | states in a manner that keeps BDD sizes under control. May be |
---|
| 156 | faster than BFS in some cases. For larger circuits, this option |
---|
| 157 | could compute more reachable states than the -A 0 option for |
---|
| 158 | the same memory constraints, consequently may prove more |
---|
| 159 | invariants false. For help on controlling options for HD, look |
---|
| 160 | up help on the command: print_hd_options [9]print_hd_options. |
---|
| 161 | Refer Ravi & Somenzi, ICCAD95. The path generated for a failed |
---|
| 162 | invariant using this method may not be the shortest path. This |
---|
| 163 | option is available only when compiled with the CUDD package. |
---|
| 164 | |
---|
| 165 | 2. Approximate Reachability Don't Cares(ARDC). Computes |
---|
| 166 | over-approximated reachable states in the reachability analysis |
---|
| 167 | step. This may be faster than the -A 0 option . The invariants |
---|
| 168 | are checked in the over-approximation. This may produce false |
---|
| 169 | negatives, but these are resolved internally using the exact |
---|
| 170 | reachable states. The final results produced are the same as |
---|
| 171 | those for exact reachable states. For help on controlling |
---|
| 172 | options for ARDC, look up help on the command: |
---|
| 173 | print_ardc_options. [10]print_ardc_options Refer 2 papers in |
---|
| 174 | TCAD96 Dec. Cho et al, one is for State Space Decomposition and |
---|
| 175 | the other is for Approximate FSM Traversal. This option is |
---|
| 176 | incompatible with -d 1 and -g options. |
---|
| 177 | |
---|
| 178 | 3. The GRAB Abstraction Refinement Method. Conducts the |
---|
| 179 | reachability analysis on an abstract model. If the invariants |
---|
| 180 | are true in the abstract model, they are also true in the |
---|
| 181 | original model. If the invariants are false, the abstract |
---|
| 182 | counter-examples are used to refine the abstract model (since |
---|
| 183 | it is still inconclusive). This procedure iterates until a |
---|
| 184 | conclusive result is reached. Note that, with this option, |
---|
| 185 | "build_partitioned_mdds" and "static_order" does not have to be |
---|
| 186 | executed before calling "check_invariants," though the default |
---|
| 187 | BDD partition and order will be reused if available. (When |
---|
| 188 | checking extremely large models, skipping either or both |
---|
| 189 | "static_order" and "build_partitioned_mdds" can often make the |
---|
| 190 | verification much faster.) The grainularity of abstraction |
---|
| 191 | refinement also depends on the parameter "partition_threshold", |
---|
| 192 | which by default is 5000; one can use the VIS command "set |
---|
| 193 | partition_threshold 1000" to change its value. For experienced |
---|
| 194 | users who want to fine-tune the different parameters of GRAB, |
---|
| 195 | please try the test command "_grab_test" ("_grab_test -h" |
---|
| 196 | prints out its usage information). Refer to Wang et al., |
---|
| 197 | ICCAD2003 and ICCD2004 for more information about the GRAB |
---|
| 198 | algorithm. Note that this option is incompatible with the "-d |
---|
| 199 | 1" and "-g" options. |
---|
| 200 | |
---|
| 201 | 4. Abstraction refinement approach using puresat algorithm, |
---|
| 202 | which is entirely based on SAT solver. It has several parts: * |
---|
| 203 | Localization base Abstraction * K-induction to prove the truth |
---|
| 204 | of a property * Bounded Model Checking to find bugs * |
---|
| 205 | Incremental concretization based methods to verify abstract |
---|
| 206 | bugs * UNSAT proof based method to obtain refinement * |
---|
| 207 | Refinement minization to guarrantee a minimal refinement For |
---|
| 208 | more information, please check the BMC'03 and STTT'05 paper of |
---|
| 209 | Li et al., "A satisfiability-based appraoch to abstraction |
---|
| 210 | refinement in model checking", and " Abstraction in symbolic |
---|
| 211 | model checking using satisfiability as the only decision |
---|
| 212 | procedure" |
---|
| 213 | |
---|
| 214 | -D |
---|
| 215 | First compute an overapproximation to the reachable states. |
---|
| 216 | Minimize the transition relation using this approximation, and |
---|
| 217 | then compute the set of reachable states exactly. This may |
---|
| 218 | accelerate reachability analysis. Refer to the paper by Moon et |
---|
| 219 | al, ICCAD98. The BDD minimizing method can be chosen by using |
---|
| 220 | "set image_minimize_method " [11]set. This option is |
---|
| 221 | incompatible with -g. |
---|
| 222 | |
---|
| 223 | -F <dbg_file> |
---|
| 224 | Write the debugger output to dbg_file. |
---|
| 225 | |
---|
| 226 | <invarFile> |
---|
| 227 | File containing invariants to be checked. |
---|
| 228 | |
---|
| 229 | Related "set" options: |
---|
| 230 | |
---|
| 231 | rch_simulate <#> |
---|
| 232 | The set option can be used to set this flag rch_simulate to specify |
---|
| 233 | the number of random vectors to be simulated. Default value for this |
---|
| 234 | number is 0. |
---|
| 235 | |
---|
| 236 | ctl_change_bracket <yes/no> |
---|
| 237 | Vl2mv automatically converts "[]" to "<>" in node names, therefore CTL |
---|
| 238 | parser does the same thing. However, in some cases a user does not |
---|
| 239 | want to change node names in CTL parsing. Then, use this set option by |
---|
| 240 | giving "no". Default is "yes". |
---|
| 241 | |
---|
| 242 | See also command : compute_reach |
---|
| 243 | |
---|
| 244 | -w <node_file> This option invoked the algorithm to generate an error |
---|
| 245 | trace divided into fated and free segements. Fate represents the |
---|
| 246 | inevitability and free is asserted when there is no inevitability. |
---|
| 247 | This can be formulated as a two-player concurrent reachability game. |
---|
| 248 | The two players are the environment and the system. The node_file is |
---|
| 249 | given To specify the variables the are controlled by the system. |
---|
| 250 | |
---|
| 251 | -W |
---|
| 252 | This option represents the case that all input variables are |
---|
| 253 | controlled by system. |
---|
| 254 | |
---|
| 255 | -G |
---|
| 256 | We proposed two algorithm to generate segemented counter example. They |
---|
| 257 | are general and restrcited algorithm. Bu default we use restricted |
---|
| 258 | algorithm. We can invoke general algorithm with -G option. For more |
---|
| 259 | information, please check the STTT'04 paper of Jin et al., "Fate and |
---|
| 260 | Free Will in Error Traces" |
---|
| 261 | _________________________________________________________________ |
---|
| 262 | |
---|
| 263 | Last updated on 20050519 10h16 |
---|
| 264 | |
---|
| 265 | References |
---|
| 266 | |
---|
| 267 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html |
---|
| 268 | 2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html |
---|
| 269 | 3. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
| 270 | 4. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html |
---|
| 271 | 5. file://localhost/projects/development/hsv/vis/common/doc/html/static_orderCmd.html |
---|
| 272 | 6. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_mddsCmd.html |
---|
| 273 | 7. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html |
---|
| 274 | 8. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
| 275 | 9. file://localhost/projects/development/hsv/vis/common/doc/html/print_hd_optionsCmd.html |
---|
| 276 | 10. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html |
---|
| 277 | 11. file://localhost/projects/development/hsv/vis/common/doc/html/setCmd.html |
---|