[11] | 1 | |
---|
| 2 | bounded_model_check - Performs a SAT-based LTL model checking on a flattened |
---|
| 3 | network |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | bounded_model_check [-h] [-v <verbosity_level>] [-m <minimum_length>] |
---|
| 7 | [-k <maximum_length>] [-s <step_value>] [-r <termination_check_step>] |
---|
| 8 | [-e] [-F <fairness_file>] [-S <sat_solver>] [-E <encoding>] [-C |
---|
| 9 | <clause_type>] [-I <inc_level>] [-d <dbg_level>] [-t <timeOutPeriod>] |
---|
| 10 | [-o <cnf_file>] [-i] <ltl_file> |
---|
| 11 | |
---|
| 12 | Performs a SAT-based LTL bounded model checking (BMC) on a flattened |
---|
| 13 | network. This command looks for a counterexample of length k ( |
---|
| 14 | minimum_length =< k =< maximum_length). If -r is specified, this |
---|
| 15 | command performs check for termination after each |
---|
| 16 | termination_check_step . If no counterexample is found, this command |
---|
| 17 | increases k by step_value (specifies by the -s option) until a |
---|
| 18 | counterexample is found, the search becomes intractable (timed out), |
---|
| 19 | or k reaches a bound (determine by the check for termination), and |
---|
| 20 | then we conclude that the LTL property passes. This command implements |
---|
| 21 | the basic encoding of Bounded Model Checking (BMC) as descibed in the |
---|
| 22 | paper "Symbolic Model Checking without BDDs". However, the -E option |
---|
| 23 | can be used to select other encoding scheme. We also applied some of |
---|
| 24 | the improvements in the BMC encoding described in the paper "Improving |
---|
| 25 | the Encoding of LTL Model Checking into SAT". To prove that an LTL |
---|
| 26 | property passes, we implement the termination methods that are |
---|
| 27 | descirebed in the papers "Checking Safety Properties Using Induction |
---|
| 28 | and a SAT-Solver" and "Proving More Properties with Bounded Model |
---|
| 29 | Checking". Before calling this command, the user should have |
---|
| 30 | initialized the design by calling the command [1]flatten_hierarchy. If |
---|
| 31 | the user uses the -r option and the LTL property is a general LTL |
---|
| 32 | property, the command [2]build_partition_maigs must be called. The aig |
---|
| 33 | graph must be built by calling the command [3]build_partition_mdds |
---|
| 34 | |
---|
| 35 | Command options: |
---|
| 36 | |
---|
| 37 | -h |
---|
| 38 | Print the command usage. |
---|
| 39 | |
---|
| 40 | -m <minimum_length> |
---|
| 41 | Minimum length of counterexample to be checked (default is 0). |
---|
| 42 | |
---|
| 43 | -k <maximum_length> |
---|
| 44 | Maximum length of counterexample to be checked (default is 1). |
---|
| 45 | |
---|
| 46 | -s <step_value> |
---|
| 47 | Incrementing value of counterexample length (default is 1). |
---|
| 48 | |
---|
| 49 | -r <termination_check_step> |
---|
| 50 | Check for termination for each termination_check_step (default |
---|
| 51 | is 0). 0 means don't check for termination. |
---|
| 52 | |
---|
| 53 | -e |
---|
| 54 | Activate early termination check. Check if there is no simple |
---|
| 55 | path starts from an initial state. Valid only for general LTL |
---|
| 56 | and safety properties. Must be used with -r option. |
---|
| 57 | |
---|
| 58 | -S <sat_solver> |
---|
| 59 | Specify SAT solver |
---|
| 60 | sat_solver must be one of the following: |
---|
| 61 | |
---|
| 62 | 0: CirCUs (Default) |
---|
| 63 | |
---|
| 64 | 1: zChaff |
---|
| 65 | |
---|
| 66 | -E <encoding> |
---|
| 67 | Specify encoding scheme |
---|
| 68 | encoding must be one of the following: |
---|
| 69 | |
---|
| 70 | 0: The original BMC encoding (Default) |
---|
| 71 | |
---|
| 72 | 1: SNF encoding |
---|
| 73 | |
---|
| 74 | 2: Fixpoint encoding |
---|
| 75 | |
---|
| 76 | -C <clause_type> |
---|
| 77 | Specify clause type |
---|
| 78 | encoding must be one of the following: |
---|
| 79 | |
---|
| 80 | 0: Apply CirCUs SAT solver on circuit (Default) |
---|
| 81 | |
---|
| 82 | 1: Apply SAT solver on CNF generated form circuit |
---|
| 83 | |
---|
| 84 | 2: Apply SAT solver on CNF |
---|
| 85 | |
---|
| 86 | -I <inc_level> |
---|
| 87 | Specify increment sat solver type |
---|
| 88 | encoding must be one of the following: |
---|
| 89 | |
---|
| 90 | 1: Trace Objective (Default) |
---|
| 91 | |
---|
| 92 | 2: Distill |
---|
| 93 | |
---|
| 94 | 3: Trace Objective + Distill |
---|
| 95 | |
---|
| 96 | -F <fairness_file> |
---|
| 97 | Read fairness constraints from <fairness_file>. Each formula in |
---|
| 98 | the file is a condition that must hold infinitely often on a |
---|
| 99 | fair path. |
---|
| 100 | |
---|
| 101 | -o <cnf_file> Save CNF formula in <cnf_file> |
---|
| 102 | -t <timeOutPeriod> |
---|
| 103 | Specify the time out period (in seconds) after which the |
---|
| 104 | command aborts. By default this option is set to infinity. |
---|
| 105 | |
---|
| 106 | -v <verbosity_level> |
---|
| 107 | Specify verbosity level. This sets the amount of feedback on |
---|
| 108 | CPU usage and code status. |
---|
| 109 | verbosity_level must be one of the following: |
---|
| 110 | |
---|
| 111 | 0: No feedback provided. This is the default. |
---|
| 112 | |
---|
| 113 | 1: Feedback on code location. |
---|
| 114 | |
---|
| 115 | 2: Feedback on code location and CPU usage. |
---|
| 116 | |
---|
| 117 | -d <dbg_level> |
---|
| 118 | Specify the amount of debugging performed when the BMC models |
---|
| 119 | check the LTL formula. |
---|
| 120 | |
---|
| 121 | dbg_level must be one of the following: |
---|
| 122 | |
---|
| 123 | 0: No debugging performed. dbg_level=0 is the default. |
---|
| 124 | |
---|
| 125 | 1: Debugging with minimal output: generate counter-example if |
---|
| 126 | the LTL formula fails and the counterexample length. |
---|
| 127 | |
---|
| 128 | -i |
---|
| 129 | Print input values causing transitions between states during |
---|
| 130 | debugging. |
---|
| 131 | |
---|
| 132 | <ltl_file> |
---|
| 133 | File containing LTL formulae to be checked. |
---|
| 134 | _________________________________________________________________ |
---|
| 135 | |
---|
| 136 | Last updated on 20050519 10h16 |
---|
| 137 | |
---|
| 138 | References |
---|
| 139 | |
---|
| 140 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
| 141 | 2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html |
---|
| 142 | 3. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_mddsCmd.html |
---|