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