Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

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


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