A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines

---

Panagiotis Manolios and Sudarshan K. Srinivasan.
MEMOCODE 2005, ACM-IEEE International Conference on Formal Methods and Models for Codesign. © ACM

Abstract

We introduce a new method of automating the verification of term-level pipelined machine models that is based on commitment refinement maps. Our method is much simpler to implement than current alternatives. More importantly, as our extensive experiments show, our method leads to more than a 30-fold improvement in verification times over the standard approaches to pipeline machine verification, which use refinement maps based on flushing and commitment. In addition, we can verify machines that are too complex to directly verify using flushing-based refinement maps.

PDF (195K) © ACM
PS (229K) © ACM