Sciweavers

DATE
2006
IEEE

Monolithic verification of deep pipelines with collapsed flushing

14 years 2 months ago
Monolithic verification of deep pipelines with collapsed flushing
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 orderof-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.
Roma Kane, Panagiotis Manolios, Sudarshan K. Srini
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where DATE
Authors Roma Kane, Panagiotis Manolios, Sudarshan K. Srinivasan
Comments (0)