Automatic Memory Reductions for RTL Model Verification

---

Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon.
International Conference on Computer Aided Design (ICCAD-2006), 2006. © ACM

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