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