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