check_ltlspec_sbmc_inc - Incremental SBMC LTL model checking
check_ltlspec_sbmc_inc [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-c] [-N]
This command generates one or more problems, and calls
SAT solver for each one. Each problem is related to a specific problem
bound, which increases from zero (0) to the given maximum problem
length. Here "length" is the bound of the problem that system
is going to generate and/or solve.
In this context the maximum problem bound is represented by the
-k command parameter, or by its default value stored in the
environment variable bmc_length.
The property to be checked may be specified using the -n idx,
-p "formula", or -P "property_name" options.
Completeness check, although slower, can be used to determine whether
the property holds.
Command options:
- -n index
- index is the numeric index of a valid LTL specification
formula actually located in the properties database.
- -p "formula" [IN context]
- Checks the formula specified on the command-line.
context is the module instance name which the variables
in formula must be evaluated in.
- -P name
- Checks the LTLSPEC property with name name in the property
database.
- -k max_length
- max_length is the maximum problem bound must be reached.
Only natural number are valid values for this option. If no value
is given the environment variable bmc_length is considered
instead.
- -c
- Performs completeness check at every step. This can be
effectively used to determine whether a property holds.
- -N
- Does not perform virtual unrolling.
For further information about this implementation see:
T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is
Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot
(ed.), Verification, Model Checking, and Abstract Interpretation,
6th International Conference VMCAI 2005, Paris, France, Volume 3385
of LNCS, pp. 380-395, Springer, 2005. Copyright ©
Springer-Verlag.
Last updated on 2010/11/03 21h:54