source: vis_dev/vis-2.3/share/help/check_invariantCmd.txt @ 26

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

vis2.3
File size: 13.7 KB
Line 
1
2  check_invariant - check all states reachable in flattened network satisfy
3  specified invariants
4     _________________________________________________________________
5
6   check_invariant [-c] [-d <dbg_level>] [-g <hints_file>] [-f] [-h] [-i] [-m]
7   [-r]     [-t    <time_out_period>]    [-v    <verbosity_level>]    [-A
8   <reachability_analysis_type>] [-D] <invar_file>
9
10   Performs invariant 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.
13
14   If the option -A3 (abstraction refinement method GRAB) is used, the command
15   [2]build_partition_maigs should also have been executed. However, in this
16   case, the default BDD manager and network partition are not mandatory,
17   though they will be used if available. (In other words, the user must run
18   the commands [3]flatten_hierarchy and [4]build_partition_maigs, but doesn't
19   have to run the commands [5]static_order and [6]build_partition_mdds before
20   calling  this  command.)  For extremely large networks, it is actually
21   favorable not to build them for the entire concrete model, but let this
22   procedure assign bdd ids and construct the partition incrementally.
23
24   Option -A4 means abstraction refinement approach using puresat algorithm,
25   which is entirely based on SAT solver.
26
27   An invariant is a set of states. Checking the invariant is the process of
28   determining that all states reachable from the initial states lie in the
29   invariant.
30
31   One way of defining an invariant is through a CTL formula which has no path
32   operators. Such formulas should be specified in the file invar_file. Note
33   that the support of any wire referred to in a formula should consist only of
34   latches. For the precise syntax of CTL formulas, see the [7]VIS CTL and LTL
35   syntax manual.
36
37   check_invariant ignores all fairness conditions associated with the FSM.
38
39   check_invariant involves reachability analysis where at every step of the
40   reachability computation all the specified invariants are checked in the
41   reachable states computed thus far. If some invariant does not hold, a proof
42   of failure is demonstrated. This consists of a path starting from an initial
43   state to a state lying outside the invariant. This path is made as short as
44   possible. For the -A 0 option or default -A option, it is the shortest path
45   leading  to  a  state outside the invariant. If a set of invariants is
46   specified, the failed formulas are reported as soon as they are detected.
47   The check is continued with the remaining invariants.
48
49   Command options:
50
51   -d <dbg_level>
52          Specify the amount of debugging performed when the system fails a
53          formula being checked.
54
55          dbg_level must be one of the following:
56
57          0 : No debugging performed. This is the default.
58
59          1 : Generate a path from an initial state to a state lying outside
60          the invariant. This option stores the onion rings just as specifying
61          -f would have. Therefore, it may take more time and memory if the
62          formula passes. This option is incompatible with -A 2 option.
63
64   -f
65          Store the set of new states (onion rings) reached at each step of
66          invariant. This option is likely to use more memory but possibly
67          faster  results  for invariants that fail. Therefore, the debug
68          information for a failed invariant, if requested, may be provided
69          faster. This option is not compatible with -A 2 options.
70
71   -g <hints_file>
72          Use guided search. The file hints_file contains a series of hints. A
73          hint is a formula that does not contain any temporal operators, so
74          hints_file has the same syntax as a file of invariants used for
75          check_invariant. The hints are used in the order given to change the
76          transition relation. The transition relation is conjoined with the
77          hint to yield an underapproximation of the transition relation. If
78          the hints are cleverly chosen, this may speed up the computation
79          considerably, because a search with the changed transition relation
80          may be much simpler than one with the original transition relation,
81          and results obtained can be reused, so that we may never have to do
82          an expensive search with the original relation. See also: Ravi and
83          Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem,
84          Ravi, and Somenzi, Efficient Decision Procedures for Model Checking
85          of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi,
86          Symbolic Guided Search for CTL Model Checking, DAC'00. This option is
87          not compatible with -A 2 option. The description of some options for
88          guided   search   can   be   found   in   the   help  page  for
89          print_guided_search_options.
90
91   -h
92          Print the command usage.
93
94   -c
95          Use the formula tree so that subformulae are not shared among the CTL
96          formulae in the input file. This option is useful in the following
97          scenario - formulae A, B and C are being checked in order and there
98          is sub-formula sharing between A and C. If the BDDs corresponding to
99          the shared sub-formula is huge then computation for B might not be
100          able to finish without using this option.
101
102   -i
103          Print  input  values  causing transitions between states during
104          debugging. Both primary and pseudo inputs are printed.
105
106   -m
107          Pipe debugger output through the UNIX utility more.
108
109   -r
110          Reduce the FSM derived from the flattened network with respect to
111          each of the invariants in the input file. By default, the FSM is
112          reduced with respect to the conjunction of the invariants in the
113          input file. If this option is used and don't cares are being used for
114          simplification, then subformula sharing is disabled (result might be
115          incorrect otherwise).
116
117          The truth of an invariant may be independant of parts of the network
118          (such as when wires have been abstracted; see [8]flatten_hierarchy).
119          These parts are effectively removed when this option is invoked; this
120          may result in more efficient invariant checking.
121
122   -t <timeOutPeriod>
123          Specify the time out period (in seconds) after which the command
124          aborts. By default this option is set to infinity.
125
126   -v <verbosity_level>
127          Specify verbosity level. This sets the amount of feedback on CPU
128          usage and code status.
129
130          verbosity_level must be one of the following:
131
132          0 : No feedback provided. This is the default.
133
134          1 : Feedback on code location.
135
136          2 : Feedback on code location and CPU usage.
137
138   -A <reachability_analysis_type>
139          This  option  allows  specification of the type of reachability
140          computation.
141
142          0:  (default) Breadth First Search. No approximate reachability
143          computation.
144
145          1: High Density Reachability Analysis (HD). Computes reachable states
146          in a manner that keeps BDD sizes under control. May be faster than
147          BFS in some cases. For larger circuits, this option could compute
148          more  reachable states than the -A 0 option for the same memory
149          constraints, consequently may prove more invariants false. For help
150          on  controlling  options  for  HD, look up help on the command:
151          print_hd_options [9]print_hd_options. Refer Ravi & Somenzi, ICCAD95.
152          The path generated for a failed invariant using this method may not
153          be the shortest path. This option is available only when compiled
154          with the CUDD package.
155
156          2.   Approximate   Reachability   Don't  Cares(ARDC).  Computes
157          over-approximated reachable states in the reachability analysis step.
158          This may be faster than the -A 0 option . The invariants are checked
159          in the over-approximation. This may produce false negatives, but
160          these are resolved internally using the exact reachable states. The
161          final results produced are the same as those for exact reachable
162          states. For help on controlling options for ARDC, look up help on the
163          command: print_ardc_options. [10]print_ardc_options Refer 2 papers in
164          TCAD96 Dec. Cho et al, one is for State Space Decomposition and the
165          other is for Approximate FSM Traversal. This option is incompatible
166          with -d 1 and -g options.
167
168          3. The GRAB Abstraction Refinement Method. Conducts the reachability
169          analysis on an abstract model. If the invariants are true in the
170          abstract model, they are also true in the original model. If the
171          invariants are false, the abstract counter-examples are used to
172          refine the abstract model (since it is still inconclusive). This
173          procedure iterates until a conclusive result is reached. Note that,
174          with this option, "build_partitioned_mdds" and "static_order" does
175          not have to be executed before calling "check_invariants," though the
176          default BDD partition and order will be reused if available. (When
177          checking  extremely  large  models,  skipping  either  or  both
178          "static_order"  and "build_partitioned_mdds" can often make the
179          verification much faster.) The grainularity of abstraction refinement
180          also depends on the parameter "partition_threshold", which by default
181          is 5000; one can use the VIS command "set partition_threshold 1000"
182          to change its value. For experienced users who want to fine-tune the
183          different  parameters  of  GRAB,  please  try  the test command
184          "_grab_test" ("_grab_test -h" prints out its usage information).
185          Refer to Wang et al., ICCAD2003 and ICCD2004 for more information
186          about the GRAB algorithm. Note that this option is incompatible with
187          the "-d 1" and "-g" options.
188
189          4. Abstraction refinement approach using puresat algorithm, which is
190          entirely based on SAT solver. It has several parts: * Localization
191          base Abstraction * K-induction to prove the truth of a property *
192          Bounded Model Checking to find bugs * Incremental concretization
193          based methods to verify abstract bugs * UNSAT proof based method to
194          obtain refinement * Refinement minization to guarrantee a minimal
195          refinement For more information, please check the BMC'03 and STTT'05
196          paper of Li et al., "A satisfiability-based appraoch to abstraction
197          refinement in model checking", and " Abstraction in symbolic model
198          checking using satisfiability as the only decision procedure"
199
200   -D
201          First compute an overapproximation to the reachable states. Minimize
202          the transition relation using this approximation, and then compute
203          the set of reachable states exactly. This may accelerate reachability
204          analysis.  Refer  to  the paper by Moon et al, ICCAD98. The BDD
205          minimizing method can be chosen by using "set image_minimize_method "
206          [11]set. This option is incompatible with -g.
207
208   -F <dbg_file>
209          Write the debugger output to dbg_file.
210
211   -w <node_file> This option invokes the algorithm to generate an error trace
212          divided into fated and free segements. Fate represents the
213          inevitability and free is asserted when there is no inevitability.
214          This can be formulated as a two-player concurrent reachability game.
215          The two players are the environment and the system. The node_file is
216          given to specify the variables the are controlled by the system.
217
218   -W
219   This option represents the case that all input variables are controlled by
220          system.
221
222   -G
223   We proposed two algorithms to generate segmented counterexamples: general
224          and restricted. By default we use the restricted algorithm. We can
225          invoke the general algorithm with -G option. For more information,
226          please read the STTT'04 paper by Jin et al., "Fate and Free Will in
227          Error Traces"
228
229   <invarFile>
230          File containing invariants to be checked.
231
232   Related "set" options:
233
234   rch_simulate <#>
235   The set option can be used to set this flag rch_simulate to specify the
236   number of random vectors to be simulated. Default value for this number is
237   0.
238
239   ctl_change_bracket <yes/no>
240   Vl2mv automatically converts "[]" to "<>" in node names, therefore CTL
241   parser does the same thing. However, in some cases a user does not want to
242   change node names in CTL parsing. Then, use this set option by giving "no".
243   Default is "yes".
244
245   See also command : compute_reach
246     _________________________________________________________________
247
248   Last updated on 20100410 00h02
249
250References
251
252   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
253   2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html
254   3. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html
255   4. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html
256   5. file://localhost/projects/development/hsv/vis/common/doc/html/static_orderCmd.html
257   6. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_mddsCmd.html
258   7. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
259   8. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html
260   9. file://localhost/projects/development/hsv/vis/common/doc/html/print_hd_optionsCmd.html
261  10. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html
262  11. file://localhost/projects/development/hsv/vis/common/doc/html/setCmd.html
Note: See TracBrowser for help on using the repository browser.