Automatic Memory Reductions for RTL Model Verification

Abstract

We present several techniques for automatically reducing memories in RTL designs. This includes a new memory abstraction algorithm that allows us to greatly reduce the size of memories and a technique based on-term rewriting that further improves the abstraction. In contrast to previously proposed methods for abstracting memories of RTL designs, our methods are general---e.g., they allow us to arbitrarily and directly compare memories---and they are sound and complete---e.g., there are no false positives or negatives. In addition, the combination of our techniques allows us to automatically verify RTL pipelined machine designs beyond the reach of current state-of-the-art methods, as our experimental results show.

PDF (160K) © ACM

Last modified: Thu Aug 31 20:16:16 EDT 2006 manolios@cc.gatech.edu

Back to Pete's home page College of Computing