SAT benchmarks based on bounded model checking

Here you will find a set of benchmark problems for SAT solvers based on the formal verification of the open-source Sun PicoJava II (tm)* microprocessor. Currently benchmark problems derived from the verification of the instruction fetch unit (ICU) are available.

The SAT problems arise in a technique called "bounded model checking", which searches for a counterexample to an assertion using up to a fixed number of transitions. A satisfiable instance indicates the presence of a counterexample of the given length or shorter.

In this set of benchmarks, a representative selection of property instances from were selected from the compositional verification of the ICU. These properties specify the behavior of this unit relative to a reference model. They are primarily properties of data rather than control. Since the property specifications are written with respect to an infinite history of the reference model, the state space that must be searched is not finite. Data abstraction has been heavily used to reduce infinite or very large data structures, such as the reference model history and main memory, to finite size.

Each property is divided into a possibly large number of cases because of bit slicing, replication in the hardware and case splitting on relations between parameters. This means that the overall verification generates a large number of similar properties. In the case of bit slicing, the properties are usually isomorphic. Thus, only a few representative cases have been chosen for this benchmark suite.

Because of the large number of cases that must be verified, these properties have been reduced using compositional methods so that each case takes typically from a few seconds to a few minutes to verify by symbolic model checking. The number of state bits involved in each property after abstraction is typically between 50 and 100, with up to a few hundred combinational variables. This means that these benchmark problems are smaller than those typically encountered in model checking RTL level designs (which may have a few hundred state variables and take on the order of a day to complete), however they are representative of problems that arise in a compositional style of verification.

Downloading the benchmark suite

An RTL verilog description of the The Sun PicoJava II (tm)* processor design is available from Sun Microsystems under an open-source-like license. Because this source code is licensed, and because the benchmark problems are derived from it, I cannot distribute these problems directly. Rather, you must download the source code from Sun Microsystems and then using the Cadence SMV system to generate the benchmarks. This also avoids a download of 178 MB. The steps are as follows:

Download and install the Cadence SMV verification system.
- Make sure to download version 08-20-01p2, and upgrade to this version if you have an earlier version installed. Earlier versions may not produce correct results.
Download the benchmark suite.
Download the Sun PicoJava II (tm)* source code, version 2.0.
Create a new directory and cd to it.
Unzip/untar the benchmark suite.
Unzip/Untar the PicoJava source code.
Patch the source code with the command "./pjpatch".
Run the command "./pjbenchgen"

This will create a set of 76 SAT problems in the directory "./sat". They break down as follows:

1.cnf - 19.cnf: Proofs broken to generate counterexamples. Unfolding depth 10. 20.cnf - 38.cnf: Same. Proofs not broken. Should be UNSAT. Unfolding depth 10. 39.cnf - 57.cnf: Same. Proofs broken to generate counterexamples. Unfolding depth 20. 20.cnf - 38.cnf: Same. Proofs not broken. Should be UNSAT. Unfolding depth 20.

At the head of each file is a comment line of the following form:

c filename.smv property-name unfold-depth SAT/UNSAT

* PicoJava II is a trademark of Sun Microsystems, Inc.

Last modified: Wed Oct 10 12:41:58 PDT 2001