A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems
Panagiotis Manolios and Sudarshan K. Srinivasan.
We present a parameterized suite of benchmark problems arising
from our work on pipelined machine verification, in the hopes
that they can be used to speed up decision procedures. While the
existence of a large number of CNF benchmarks has spurred the
development of efficient SAT solvers, the benchmarks available
for more expressive logics are quite limited. Our work on
pipelined machine verification has yielded many problems that not
only have complex models, but also have complex correctness
statements, involving invariants and symbolic simulations of the
models for dozens of steps. Many of these proofs take hundreds of
thousands of seconds to check using the UCLID decision procedure
and SAT solvers such as Zchaff and Siege. More complex
problems can be generated by using PiMaG, a Web application that
we developed. PiMaG generates problems in UCLID, SVC, and CNF
formats based on user-provided parameters specifying features of
the pipelined machines and their correctness statements.
Download the core benchmarks below or use our tool to generate custom benchmarks.
PiMaG: The Pipeline Machine GeneratorUse PiMag to generate more complex benchmarks. Start by selecting a base processor model (either 6 or 7 stages), but note that only the 7 stage model can have an instruction queue. Next, select the type refinement map you want to use. The rest of the features are self-explanatory and are covered in detail in the accompanying paper. Finally, choose what format(s) you want, including UCLID, SVC and CNF. (Currently only the UCLID format is available, but UCLID can generate SVC and CNF file; bear with us while we get the cgi server properly configured.)
Pipelined Machine Verification References
- This paper describes the notion of correctness based
on Well Founded Equivalence Bisimulation (WEB) refinement
that we use to verify our models. Panagiotis Manolios.
Correctness of Pipelined Machines. In W. A. Hunt,
Jr. and S. D. Johnson, editors, Formal Methods in
Computer-Aided Design, FMCAD 2000, volume 1954 of LNCS,
pages 161-178. Springer-Verlag,
- This paper presents recent work on automating WEB refinement proofs using the UCLID decision procedure. Panagiotis Manolios and Sudarshan K. Srinivasan. Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements. DATE 2004, Design, Automation, and Test in Europe, 2004.