In this paper we report on new techniques for verifying contentaddressable memories (CAMs), and demonstrate that these techniqueswork well for large industrial designs. It was shown in [Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation], that theformal verification technique of symbolic trajectory evaluation (STE)could be used successfully on memory arrays. We have extended thatwork to verify what are perhaps the most combinatorially difficultclass of memory arrays, CAMs. We use new Boolean encodings toverify CAMs, and show that these techniques scale well, in that spacerequirements increase linearly, or sub-linearly, with the various CAMsize parameters.In this paper, we describe the verification of two CAMs froma recentPowerPC microprocessor design, a Block Address Translation unit(BAT), and a Branch Target Address Cache unit (BTAC). The BATis a complex CAM, with variable length bit masks. The BTAC is a64-entry, 64-bits per entry, fully associative CAM and is part of thespeculative instruction fetch mechanism of the microprocessor. Webelieve that ours is the first work on formally verifying CAMs, and webelieve our techniques make it feasible to efficiently verify the varietyof CAMs found on modern processors.