A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems
Panagiotis Manolios and Sudarshan K. Srinivasan.
CHARME 2005, the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2005. © Springer-Verlag
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.
PDF (195K) © Springer-Verlag
PS (229K) © Springer-Verlag