Computer Science Department
School of Computer Science, Carnegie Mellon University
Formal Verification of Memory Arrays
We have adopted the formal technique of Symbolic Trajectory Evaluation (STE) to solve the array verification problem. STE uses a form of symbolic simulation to check whether a finite state system satisfies a formula expressed in a carefully restricted temporal logic. It can handle switch-level circuits and detailed system timing. However, STE does not resolve many fundamental issues important for verifying arrays. These include the state explosion problem, causing prohibitively large ordered binary decision diagrams (OBDDs) for certain classes of circuits, and the switch-level analysis bottleneck, limiting the size of switch-level circuits that can be analyzed prior to running STE.
Our thesis builds upon earlier work on STE to overcome these problems. We have developed techniques to exploit symmetry while verifying transistor-level circuits by STE. We show that exploiting symmetry allows one to verify systems several orders of magnitude larger than otherwise possible. We have verified memory arrays with multi-million transistors. The techniques we have developed also successfully overcome the switch-level analysis bottleneck. We believe that with our work, the problem of static random access memory (SRAM) verification is solved. We have developed techniques based on new Boolean encodings to efficiently verify content addressable memories (CAMs). Our encodings scale up well in terms of verification memory requirements, as compared to naive approaches. From our experimental results, and our case studies of PowerPC CAMs, we believe that we have solved the problem of verifying all the different types of CAMs that are found on a modern microprocessor. To facilitate the use of STE, we have developed an automated technique to identify the internal state nodes in transistor netlists. We have used the techniques developed in this thesis to successfully verify several memory arrays from state of the art PowerPC microprocessor designs.