source: vis_dev/vis-2.3/share/help/bounded_model_checkCmd.txt @ 82

Last change on this file since 82 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 5.2 KB
Line 
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
136References
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
Note: See TracBrowser for help on using the repository browser.