A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems

---

Panagiotis Manolios and Sudarshan K. Srinivasan.

Abstract

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.

Core Benchmarks

• UCLID format.
• SVC format.
• CNF format.
• UCLID, SVC, and CNF formats.

PiMaG: The Pipeline Machine Generator

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

Base Model:
6 Stage
7 Stage

Refinement Map:
Commitment ("Good MA")
Commitment (GFI)
Flushing

Length of instruction queue:
Can vary between 0 and 20 for commitment (GFI or "Good MA") and 0 and 5 for flushing.
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20

Cache and Write Buffer:
None
Instruction cache
Instruction cache and data cache
Instruction cache, data cache, and write buffer

Length of write buffer (applicable only if you selected a write buffer):
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20

Branch Prediction:
Predict not taken
Branch prediction abstraction scheme 1
Branch prediction abstraction scheme 2

Benchmark Formats:
(You can select more than one)
UCLID SVC CNF

When ready, click on the "Submit" button. or

---

Pipelined Machine Verification References

1. 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, 2000.

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