Formal verification of content addressable memories using symbolic trajectory evaluation

In this paper we report on new techniques for verifying content addressable memories (CAMs), and demonstrate that these techniques work well for large industrial designs. It was shown in [6], that the formal verification technique of symbolic trajectory evaluation (STE) could be used successfully on memory arrays. We have extended that work to verify what are perhaps the most combinatorially difficult class of memory arrays, CAMs. We use new Boolean encodings to verify CAMs, and show that these techniques scale well, in that space requirements increase linearly, or sub-linearly, with the various CAM size parameters. In this paper, we describe the verification of two CAMs from a recent PowerPCTM microprocessor design, a Block Address Translation unit (BAT), and a Branch Target Address Cache unit (BTAC). The BAT is a complex CAM, with variable length bit masks. The BTAC is a 64-entry, 64-bits per entry, fully associative CAM and is part of the speculative instruction fetch mechanism of the microprocessor. We believe that ours is the first work on formally verifying CAMs, and we believe our techniques make it feasible to efficiently verify the variety of CAMs found on modern processors. 1