Generating test programs to cover pipeline interactions

ABSTRACT

Functional validation of a processor design through execution of a suite of test programs is common industrial practice. In this paper, we develop a high-level architectural specification driven methodology for systematic test-suite generation. Our primary contribution is an automated test-suite generation methodology that covers all possible processor pipeline interactions. To accomplish this automation, we (1) develop a fully formal processor model based on communicating extended finite state machines, and (2) traverse the processor model for on-the-fly generation of short test programs covering all reachable states and transitions. Our test generation method achieves several orders of magnitude reduction in test-suite size compared to the previously proposed formal approaches for test generation, leading to drastic reduction in validation effort.

REFERENCES

• 1: A. Aharon et al. Test program generation for functional verification of PowerPC processors in IBM. In DAC, 1995.
• 2: T. Austin, E. Larson, and D. Ernst. Simplescalar: An infrastructure for computer system modeling. IEEE Computer, 35(2), 2002.
• 3: K. T. Cheng and A. S. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In DAC, 1993.
• 4: T. A. Diep and J. P. Shen. Systematic validation of pipeline interlock for superscalar microarchitectures. In FTCS, 1995.
• 5: D. Geist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur, and Y. Wolfsthal. Coverage-directed test generation using symbolic techniques. In FMCAD, 1996.
• 6: H-M. Koo and P. Mishra. Functional test generation using design and property decomposition techniques. ACM TECS, 8(4), 2009.
• 7: P. Mishra and N. Dutt. Specification-driven directed test generation for validation of pipelined processors. ACM TODAES, 13(2), 2008.
• 8: W. Qin and S. Malik. Flexible and formal modeling of microprocessors with application to retargetable simulation. In DATE, 2003.
• 9: W. Qin, S. Rajagopalan, and S. Malik. A formal concurrency model based architecture description language for synthesis of software development tools. In LCTES, 2004.
• 10: S. Ur and Y. Yadin. Micro-arachitecture coverage directed generation of test programs. In DAC, 1999.
• 11: Q. Zhu, A. Shrivastava, and N. Dutt. Functional and timing validation of partially bypassed processor pipelines. In DATE, 2007.

INDEX TERMS

General Terms:
Algorithms, Verification

Keywords:
automated test generation, pipelines, state space exploration