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]] [-k max_length] [-a algorithm]
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.
- -k max_length
- Use to specify the maximal deepth 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
-
Last updated on 2009/01/30 15h:04