Design, Automation and Test in Europe (DATE'05) Volume 2
Refinement Maps for Efficient Verification of Processor Models
Munich, Germany
March 07-March 11
ISBN: 0-7695-2288-2
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.
Citation:
Panagiotis Manolios, Sudarshan K. Srinivasan, "Refinement Maps for Efficient Verification of Processor Models," date, vol. 2, pp.1304-1309, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005