check_invar_bmc - Generates and solve the given invariant, or all invariants if no formula is given
check_invar_bmc [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-a algorithm] [-o filename]
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 only when selected algorithm is een-sorensson).
Use to specify the maximal deepth to be reached by the een-sorensson
invariant checking algorithm. If not specified, the value assigned
to the system variable bmc_length is taken.
- -a algorithm
- Uses the specified algorithm to solve the invariant. If used, this
option will override system variable bmc_invar_alg.
At the moment, possible values are: "classic", "een-sorensson".
- -o filename
- filename is the name of the dumped dimacs file, without
extension.
It may contain special symbols which will be macro-expanded to form
the real file name. Possible symbols are:
- @F: model name with path part
- @f: model name without path part
- @n: index of the currently processed formula in the properties
database
- @@: the '@' character
Last updated on 2010/05/19 22h:26