On measuring the effectiveness of various design validation approaches for PowerPC microprocessor embedded arrays

ABSTRACT

Design validation for embedded arrays remains as a challenging problem in today's microprocessor design environment. At Somerset, validation of array designs relies on both formal verification and vector simulation. Although several methods for array design validation have been proposed and had great success [Ganguly et al. 1996; Pandey et al. 1996, 1997; Wang and Abadir 1997], little evidence has been reported for the effectiveness of these methods with respect to the detection of design errors. In this paper, we measure the effectiveness of different validation approaches based on automatic design error injection and simulation. The technique provides a systematic way to evaluate various validation approaches at both logic and transistor levels. Experimental results on recent PowerPC microprocessor arrays will be discussed and reported.

REFERENCES

• 1: ABADIR, M. S., FERGUSON, J., AND KIRKLAND, T.E. 1988. Logic design verification via test generation. IEEE Trans. Computer-Aided Design 7, 1 (Jan.), 138-148.
• 2: Randal E. Bryant, Symbolic simulation—techniques and applications, Proceedings of the 27th ACM/IEEE conference on Design automation, p.517-521, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.128296]
• 3: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 4: 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
• 5: Craig Hunter , Jeff Slaton , Jim Eno , Romesh M. Jessani , Carl Dietz, The PowerPC 603TM Microprocessor: An Array Built-In Self-Test Mechanism, Proceedings of the IEEE International Test Conference on TEST: The Next 25 Years, p.388-394, October 02-06, 1994
• 6: Charles H. Malley , Max Dieudonné, Logic verification methodology for PowerPC microprocessors, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.234-240, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217535]
• 7: 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]
• 8: Manish Pandey , Richard Raimi , Randal E. Bryant , Magdy S. Abadir, Formal verification of content addressable memories using symbolic trajectory evaluation, Proceedings of the 34th annual conference on Design automation, p.167-172, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266056]
• 9: 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]
• 10: Li-C. Wang , Magdy S. Abadir, A New Validation Methodology Combining Test and Formal Verification for PowerPCTM Microprocessor Arrays, Proceedings of the IEEE International Test Conference, p.954-963, November 03-05, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Simulation

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Simulation; Verification

General Terms:
Design, Verification

Keywords:
ATPG, assertion test generation, design error model, logic verification, symbolic trajectory evaluation, validation