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/11/03 21h:54