gen_invar_bmc - Generates the given invariant, or all invariants if no formula is given
gen_invar_bmc [-h | -n idx | -p "formula" [IN context] | -P "name"] [-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 invariant property stored in the properties
database with name "name"
- -o filename
- filename is the name of the dumped dimacs file,
without extension.
If you
do not use this option the dimacs file name is taken from the
environment variable bmc_invar_dimacs_filename.
File name may contain special symbols which will be macro-expanded
to form the real dimacs 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 2012/11/18 14h:16