Monolithic Verification of Deep Pipelines with Collapsed Flushing
Roma Kane, Panagiotis Manolios, and Sudarshan K. Srinivasan.
DATE 2006, Design, Automation, and Test in Europe. © ACM
We introduce collapsed flushing, a new flushing-based refinement
map for automatically verifying safety and liveness properties of
term-level pipelined machine models. We also present a new
method for handling liveness that is both simpler to define and
easier to verify than previous approaches. To empirically
validate collapsed flushing, we ran extensive experiments which
show more than an order-of-magnitude improvement in verification
times over standard flushing. Furthermore, by combining
collapsed flushing with commitment refinement maps, we can
monolithically verify complex pipelined machine models with deep
pipelines---a salient feature of state-of-the-art microprocessor
designs---that previous approaches cannot handle.
PDF (72K) © ACM