check_pslspec - Performs fair PSL model checking.
check_pslspec [-h] [-m | -o output-file] [-n number | -p "psl-expr [IN context]" | -P "name"] [-b|-s [-i] [-c] [-N] [-g] [-1] [-k bmc_length] [-l loopback]]
Performs fair PSL model checking.
A psl-expr to be checked can be specified at command line
using option -p. Alternatively, option -n can be used
for checking a particular formula in the property database. If
neither -n nor -p are used, all the PSLSPEC formulas in
the database are checked.
Command options:
- -m
- Pipes the output generated by the command in processing
SPECs to the program specified by the
PAGER shell variable if defined, else
through the UNIX command "more".
- -o output-file
- Writes the output generated by the command in processing
PSLSPECs to the file output-file.
- -p "psl-expr [IN context]"
- A PSL formula to be checked. context is the module
instance name which the variables in ctl-expr must
be evaluated in.
- -n number
- Checks the PSL property with index number in the property
database.
- -P name
- Checks the PSL property named name in the property
database.
- -b When specified, the BMC engine will be used for
checking those PSL properties that can be converted to LTL
specifications. The SAT solver to be used will be chosen according
to the current value of the system variable sat_solver. Non-LTL
properties will be ignored.
- -s When specified, the SBMC engine will be used for
checking those PSL properties that can be converted to LTL
specifications. The SAT solver to be used will be chosen according
to the current value of the system variable sat_solver. Non-LTL
properties will be ignored.
- -i Uses incremental SAT solving when this feature is
available. This option must be mandatorily used in combination
with the option -b.
- -c Performs completeness check. This option can be
used only in combination with -s. This options implies also -i
- -N Does not perform virtual unrolling. This option can be
used only in combination with -s. This options implies also -i
- -g While solving a problem, dumps it as a DIMACS
file whose name depends on the content of the system variable
"bmc_dimacs_filename". This feature is not allowed when the option
-i is used as well.
- -1 Generates and solves a single problem instead of
iterating through 0 and bmc_length.
- -k bmc_length
- bmc_length is the maximum problem bound must be reached if
the option -1 is not specified. If -1 is specified, bmc_length is
the exact length of the problem to be generated.
Only natural number are valid values for this option. If no value
is given the environment variable bmc_length is considered
instead.
- -l loopback
- loopback value may be:
- a natural number in (0, bmc_length-1). Positive sign ('+') can
be also used as prefix of the number. Any invalid combination of length
and loopback will be skipped during the generation/solving process.
- a negative number in (-1, -bmc_length). In this case
loopback is considered a value relative to bmc_length.
Any invalid combination of length and loopback will be skipped
during the generation/solving process.
- the symbol 'X', which means "no loopback"
- the symbol '*', which means "all possible loopback from zero to
bmc_length-1"
Last updated on 2010/05/19 15h:56