source: vis_dev/vis-2.1/share/help/bounded_model_checkCmd.txt @ 14

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

Add vis
File size: 5.4 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>]
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
138References
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
Note: See TracBrowser for help on using the repository browser.