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.
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