[14] | 1 | |
---|
| 2 | model_check - perform fair CTL model checking on a flattened network |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | model_check [-b] [-c] [-d <dbg_level>] [-f <dbg_file>] [-g <hints_file>] |
---|
| 6 | [-h] [-i] [-m] [-r] [-t <time_out_period>][-v <verbosity_level>] [-D |
---|
| 7 | <dc_level>] [-F] [-S <schedule>] [-V] [-B] [-I] [-C] [-w <node_file>] [-W] |
---|
| 8 | [-G] <ctl_file> |
---|
| 9 | |
---|
| 10 | Performs fair CTL model 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. Regardless of the options, no 'false positives' or 'false |
---|
| 13 | negatives' will occur: the result is correct for the given circuit. |
---|
| 14 | |
---|
| 15 | Properties to be verified should be provided as CTL formulas in the file |
---|
| 16 | ctl_file. Note that the support of any wire referred to in a formula should |
---|
| 17 | consist only of latches. For the precise syntax of CTL formulas, see the |
---|
| 18 | [2]VIS CTL and LTL syntax manual. |
---|
| 19 | |
---|
| 20 | Properties of the form AG f, where f is a formula not involving path |
---|
| 21 | quantifiers are referred to as invariants; for such properties it may be |
---|
| 22 | substantially faster to use the [3]check_invariant command. |
---|
| 23 | |
---|
| 24 | A fairness constraint can be specified by invoking the [4]read_fairness |
---|
| 25 | command; if none is specified, all paths are taken to be fair. If some |
---|
| 26 | initial states do not lie on a fair path, the model checker prints a message |
---|
| 27 | to this effect. |
---|
| 28 | |
---|
| 29 | A formula passes iff it is true for all initial states of the system. |
---|
| 30 | Therefore, in the presence of multiple initial states, if a formula fails, |
---|
| 31 | the negation of the formula may also fail. |
---|
| 32 | |
---|
| 33 | If a formula does not pass, a (potentially partial) proof of failure |
---|
| 34 | (referred to as a debug trace) is demonstrated. Fair paths are represented |
---|
| 35 | by a finite sequence of states (the stem) leading to a fair cycle, i.e. a |
---|
| 36 | cycle on which there is a state from each fairness condition. The level of |
---|
| 37 | detail of the proof can be specified (see option -d). |
---|
| 38 | |
---|
| 39 | Both backward (future tense CTL formulas) and forward (past tense CTL |
---|
| 40 | formulas) model checking can be performed. Forward model checking is based |
---|
| 41 | on Iwashita's ICCAD96 paper. Future tense CTL formulas are automatically |
---|
| 42 | converted to past tense ones as much as possible in forward model checking. |
---|
| 43 | |
---|
| 44 | Command options: |
---|
| 45 | |
---|
| 46 | -b |
---|
| 47 | Use backward analysis when performing debugging; the default is to |
---|
| 48 | use forward analysis. This should be tried when the debugger spends a |
---|
| 49 | large amount of time when creating a path to a fair cycle. This |
---|
| 50 | option is not compatible with forward model checking option (-F). |
---|
| 51 | |
---|
| 52 | -c |
---|
| 53 | Use the formula tree so that there is no sharing of sub-formulae |
---|
| 54 | among the formulae in the input file. This option is useful in the |
---|
| 55 | following scenario - formulae A, B and C are being checked in order |
---|
| 56 | and there is sub-formula sharing between A and C. If the BDDs |
---|
| 57 | corresponding to the shared sub-formula is huge then computation for |
---|
| 58 | B might not be able to finish without using this option. |
---|
| 59 | |
---|
| 60 | -d <dbg_level> |
---|
| 61 | Specify the amount of debugging performed when the system fails a |
---|
| 62 | formula being checked. Note that it may not always be possible to |
---|
| 63 | give a simple counter-example to show that a formula is false, since |
---|
| 64 | this may require enumerating all paths from a state. In such a case |
---|
| 65 | the model checker will print a message to this effect. This option is |
---|
| 66 | incompatible with -F. |
---|
| 67 | |
---|
| 68 | dbg_level must be one of the following: |
---|
| 69 | |
---|
| 70 | 0: No debugging performed. dbg_level=0 is the default. |
---|
| 71 | |
---|
| 72 | 1: Debugging with minimal output: generate counter-examples for |
---|
| 73 | universal formulas (formulas of the form AX|AF|AU|AG) and witnesses |
---|
| 74 | for existential formulas (formulas of the form EX|EF|EU|EG). States |
---|
| 75 | on a path are not further analyzed. |
---|
| 76 | |
---|
| 77 | 2: Same as dbg_level=1, but more verbose. (The subformulas are |
---|
| 78 | printed, too.) |
---|
| 79 | |
---|
| 80 | 3: Maximal automatic debugging: as for level 1, except that states |
---|
| 81 | occurring on paths will be recursively analyzed. |
---|
| 82 | |
---|
| 83 | 4: Manual debugging: at each state, the user is queried if more |
---|
| 84 | feedback is desired. |
---|
| 85 | |
---|
| 86 | -f <dbg_file> |
---|
| 87 | Write the debugger output to dbg_file. This option is incompatible |
---|
| 88 | with -F. Notes: when you use -d4 (interactive mode), -f is not |
---|
| 89 | recommended, since you can't see the output of vis on stdout. |
---|
| 90 | |
---|
| 91 | -g <hints_file> |
---|
| 92 | Use guided search. The file hints_file contains a series of hints. A |
---|
| 93 | hint is a formula that does not contain any temporal operators, so |
---|
| 94 | hints_file has the same syntax as a file of invariants used for |
---|
| 95 | check_invariant. The hints are used in the order given to change the |
---|
| 96 | transition relation. In the case of least fixpoints (EF, EU), the |
---|
| 97 | transition relation is conjoined with the hint, whereas for greatest |
---|
| 98 | fixpoints the transition relation is disjoined with the negation of |
---|
| 99 | the hint. If the hints are cleverly chosen, this may speed up the |
---|
| 100 | computation considerably, because a search with the changed |
---|
| 101 | transition relation may be much simpler than one with the original |
---|
| 102 | transition relation, and results obtained can be reused, so that we |
---|
| 103 | may never have to do a complicated search with the original relation. |
---|
| 104 | Note: hints in terms of primary inputs are not useful for greatest |
---|
| 105 | fixpoints. See also: Ravi and Somenzi, Hints to accelerate symbolic |
---|
| 106 | traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision |
---|
| 107 | Procedures for Model Checking of Linear Time Logic Properties, |
---|
| 108 | CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL |
---|
| 109 | Model Checking, DAC'00. |
---|
| 110 | |
---|
| 111 | For formulae that contain both least and greatest fixpoints, the |
---|
| 112 | behavior depends on the flag guided_search_hint_type. If it is set to |
---|
| 113 | local (default) then every subformula is evaluated to completion, |
---|
| 114 | using all hints in order, before the next subformula is started. For |
---|
| 115 | pure ACTL or pure ECTL formulae, we can also set |
---|
| 116 | guided_search_hint_type to global, in which case the entire formula |
---|
| 117 | is evaluated for one hint before moving on to the next hint, using |
---|
| 118 | underapproximations. The description of the options for guided search |
---|
| 119 | can be found in the help page for print_guided_search_options. |
---|
| 120 | |
---|
| 121 | model_check will call reachability without any guided search, even if |
---|
| 122 | -g is used. If you want to perform reachability with guided search, |
---|
| 123 | call rch directly. |
---|
| 124 | |
---|
| 125 | Incompatible with -F. |
---|
| 126 | |
---|
| 127 | -h |
---|
| 128 | Print the command usage. |
---|
| 129 | |
---|
| 130 | -i |
---|
| 131 | Print input values causing transitions between states during |
---|
| 132 | debugging. Both primary and pseudo inputs are printed. This option is |
---|
| 133 | incompatible with -F. |
---|
| 134 | |
---|
| 135 | -m |
---|
| 136 | Pipe debugger output through the UNIX utility more. This option is |
---|
| 137 | incompatible with -F. |
---|
| 138 | |
---|
| 139 | -r |
---|
| 140 | Reduce the FSM derived from the flattened network with respect to |
---|
| 141 | each formula being checked. By default, the FSM is reduced with |
---|
| 142 | respect to the conjunction of the formulae in the input file. If this |
---|
| 143 | option is used and don't cares are being used for simplification, |
---|
| 144 | then subformula sharing is disabled (result might be incorrect |
---|
| 145 | otherwise). |
---|
| 146 | |
---|
| 147 | The truth of a formula may be independent of parts of the network |
---|
| 148 | (such as when wires have been abstracted; see [5]flatten_hierarchy). |
---|
| 149 | These parts are effectively removed when this option is invoked; this |
---|
| 150 | may result in more efficient model checking. |
---|
| 151 | |
---|
| 152 | -t <timeOutPeriod> |
---|
| 153 | Specify the time out period (in seconds) after which the command |
---|
| 154 | aborts. By default this option is set to infinity. |
---|
| 155 | |
---|
| 156 | -v <verbosity_level> |
---|
| 157 | Specify verbosity level. This sets the amount of feedback on CPU |
---|
| 158 | usage and code status. |
---|
| 159 | verbosity_level must be one of the following: |
---|
| 160 | |
---|
| 161 | 0: No feedback provided. This is the default. |
---|
| 162 | |
---|
| 163 | 1: Feedback on code location. |
---|
| 164 | |
---|
| 165 | 2: Feedback on code location and CPU usage. |
---|
| 166 | |
---|
| 167 | -B |
---|
| 168 | Check for vacuously passing formulae using the algorithm of Beer et |
---|
| 169 | al. (CAV97). The algorithm applies to a subset of ACTL (w-ACTL) and |
---|
| 170 | replaces the smallest important subformula of a passing property with |
---|
| 171 | either FALSE or TRUE depending on its negation parity. It then |
---|
| 172 | applies model checking to the resulting witness formula. If the |
---|
| 173 | witness formula also passes, then the original formula is deemed to |
---|
| 174 | pass vacuously. If the witness formula fails, a counterexample to it |
---|
| 175 | provides an interesting witness to the original passing formula. See |
---|
| 176 | the CAV97 paper for the definitions of w-ACTL, important subformula, |
---|
| 177 | and interesting witness. In short, one of the operands of a binary |
---|
| 178 | operator in a w-ACTL formula must be a propositional formula. See |
---|
| 179 | also the -V option. |
---|
| 180 | |
---|
| 181 | -C |
---|
| 182 | Compute coverage of all observable signals in a set of CTL formulae |
---|
| 183 | using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the |
---|
| 184 | verbosity level (-v option) is equal to 0, only the coverage stats |
---|
| 185 | are printed. If verbosity level is greater than zero, then detailed |
---|
| 186 | information of the computation at each step of the algorithm is also |
---|
| 187 | provided. Debug information is provided in the form of states not |
---|
| 188 | covered for each observable signal if the dbg_level (-d option) is |
---|
| 189 | greater than 0. The number of states printed is set by the vis |
---|
| 190 | environment variable 'nr_uncoveredstates'. By default the number of |
---|
| 191 | states printed is 1. The value of nr_uncoveredstates can be set using |
---|
| 192 | the set command. See also the -I option. |
---|
| 193 | |
---|
| 194 | -D <dc_level> |
---|
| 195 | Specify extent to which don't cares are used to simplify MDDs in |
---|
| 196 | model checking. Don't cares are minterms on which the values taken by |
---|
| 197 | functions do not affect the computation; potentially, these minterms |
---|
| 198 | can be used to simplify MDDs and reduce the time taken to perform |
---|
| 199 | model checking. The -g flag for guided search does not affect the way |
---|
| 200 | in which the don't-care conditions are computed. |
---|
| 201 | dc_level must be one of the following: |
---|
| 202 | |
---|
| 203 | 0 : No don't cares are used. |
---|
| 204 | |
---|
| 205 | 1 : Use unreachable states as don't cares. This is the default. |
---|
| 206 | |
---|
| 207 | 2 : Use unreachable states as don't cares and in the EU computation, |
---|
| 208 | use 'frontiers' for image computation. |
---|
| 209 | |
---|
| 210 | 3 : First compute an overapproximation of the reachable states |
---|
| 211 | (ARDC), and use that as the cares set. Use `frontiers' for image |
---|
| 212 | computation. For help on controlling options for ARDC, look up help |
---|
| 213 | on the command: [6]print_ardc_options. Refer to Moon, Jang, Somenzi, |
---|
| 214 | Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model |
---|
| 215 | Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD |
---|
| 216 | December 1996: one is for State Space Decomposition and the other is |
---|
| 217 | for Approximate FSM Traversal. |
---|
| 218 | |
---|
| 219 | -F |
---|
| 220 | Use forward model checking based on Iwashita's method in ICCAD96. |
---|
| 221 | Future tense CTL formulas are automatically converted to past tense |
---|
| 222 | ones as much as possible. Converted forward formulas are printed when |
---|
| 223 | verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m) |
---|
| 224 | are ignored with this option. We have seen that forward model |
---|
| 225 | checking was much faster than backward in many cases, also forward |
---|
| 226 | was much slower than backward in many cases. |
---|
| 227 | |
---|
| 228 | -I |
---|
| 229 | Compute coverage of all observable signals in a set of CTL formulae |
---|
| 230 | using an improved algorithm of Jayakumar, Purandare, Somenzi |
---|
| 231 | (DAC'03). If the verbosity level (-v option) is equal to 0, only the |
---|
| 232 | coverage stats are printed. If verbosity level is greater than zero, |
---|
| 233 | then detailed information of the computation at each step of the |
---|
| 234 | algorithm is also provided. Debug information is provided in the form |
---|
| 235 | of states not covered for each observable signal if the dbg_level (-d |
---|
| 236 | option) is greater than 0. The number of states printed is set by the |
---|
| 237 | vis environment variable 'nr_uncoveredstates'. By default the number |
---|
| 238 | of states printed is 1. The value of nr_uncoveredstates can be set |
---|
| 239 | using the set command. Compared to the -C option, this one produces |
---|
| 240 | more accurate results and deals with a larger subset of CTL. |
---|
| 241 | |
---|
| 242 | -S <schedule> |
---|
| 243 | Specify schedule for GSH algorithm, which generalizes the Emerson-Lei |
---|
| 244 | algorithm and is used to compute greatest fixpoints. The choice of |
---|
| 245 | schedule affects the sequence in which EX and EU operators are |
---|
| 246 | applied. It makes a difference only when fairness constraints are |
---|
| 247 | specified. |
---|
| 248 | <schedule> must be one of the following: |
---|
| 249 | |
---|
| 250 | EL : EU and EX operators strictly alternate. This is the default. |
---|
| 251 | |
---|
| 252 | EL1 : EX is applied once for every application of all EUs. |
---|
| 253 | |
---|
| 254 | EL2 : EX is applied repeatedly after each application of all EUs. |
---|
| 255 | |
---|
| 256 | budget : a hybrid of EL and EL2. |
---|
| 257 | |
---|
| 258 | random : enabled operators are applied in (pseudo-)random order. |
---|
| 259 | |
---|
| 260 | off : GSH is disabled, and the old algorithm is used instead. The old |
---|
| 261 | algorithm uses the EL schedule, but the termination checks are less |
---|
| 262 | sophisticated than in GSH. |
---|
| 263 | |
---|
| 264 | -V |
---|
| 265 | Check for vacuously passing formulae with the algorithm of Purandare |
---|
| 266 | and Somenzi (CAV2002). The algorithm applies to all of CTL, and to |
---|
| 267 | both passing and failing properties. It says whether a passing |
---|
| 268 | formula may be strengthened and still pass, and whether a failing |
---|
| 269 | formula may be weakened and still fail. It considers all leaves of a |
---|
| 270 | formula that are under one negation parity (e.g., not descendants of |
---|
| 271 | a XOR or EQ node) for replacement by either TRUE or FALSE. See also |
---|
| 272 | the -B option. |
---|
| 273 | |
---|
| 274 | -w <node_file> This option invoked the algorithm to generate an error trace |
---|
| 275 | divided into fated and free segements. Fate represents the |
---|
| 276 | inevitability and free is asserted when there is no inevitability. |
---|
| 277 | This can be formulated as a two-player concurrent reachability game. |
---|
| 278 | The two players are the environment and the system. The node_file is |
---|
| 279 | given to specify the variables the are controlled by the system. |
---|
| 280 | |
---|
| 281 | -W |
---|
| 282 | This option represents the case that all input variables are controlled by |
---|
| 283 | system. |
---|
| 284 | |
---|
| 285 | -G |
---|
| 286 | We proposed two algorithm to generate segemented counter example. They are |
---|
| 287 | general and restrcited algorithm. Bu default we use restricted |
---|
| 288 | algorithm. We can invoke general algorithm with -G option. For more |
---|
| 289 | information, please check the STTT'04 paper of Jin et al., "Fate and |
---|
| 290 | Free Will in Error Traces" |
---|
| 291 | |
---|
| 292 | <ctl_file> |
---|
| 293 | File containing CTL formulas to be model checked. |
---|
| 294 | |
---|
| 295 | Related "set" options: |
---|
| 296 | |
---|
| 297 | ctl_change_bracket <yes/no> |
---|
| 298 | Vl2mv automatically converts "[]" to "<>" in node names, therefore |
---|
| 299 | CTL parser does the same thing. However, in some cases a user does |
---|
| 300 | not want to change node names in CTL parsing. Then, use this set |
---|
| 301 | option by giving "no". Default is "yes". |
---|
| 302 | |
---|
| 303 | guided_search_hint_type |
---|
| 304 | Switches between local and global hints (see the -g option, or the |
---|
| 305 | help page for set). |
---|
| 306 | |
---|
| 307 | See also commands : approximate_model_check, incremental_ctl_verification |
---|
| 308 | _________________________________________________________________ |
---|
| 309 | |
---|
| 310 | Last updated on 20100410 00h02 |
---|
| 311 | |
---|
| 312 | References |
---|
| 313 | |
---|
| 314 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html |
---|
| 315 | 2. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html |
---|
| 316 | 3. file://localhost/projects/development/hsv/vis/common/doc/html/check_invariantCmd.html |
---|
| 317 | 4. file://localhost/projects/development/hsv/vis/common/doc/html/read_fairnessCmd.html |
---|
| 318 | 5. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
| 319 | 6. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html |
---|