ltl_model_check - perform LTL model checking on a flattened network

Performs LTL model checking on a flattened network. Before calling this command, the user should have initialized the design by calling the command init_verify. Regardless of the options, no 'false positives' or 'false negatives' will occur: the result is correct for the given circuit.

Properties to be verified should be provided as LTL formulae in the file ltl_file. Note that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of LTL formulas, see the VIS CTL and LTL syntax manual.

A formula passes iff it is true for all initial states of the system. Therefore, in the presence of multiple initial states, if a formula fails, the negation of the formula may also fail.

If a formula does not pass, a (potentially partial) proof of failure (referred to as a debug trace) is demonstrated. Fair paths are represented by a finite sequence of states (the stem) leading to a fair cycle, i.e. a cycle on which there is a state from each fairness condition. Whether demostrate the proof or not can be specified (see option -d).

Command options:

-a <ltl2aut_algorithm>

Specify the algorithm used in LTL formula -> Buechi automaton translation.

ltl2aut_algorithm must be one of the following:

0: GPVW.

1: GPVW+.

2: LTL2AUT.

3: WRING (default).

-b

Use boolean minimization during the LTL to Automaton translation.

-d <dbg_level>

Specify whether to demonstrate a counter-example when the system fails a formula being checked.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Generate a counter-example (a path to a fair cycle).

-f <dbg_file>

Write the debugger output to dbg_file.

-h

Print the command usage.

-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.

-t <timeOutPeriod>

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

-s

Print debug output in the format accepted by the simulate command.

-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 <le_method>

Specify whether the compositional SCC analysis algorithm, Divide and Compose (DnC), is enabled for language emptiness checking. The DnC algorithm first enumerates fair SCCs in an over-approximated abstract model, and then successively refines them in the more concrete models. Since non-fair SCCs can be ignored in the more concrete models, a potentially large part of the state space are pruned away early on when the computations are cheap.

le_method must be one of the following:

0 : no use of Divide and Compose (Default).

1 : use Divide and Compose.

-D <dc_level>

Specify extent to which don't cares are used to simplify MDDs in model checking. Don't cares are minterms on which the value taken by functions does not affect the computation; potentially, these minterms can be used to simplify MDDs and reduce the time taken to perform model checking.
dc_level must be one of the following:

0 : No don't cares are used.

1 : Use unreachable states as don't cares. This is the default.

2 : Use unreachable states as don't cares and in the EU computation, use 'frontiers' for image computation.

3 : First compute an overapproximation of the reachable states (ARDC), and use that as the cares set. Use `frontiers' for image computation. For help on controlling options for ARDC, look up help on the command: print_ardc_options. Refer to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD December 1996: one is for State Space Decomposition and the other is for Approximate FSM Traversal.

-S <schedule>

Specify schedule for GSH algorithm, which generalizes the Emerson-Lei algorithm and is used to compute greatest fixpoints. The choice of schedule affects the sequence in which EX and EU operators are applied. It makes a difference only when fairness constraints are specified.
<schedule> must be one of the following:

EL : EU and EX operators strictly alternate. This is the default.

EL1 : EX is applied once for every application of all EUs.

EL2 : EX is applied repeatedly after each application of all EUs.

budget : a hybrid of EL and EL2

random : enabled operators are applied in (pseudo-)random order.

off : GSH is disabled, and the old algorithm is used instead. The old algorithm uses the EL , but the termination checks are less sophisticated than in GSH.

-F

Use forward analysis in the computation of the greatest fixpoint. This option is incompatible with -d 1 or higher and can only be used with -D 1.

-L <lockstep_mode>

Use the lockstep algorithm, which is based on fair SCC enumeration.
<lockstep_mode> must be one of the following:

off : Lockstep is disabled. This is the default. Language emptiness is checked by computing a hull of the fair SCCs.

on : Lockstep is enabled.

all : Lockstep is enabled; all fair SCCs are enumerated instead of terminating as soon as one is found. This can be used to study the SCCs of a graph, but it is slower than the default option.

n : (n is a positive integer). Lockstep is enabled and up to n fair SCCs are enumerated. This is less expensive than all , but still less efficient than on , even when n = 1 .

-X

Disable strength reduction (use different decision procedures for strong, weak, and terminal automaton). Strength reduction is the default. Refer to Bloem, Ravi, Somenzi, "Efficient Decision Procedures for LTL Model Checking," CAV99.

-Y

Disable incremental construction of the partition for (MxA). Instead, build a new partition from the scratch. Incremental construction of the partition is the default.

-Z

Add arcs into the Buechi automaton by direct simulation relation, to heuristically reduce the length of shortest counter-example in model checking. Refer to Awedh and Somenze, "Proving More Properties with Bounded Model Checking," CAV04.

-M

Maximize (adding arcs to) Buechi automaton using Direct Simulation.

<ltl_file>

File containing LTL formulas to be model checked.

ltl_change_bracket <yes/no>

Vl2mv automatically converts "[]" to "<>" in node names, therefore CTL* parser does the same thing. However, in some cases a user does not want to change node names in CTL* parsing. Then, use this set option by giving "no". Default is "yes".

See also commands : model_check, approximate_model_check, incremental_ctl_verification

---

Last updated on 20050519 00h50