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