Using Bounded Model Checking with SMV
Introduction
Bounded model checking is a technique that uses a SAT solver to search
for counterexamples of a bounded length. Finding counterexamples in
this way is sometimes significantly faster than using symbolic model
checking. Thus, you may want to use bounded model checking while "debugging"
your proof, and then switch to full model checking to complete the
proof.
Installation
SMV comes with its own SAT solver, which it uses by default.
However, it can be made to work with your favorite SAT solver
that uses the DIMACS format.
I recommend the "zChaff" solver
from Princeton university. SMV has built-in support for this
solver, but you must install it yourself.
Under a Unix-like operating system
To use zChaff, you only have to install the pre-compiled
binary from Princeton and make it available under the name "zchaff" in your PATH.
Please note that Princeton makes zChaff available for free download only
for evaluation and non-commercial use. For commercial use, the software
must be licensed. The SMV license does not cover zChaff
or any other SAT solver. See below for instructions on using SMV with other
SAT solvers.
Under a Windows operating systems
Currently no pre-compiled zChaff binary is available for the Windows
operating systems. This means you must download the source code and
compile it using the GNU tools under Cygwin.
Then make the resulting binary available under the name "zchaff" in your
Win32 PATH. Also, make the library cygwin1.dll available in your Win32 PATH.
This is very important! SMV is not a Cygwin application. It will not find programs
and libraries in your Cygwin PATH. If you get the error message "child process exited
abnormally" when you try to use bounded model checking, you have probably done this
incorrectly. Try running zchaff from a DOS command line to make sure that Windows
is finding the zchaff binary and the cygwin1.dll library.
Using bounded model checking
Use of bounded model checking with SMV is described in the man page smv(1). Briefly, the command
smv -bmc -l length file.smv
will check properties in file "file.smv" using bounded model checking, with maximum counterexample
length of "length" transitions. Note, this can only produce counterexamples, and will never produce the
result "true" for a property. Bounded model checking can also be selected in the options
menu in the visual interface "vw". To use your favorite sat solver instead of SMV's default
solver, add the "-satsolver"
option, like this:
smv -bmc -l length -satsolver zchaff file.smv
Interfacing SAT solvers to SMV
Unfortunately, while there is a standard input format for SAT solvers (the DIMACS format),
there is apparently no standard output format. This means that to interface a SAT solver
to SMV you must write a wrapper script that parses the output of the solver and writes the
result to a file in a standard format. The script can be written in any language under
Unix. Under windows, only Tcl scripts are supported.
Suppose, for example, that you have a SAT solver named "foosat". You should write a script
called runfoosat, to be executed as follows:
runfoosat inputfilename outputfilename
The input file will be in DIMACS format (accepted by most SAT solvers). The output file must be
a sequence of decimal numbers separated by whitespace (that is, space, tab and newline
characters). The first number in this list is zero for the unsatisfiable case, and one
for the satisfiable case. In the satisfiable case, the remaining numbers are the numbers
of the positive literals in the satisfying assignment. Negative numbers included in this
file are ignored. The literals need not be sorted. Any other output from the solver (e.g.,
run-time statistics) can be passed through to the standard output, and will we displayed
as part of SMV's "log".
On Unix-like operating systems, the script runfoosat should be made executable and placed somewhere in
the user's path. On windows, the script runfoosat must be a Tcl script, and must be placed in the folder "bin" in
the SMV installation folder (by default c:\Program Files\SMV\bin). As an example, here is
the script runzchaff:
#!/bin/sh
# the next line restarts using tclsh \
exec tclsh "$0" "$@"
set f [open "|zchaff [lindex $argv 0]" "r"]
set outfile [open [lindex $argv 1] "w"]
while {![eof $f]} {
gets $f l
puts $l
if {[string match *unsatisfiable* $l]} {
puts $outfile 0
} elseif {[string match *satisfiable* $l]} {
puts $outfile 1
while {![eof $f]} {
gets $f l
if {[string match Max* $l]} {
break
}
puts $outfile $l
}
}
}
close $f
close $outfile
Ken McMillan
Last modified: Fri Oct 11 17:46:05 PDT 2002