Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Refinement Maps for Efficient Verification of Processor Models

Panagiotis Manolios and Sudarshan K. Srinivasan.
DATE 2005, Design, Automation, and Test in Europe. © ACM


While most of the effort in improving verification times for pipeline machine verification has focused on faster decision procedures, we show that the refinement maps used also have a drastic impact on verification times. We introduce a new class of refinement maps for pipelined machine verification, and using the state-of-the-art verification tools UCLID and Siege we show that one can attain several orders of magnitude improvements in verification times over the standard flushing-based refinement maps, even enabling the verification of machines that are too complex to otherwise automatically verify.

PDF (74K) © ACM