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