Verification of memory arrays is an important part of processor verification. Memory arrays include circuits such as on-chip caches, cache tags, register files, and branch prediction buffers having memory cores embedded within complex logic. Such arrays cover large areas of the chip and are critical to the functionality and performance of the system. Hence, these circuits are custom designed at the transistor level to optimize area and performance. Conventional simulation based verification approaches do not work for arrays, as it is infeasible to simulate the astronomical number of simulation patterns that are required to verify these designs. Therefore, we need to look at formal methods to ensure the correctness of these circuits.

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.

183 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu