High-level design verification of microprocessors via error modeling

ABSTRACT

A design verification methodology for microprocessor hardware based on modeling design errors and generating simulation vectors for the modeled errors via physical fault testing techniques is presented. We have systematically collected design error data from a number of microprocessor design projects. The error data is used to derive error models suitable for design verification testing. A class of basic error models is identified and shown to yield tests that provide good coverage of common error types. To improve coverage for more complex errors, a new class of conditional error models is introduced. An experiment to evaluate the effectiveness of our methodology is presented. Single actual design errors are injected into a correct design, and it is determined if the methodology will generate a test that detects the actual errors. The experiment has been conducted for two microprocessor designs and the results indicate that very high coverage of actual design errors can be obtained with test sets that are complete for a small number of synthetic error models.

REFERENCES

• 1: ABADIR, M. S., FERGUSON, J., AND KIRKLAND, T.E. 1988. Logic design verification via test generation. IEEE Trans. Computer-Aided Des. 7, 1 (Jan.), 138-148.
• 2: A. Aharon , B. Dorfman , E. Gofman , M. Leibowitz , V. Schwartzburd , A. Bar-David, Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generator, IBM Systems Journal, v.30 n.4, p.527-538, 1991
• 3: Hussain Al-Asaad , John P. Hayes, Design verification via simulation and automatic test pattern generation, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.174-180, November 05-09, 1995, San Jose, California, United States
• 4: AL-ASAAD, H., VAN CAMPENHOUT, D., HAYES, J. P., MUDGE, T., AND BROWN, R. B. 1997. High-level design verification of microprocessors via error modeling. In Digest of the IEEE High-Level Design Validation and Test Workshop. IEEE Computer Society Press, Los Alamitos, CA, 194-201.
• 5: Ghassan Al Hayek , Chantal Robach, From Specification Validation to Hardware Testing: A Unified Method, Proceedings of the IEEE International Test Conference on Test and Design Validity, p.885-893, October 20-25, 1996
• 6: BHATTACHARYA, D., AND HAYES, J.P. 1985. High-Level test generation using bus faults. In Digest of the 15th International Symposium on Fault-Tolerant Computing. IEEE, New York, 65-70.
• 7: Boris Beizer, Software testing techniques (2nd ed.), Van Nostrand Reinhold Co., New York, NY, 1990
• 8: BRGLEZ, F., AND FUJIWARA, H. 1985. A neutral netlist of 10 combinational benchmark circuits and a target translator in Fortran. In Proceedings of the IEEE Symposium on Circuits and Systems. IEEE Computer Society Press, Los Alamitos, CA, 695-698.
• 9: BROWN, R., ET AL. 1996. Complementary GaAs technology as a GHz microprocessor. In Technical Digest of the GaAs IC Symposium. IEEE Piscataway, NJ, 313-316.
• 10: CADENCE DESIGN SYSTEMS, INC. 1994. Verilog-XL Reference Manual. Cadence Design Systems, Inc.
• 11: Françoise Casaubieilh , Anthony McIsaac , Mike Benjamin , Mike Bartley , François Pogodalla , Frédéric Rocheteau , Mohamed Belhadj , Jeremy Eggleton , Gérard Mas , Geoff Barrett , Christian Berthet, Functional verification methodology of Chameleon processor, Proceedings of the 33rd annual conference on Design automation, p.421-426, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240599]
• 12: CEDERQVIST, P., ET AL. 1995. Version management with CVS. Signum Support AB, Linkoping, Sweden.
• 13: A. Chandra , V. Iyengar , D. Jameson , R. Jawalekar , I. Nair , B. Rosen , M. Mullen , J. Yoon , R. Armoni , D. Geist , Y. Wolfsthal, AVPGEN—a test generator for architecture verification, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.3 n.2, p.188-200, June 1995 [doi>10.1109/92.386220]
• 14: COLWELL, R. P., AND LETHIN, R.J. 1994. Latent design faults in the development of the Multiflow TRACE/200. IEEE Trans. Reliabil. 43, 4 (Dec.), 557-565.
• 15: DEMILLO, R. A., LIPTON, R. J., AND SAYWARD, F.G. 1978. Hints on test data selection: Help for the practicing programmer. IEEE Comput. (Apr.), 34-41.
• 16: Srinivas Devadas , Abhijit Ghosh , Kurt Keutzer, An observability-based code coverage metric for functional simulation, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.418-425, November 10-14, 1996, San Jose, California, United States
• 17: Gopi Ganapathy , Ram Narayan , Glenn Jorden , Denzil Fernandez , Ming Wang , Jim Nishimura, Hardware emulation for functional verification of K5, Proceedings of the 33rd annual conference on Design automation, p.315-318, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240578]
• 18: M. C. Hansen , J. P. Hayes, High-level test generation using physically-induced faults, Proceedings of the 13th IEEE VLSI Test Symposium (VTS'95), p.20, April 30-May 03, 1995
• 19: David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
• 20: Anoosh Hosseini , Dimitrios Mavroidis , Pavlos Konas, Code generation and analysis for the functional verification of micro processors, Proceedings of the 33rd annual conference on Design automation, p.305-310, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240574]
• 21: INTEL CORPORATION. 1998. Pentium Processor Specification Update. Available from http:// www.intel.com.
• 22: Michael Katrowitz , Lisa M. Noack, I'm done simulating; now what? Verification coverage analysis and correctness checking of the DEC chip 21164 Alpha microprocessor, Proceedings of the 33rd annual conference on Design automation, p.325-330, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240580]
• 23: KIM, H. 1996. C880 high-level Verilog description. Internal Report. Univ. Michigan, Ann Arbor, MI.
• 24: K. N. King , A. Jefferson Offutt, A Fortran language system for mutation-based software testing, Software—Practice & Experience, v.21 n.7, p.685-718, July 1991 [doi>10.1002/spe.4380210704]
• 25: Jainendra Kumar, Prototyping the M68060 for Concurrent Verification, IEEE Design & Test, v.14 n.1, p.34-41, January 1997 [doi>10.1109/54.573363]
• 26: MIPS TECHNOLOGIES, INC. 1994. MIPS R4OOOPC/SC Errata, Processor Revision 2.2 and 3.0. (May).
• 27: A. Jefferson Offutt , Ammei Lee , Gregg Rothermel , Roland H. Untch , Christian Zapf, An experimental determination of sufficient mutant operators, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.2, p.99-118, April 1996 [doi>10.1145/227607.227610]
• 28: PALNITKAR, S., SAGGURTI, P., AND KUANG, S.-H. 1994. Finite state machine trace analysis program. In Proceedings of the International Verilog HDL Conference. IEEE Computer Science Press, Los Alamitos, CA, 52-57.
• 29: POSTIFF, M. 1996. LC-2 Programmer's Reference Manual, rev. 3.1. Univ. Michigan, Ann Arbor, MI.
• 30: TEXAS INSTRUMENTS. 1988. The TTL Logic Data Book. Texas Instruments, Dallas, TX.
• 31: WOODWARD, M.R. 1993. Mutation testing--Its origin and evolution. Inf. Softw. Tech. 35, (Mar.). 163-169.
• 32: Michael Yoeli, Formal Verification of Hardware Design, IEEE Computer Society Press, Los Alamitos, CA, 1990

INDEX TERMS

Primary Classification:
  B. Hardware

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION

General Terms:
Verification

Keywords:
design errors, design verification, error modeling