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

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

Last modified: Mon Jun 6 11:36:32 EDT 2005 manolios@cc.gatech.edu

Back to Pete's home page College of Computing