check_invar_bmc_inc - Generates and solve the given invariant, or all invariants if no formula is given


check_invar_bmc_inc [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-a algorithm] [-s strategy]

Command options:

-n index
index is the numeric index of a valid INVAR specification formula actually located in the properties database.
The validity of index value is checked out by the system.
-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 INVARSPEC property with name name in the property database.
-k max_length
Use to specify the maximal depth to be reached by the incremental invariant checking algorithm. If not specified, the value assigned to the system variable bmc_length is taken.
-a algorithm
Use to specify incremental invariant checking algorithm. Currently this can be one of the following values: dual, zigzag, falsification.
-s strategy
Use to specify closure strategy (this currenly applies to dual algorithm only). This can be one of the following values: backward, forward.

Last updated on 2011/04/06 21h:13