check_invariant - check all states reachable in flattened network satisfy specified invariants

Performs invariant checking on a flattened network. Before calling this command, the user should have initialized the design by calling the command init_verify.

If the option -A3 (abstraction refinement method GRAB) is used, the command build_partition_maigs should also have been executed. However, in this case, the default BDD manager and network partition are not mandatory, though they will be used if available. (In other words, the user must run the commands flatten_hierarchy and build_partition_maigs, but doesn't have to run the commands static_order and build_partition_mdds before calling this command.) For extremely large networks, it is actually favorable not to build them for the entire concrete model, but let this procedure assign bdd ids and construct the partition incrementally.

Option -A4 means abstraction refinement approach using puresat algorithm, which is entirely based on SAT solver.

An invariant is a set of states. Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant.

One way of defining an invariant is through a CTL formula which has no path operators. Such formulas should be specified in the file invar_file. Note that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.

check_invariant ignores all fairness conditions associated with the FSM.

check_invariant involves reachability analysis where at every step of the reachability computation all the specified invariants are checked in the reachable states computed thus far. If some invariant does not hold, a proof of failure is demonstrated. This consists of a path starting from an initial state to a state lying outside the invariant. This path is made as short as possible. For the -A 0 option or default -A option, it is the shortest path leading to a state outside the invariant. If a set of invariants is specified, the failed formulas are reported as soon as they are detected. The check is continued with the remaining invariants.

Command options:

-d <dbg_level>

Specify the amount of debugging performed when the system fails a formula being checked.

dbg_level must be one of the following:

0 : No debugging performed. This is the default.

1 : Generate a path from an initial state to a state lying outside the invariant. This option stores the onion rings just as specifying -f would have. Therefore, it may take more time and memory if the formula passes. This option is incompatible with -A 2 option.

-f

Store the set of new states (onion rings) reached at each step of invariant. This option is likely to use more memory but possibly faster results for invariants that fail. Therefore, the debug information for a failed invariant, if requested, may be provided faster. This option is not compatible with -A 2 options.

-g <hints_file>

Use guided search. The file hints_file contains a series of hints. A hint is a formula that does not contain any temporal operators, so hints_file has the same syntax as a file of invariants used for check_invariant. The hints are used in the order given to change the transition relation. The transition relation is conjoined with the hint to yield an underapproximation of the transition relation. If the hints are cleverly chosen, this may speed up the computation considerably, because a search with the changed transition relation may be much simpler than one with the original transition relation, and results obtained can be reused, so that we may never have to do an expensive search with the original relation. See also: Ravi and Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, DAC'00. This option is not compatible with -A 2 option. The description of some options for guided search can be found in the help page for print_guided_search_options.

-h

Print the command usage.

-c

Use the formula tree so that subformulae are not shared among the CTL formulae in the input file. This option is useful in the following scenario - formulae A, B and C are being checked in order and there is sub-formula sharing between A and C. If the BDDs corresponding to the shared sub-formula is huge then computation for B might not be able to finish without using this option.

-i

Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.

-m

Pipe debugger output through the UNIX utility more.

-r

Reduce the FSM derived from the flattened network with respect to each of the invariants in the input file. By default, the FSM is reduced with respect to the conjunction of the invariants in the input file. If this option is used and don't cares are being used for simplification, then subformula sharing is disabled (result might be incorrect otherwise).

The truth of an invariant may be independant of parts of the network (such as when wires have been abstracted; see flatten_hierarchy). These parts are effectively removed when this option is invoked; this may result in more efficient invariant checking.

-t <timeOutPeriod>

Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-v <verbosity_level>

Specify verbosity level. This sets the amount of feedback on CPU usage and code status.

verbosity_level must be one of the following:

0 : No feedback provided. This is the default.

1 : Feedback on code location.

2 : Feedback on code location and CPU usage.

-A <reachability_analysis_type>

This option allows specification of the type of reachability computation.

0: (default) Breadth First Search. No approximate reachability computation.

1: High Density Reachability Analysis (HD). Computes reachable states in a manner that keeps BDD sizes under control. May be faster than BFS in some cases. For larger circuits, this option could compute more reachable states than the -A 0 option for the same memory constraints, consequently may prove more invariants false. For help on controlling options for HD, look up help on the command: print_hd_options . Refer Ravi & Somenzi, ICCAD95. The path generated for a failed invariant using this method may not be the shortest path. This option is available only when compiled with the CUDD package.

2. Approximate Reachability Don't Cares(ARDC). Computes over-approximated reachable states in the reachability analysis step. This may be faster than the -A 0 option . The invariants are checked in the over-approximation. This may produce false negatives, but these are resolved internally using the exact reachable states. The final results produced are the same as those for exact reachable states. For help on controlling options for ARDC, look up help on the command: print_ardc_options. Refer 2 papers in TCAD96 Dec. Cho et al, one is for State Space Decomposition and the other is for Approximate FSM Traversal. This option is incompatible with -d 1 and -g options.

3. The GRAB Abstraction Refinement Method. Conducts the reachability analysis on an abstract model. If the invariants are true in the abstract model, they are also true in the original model. If the invariants are false, the abstract counter-examples are used to refine the abstract model (since it is still inconclusive). This procedure iterates until a conclusive result is reached. Note that, with this option, "build_partitioned_mdds" and "static_order" does not have to be executed before calling "check_invariants," though the default BDD partition and order will be reused if available. (When checking extremely large models, skipping either or both "static_order" and "build_partitioned_mdds" can often make the verification much faster.) The grainularity of abstraction refinement also depends on the parameter "partition_threshold", which by default is 5000; one can use the VIS command "set partition_threshold 1000" to change its value. For experienced users who want to fine-tune the different parameters of GRAB, please try the test command "_grab_test" ("_grab_test -h" prints out its usage information). Refer to Wang et al., ICCAD2003 and ICCD2004 for more information about the GRAB algorithm. Note that this option is incompatible with the "-d 1" and "-g" options.

4. Abstraction refinement approach using puresat algorithm, which is entirely based on SAT solver. It has several parts: * Localization base Abstraction * K-induction to prove the truth of a property * Bounded Model Checking to find bugs * Incremental concretization based methods to verify abstract bugs * UNSAT proof based method to obtain refinement * Refinement minization to guarrantee a minimal refinement For more information, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"

-D

First compute an overapproximation to the reachable states. Minimize the transition relation using this approximation, and then compute the set of reachable states exactly. This may accelerate reachability analysis. Refer to the paper by Moon et al, ICCAD98. The BDD minimizing method can be chosen by using "set image_minimize_method " . This option is incompatible with -g.

-F <dbg_file>

Write the debugger output to dbg_file.

<invarFile>

File containing invariants to be checked.