source: vis_dev/vis-2.3/share/help/ltl_model_checkCmd.txt @ 41

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

vis2.3
File size: 8.6 KB
Line 
1
2  ltl_model_check - perform LTL model checking on a flattened network
3     _________________________________________________________________
4
5   ltl_model_check  [-a  <ltl2aut_algorithm>]  [-b]  [-d <dbg_level>] [-f
6   <dbg_file>] [-h] [-i] [-m] [-s] [-t <time_out_period>][-v <verbosity_level>]
7   [-A <le_method>] [-D <dc_level>] [-L <lockstep_mode>] [-S <schedule>] [-F]
8   [-X] [-Y] [-M] <ltl_file>
9
10   Performs LTL model checking on a flattened network. Before calling this
11   command, the user should have initialized the design by calling the command
12   [1]init_verify. Regardless of the options, no 'false positives' or 'false
13   negatives' will occur: the result is correct for the given circuit.
14
15   Properties to be verified should be provided as LTL formulae in the file
16   ltl_file. Note that the support of any wire referred to in a formula should
17   consist only of latches. For the precise syntax of LTL formulas, see the
18   [2]VIS CTL and LTL syntax manual.
19
20   A  formula passes iff it is true for all initial states of the system.
21   Therefore, in the presence of multiple initial states, if a formula fails,
22   the negation of the formula may also fail.
23
24   If  a  formula does not pass, a (potentially partial) proof of failure
25   (referred to as a debug trace) is demonstrated. Fair paths are represented
26   by a finite sequence of states (the stem) leading to a fair cycle, i.e. a
27   cycle  on which there is a state from each fairness condition. Whether
28   demostrate the proof or not can be specified (see option -d).
29
30   Command options:
31
32   -a <ltl2aut_algorithm>
33          Specify  the  algorithm used in LTL formula -> Buechi automaton
34          translation.
35
36          ltl2aut_algorithm must be one of the following:
37
38          0: GPVW.
39
40          1: GPVW+.
41
42          2: LTL2AUT.
43
44          3: WRING (default).
45
46   -b
47          Use boolean minimization during the LTL to Automaton translation.
48
49   -d <dbg_level>
50          Specify whether to demonstrate a counter-example when the system
51          fails a formula being checked.
52
53          dbg_level must be one of the following:
54
55          0: No debugging performed. dbg_level=0 is the default.
56
57          1: Generate a counter-example (a path to a fair cycle).
58
59   -f <dbg_file>
60          Write the debugger output to dbg_file.
61
62   -h
63          Print the command usage.
64
65   -i
66          Print  input  values  causing transitions between states during
67          debugging. Both primary and pseudo inputs are printed.
68
69   -m
70          Pipe debugger output through the UNIX utility more.
71
72   -t <timeOutPeriod>
73          Specify the time out period (in seconds) after which the command
74          aborts. By default this option is set to infinity.
75
76   -s
77          Print debug output in the format accepted by the [3]simulate command.
78
79   -v <verbosity_level>
80          Specify verbosity level. This sets the amount of feedback on CPU
81          usage and code status.
82          verbosity_level must be one of the following:
83
84          0: No feedback provided. This is the default.
85
86          1: Feedback on code location.
87
88          2: Feedback on code location and CPU usage.
89
90   -A <le_method>
91          Specify whether the compositional SCC analysis algorithm, Divide and
92          Compose (DnC), is enabled for language emptiness checking. The DnC
93          algorithm first enumerates fair SCCs in an over-approximated abstract
94          model,  and then successively refines them in the more concrete
95          models. Since non-fair SCCs can be ignored in the more concrete
96          models, a potentially large part of the state space are pruned away
97          early on when the computations are cheap.
98
99          le_method must be one of the following:
100
101          0 : no use of Divide and Compose (Default).
102
103          1 : use Divide and Compose.
104
105   -D <dc_level>
106          Specify extent to which don't cares are used to simplify MDDs in
107          model checking. Don't cares are minterms on which the value taken by
108          functions  does  not affect the computation; potentially, these
109          minterms can be used to simplify MDDs and reduce the time taken to
110          perform model checking.
111          dc_level must be one of the following:
112
113          0 : No don't cares are used.
114
115          1 : Use unreachable states as don't cares. This is the default.
116
117          2 : Use unreachable states as don't cares and in the EU computation,
118          use 'frontiers' for image computation.
119
120          3  : First compute an overapproximation of the reachable states
121          (ARDC), and use that as the cares set. Use `frontiers' for image
122          computation. For help on controlling options for ARDC, look up help
123          on the command: [4]print_ardc_options. Refer to Moon, Jang, Somenzi,
124          Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model
125          Checking",  ICCAD98,  and to two papers by Cho et al, IEEE TCAD
126          December 1996: one is for State Space Decomposition and the other is
127          for Approximate FSM Traversal.
128
129   -S <schedule>
130          Specify schedule for GSH algorithm, which generalizes the Emerson-Lei
131          algorithm and is used to compute greatest fixpoints. The choice of
132          schedule  affects the sequence in which EX and EU operators are
133          applied. It makes a difference only when fairness constraints are
134          specified.
135          <schedule> must be one of the following:
136
137          EL : EU and EX operators strictly alternate. This is the default.
138
139          EL1 : EX is applied once for every application of all EUs.
140
141          EL2 : EX is applied repeatedly after each application of all EUs.
142
143          budget : a hybrid of EL and EL2
144
145          random : enabled operators are applied in (pseudo-)random order.
146
147          off : GSH is disabled, and the old algorithm is used instead. The old
148          algorithm  uses  the  EL  , but the termination checks are less
149          sophisticated than in GSH.
150
151   -F
152          Use forward analysis in the computation of the greatest fixpoint.
153          This option is incompatible with -d 1 or higher and can only be used
154          with -D 1.
155
156   -L <lockstep_mode>
157          Use the lockstep algorithm, which is based on fair SCC enumeration.
158          <lockstep_mode> must be one of the following:
159
160          off : Lockstep is disabled. This is the default. Language emptiness
161          is checked by computing a hull of the fair SCCs.
162
163          on : Lockstep is enabled.
164
165          all : Lockstep is enabled; all fair SCCs are enumerated instead of
166          terminating as soon as one is found. This can be used to study the
167          SCCs of a graph, but it is slower than the default option.
168
169          n : (n is a positive integer). Lockstep is enabled and up to n fair
170          SCCs are enumerated. This is less expensive than all , but still less
171          efficient than on , even when n = 1 .
172
173   -X
174          Disable strength reduction (use different decision procedures for
175          strong, weak, and terminal automaton). Strength reduction is the
176          default.  Refer  to  Bloem,  Ravi, Somenzi, "Efficient Decision
177          Procedures for LTL Model Checking," CAV99.
178
179   -Y
180          Disable incremental construction of the partition for (MxA). Instead,
181          build a new partition from the scratch. Incremental construction of
182          the partition is the default.
183
184   -Z
185          Add arcs into the Buechi automaton by direct simulation relation, to
186          heuristically reduce the length of shortest counter-example in model
187          checking. Refer to Awedh and Somenze, "Proving More Properties with
188          Bounded Model Checking," CAV04.
189
190   -M
191          Maximize (adding arcs to) Buechi automaton using Direct Simulation.
192
193   <ltl_file>
194          File containing LTL formulas to be model checked.
195
196   Related "set" options:
197
198   ltl_change_bracket <yes/no>
199          Vl2mv automatically converts "[]" to "<>" in node names, therefore
200          CTL* parser does the same thing. However, in some cases a user does
201          not want to change node names in CTL* parsing. Then, use this set
202          option by giving "no". Default is "yes".
203
204          See   also  commands  :  model_check,  approximate_model_check,
205          incremental_ctl_verification
206            __________________________________________________________
207
208          Last updated on 20100410 00h02
209
210References
211
212   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
213   2. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
214   3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html
215   4. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html
Note: See TracBrowser for help on using the repository browser.