Formal verification of content addressable memories using symbolic trajectory evaluation

ABSTRACT

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.

REFERENCES

• 1: Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
• 2: R. E. Bryant, "Formal Verification of Memory Circuits by Switch-Level Simulation," IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems, Vol.10, no.l, Jan. 1991; pp. 94-102.
• 3: Neeta Ganguly , Magdy S. Abadir , Manish Pandey, PowerPCTM Array Verification Methodology using Formal Techniques, Proceedings of the IEEE International Test Conference on Test and Design Validity, p.857-864, October 20-25, 1996
• 4: Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992
• 5: "PowerPCTM Microprocessor Family: The Programming Environments," Motorola Inc., 1994.
• 6: Manish Pandey , Richard Raimi , Derek L. Beatty , Randal E. Bryant, Formal verification of PowerPC arrays using symbolic trajectory evaluation, Proceedings of the 33rd annual conference on Design automation, p.649-654, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240641]
• 7: Carl-Johan H. Seger , Randal E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, v.6 n.2, p.147-189, March 1995 [doi>10.1007/BF01383966]
• 8: Carl Seger, VOSS - A Formal Hardware Verification System User''s Guide, University of British Columbia, Vancouver, BC, Canada, 1993
• 9: Neil H. E. Weste , Kamran Eshraghian, Principles of CMOS VLSI design: a systems perspective, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  C. Computer Systems Organization

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification