[14] | 1 | |
---|
| 2 | bdd_sat_bounded_model_check - performs an LTL bounded model checking on a |
---|
| 3 | flattened network |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | bdd_sat_bounded_model_check [-h] [-v <verbosity_level>] [-d <dbg_level>] |
---|
| 7 | [-i] -m <minimum_length> -k <maximum_length> -s <step_value> -o <cnf_file> |
---|
| 8 | <ltl_file> |
---|
| 9 | |
---|
| 10 | Performs an LTL bounded model checking on a flattened network. This command |
---|
| 11 | looks for a counterexample of length ⥠minimum_length and †maximum_length. |
---|
| 12 | It increments the length by step_value. Before calling this command, the |
---|
| 13 | user should have initialized the design by calling the command |
---|
| 14 | [1]flatten_hierarchy, and then calling the command [2]build_partition_maigs. |
---|
| 15 | |
---|
| 16 | The value of maximum length must be >= minimum length. |
---|
| 17 | |
---|
| 18 | Command options: |
---|
| 19 | |
---|
| 20 | -h |
---|
| 21 | Print the command usage. |
---|
| 22 | |
---|
| 23 | -m <minimum_length> |
---|
| 24 | Minimum length of counterexample to be checked (default is 0). |
---|
| 25 | |
---|
| 26 | -k <maximum_length> |
---|
| 27 | Maximum length of counterexample to be checked (default is 1). |
---|
| 28 | |
---|
| 29 | -s <step_value> |
---|
| 30 | Incrementing value of counterexample length (default is 1). |
---|
| 31 | |
---|
| 32 | -r <inductive_Step> |
---|
| 33 | Use inductive proof at each step_value to check if the property |
---|
| 34 | passes (default is 0). 0 means don't use the inductive proof. BMC |
---|
| 35 | will check using the indcution if the property passes if the current |
---|
| 36 | length of the counterexample is a multiple of inductive_Step. |
---|
| 37 | |
---|
| 38 | -F <fairness_file> |
---|
| 39 | Read fairness constraints from <fairness_file>. Each formula in the |
---|
| 40 | file is a condition that must hold infinitely often on a fair path. |
---|
| 41 | |
---|
| 42 | -o <cnf_file> Save the CNF formula in <cnf_file> |
---|
| 43 | -t <timeOutPeriod> |
---|
| 44 | Specify the time out period (in seconds) after which the command |
---|
| 45 | aborts. By default this option is set to infinity. |
---|
| 46 | |
---|
| 47 | -v <verbosity_level> |
---|
| 48 | Specify verbosity level. This sets the amount of feedback on CPU |
---|
| 49 | usage and code status. |
---|
| 50 | verbosity_level must be one of the following: |
---|
| 51 | |
---|
| 52 | 0: No feedback provided. This is the default. |
---|
| 53 | |
---|
| 54 | 1: Feedback on code location. |
---|
| 55 | |
---|
| 56 | 2: Feedback on code location and CPU usage. |
---|
| 57 | |
---|
| 58 | -d <dbg_level> |
---|
| 59 | Specify the amount of debugging performed when the BMC models check |
---|
| 60 | the LTL formula. |
---|
| 61 | |
---|
| 62 | dbg_level must be one of the following: |
---|
| 63 | |
---|
| 64 | 0: No debugging performed. dbg_level=0 is the default. |
---|
| 65 | |
---|
| 66 | 1: Debugging with minimal output: generate counter-example if the LTL |
---|
| 67 | formula fails and the counterexample length. |
---|
| 68 | |
---|
| 69 | -h |
---|
| 70 | Print the command usage. |
---|
| 71 | |
---|
| 72 | -i |
---|
| 73 | Print input values causing transitions between states during |
---|
| 74 | debugging. |
---|
| 75 | |
---|
| 76 | -o <cnf_file>; |
---|
| 77 | File containing CNF of the counterexample if exist. If specifies, the |
---|
| 78 | user can exam this file looking for information about the generated |
---|
| 79 | path. This file will be the input to the SAT solver. The contents of |
---|
| 80 | this file is in dimacs format. |
---|
| 81 | |
---|
| 82 | <ltl_file> |
---|
| 83 | File containing LTL formulas to be model checked. |
---|
| 84 | _________________________________________________________________ |
---|
| 85 | |
---|
| 86 | Last updated on 20100410 00h02 |
---|
| 87 | |
---|
| 88 | References |
---|
| 89 | |
---|
| 90 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
| 91 | 2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html |
---|