Functional test generation using property decompositions for validation of pipelined processors

ABSTRACT

Functional validation is a major bottleneck in pipelined processor design. Simulation using functional test vectors is the most widely used form of processor validation. While existing model checking based approaches have proposed several promising ideas for efficient test generation, many challenges remain in applying them to realistic pipelined processors. The time and resources required for test generation using existing model checking based techniques can be extremely large. This paper presents an efficient test generation technique using decompositional model checking. The contribution of the paper is the development of both property and design decomposition procedures for efficient test generation of pipelined processors. Our experimental results using a multi-issue MIPS processor demonstrate several orders-of-magnitude reduction in memory requirement and test generation time.

REFERENCES

• 1: Allon Adir , Eli Almog , Laurent Fournier , Eitan Marcus , Michal Rimon , Michael Vinov , Avi Ziv, Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification, IEEE Design & Test, v.21 n.2, p.84-93, March 2004 [doi>10.1109/MDT.2004.1277900]
• 2: Aharon Aharon , Dave Goodman , Moshe Levinger , Yossi Lichtenstein , Yossi Malka , Charlotte Metzger , Moshe Molcho , Gil Shurek, Test program generation for functional verification of PowerPC processors in IBM, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.279-285, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217542]
• 3: Ashok Halambi , Peter Grun , Vijay Ganesh , Asheesh Khare , Nikil Dutt , Alex Nicolau, EXPRESSION: a language for architecture exploration through compiler/simulator retargetability, Proceedings of the conference on Design, automation and test in Europe, p.100-es, January 1999, Munich, Germany [doi>10.1145/307418.307549]
• 4: Christian Jacobi, II, Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving, Proceedings of the 14th International Conference on Computer Aided Verification, p.309-323, July 27-31, 2002
• 5: David Van Campenhout , Trevor Mudge , John P. Hayes, High-level test generation for design verification of pipelined microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.185-188, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309912]
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 8: Ganapathy Parthasarathy , Madhu K. Iyer , Kwang-Ting (Tim) Cheng , Li-C. Wang, Safety Property Verification Using Sequential SAT and Bounded Model Checking, IEEE Design & Test, v.21 n.2, p.132-143, March 2004 [doi>10.1109/MDT.2004.1277906]
• 9: Hiroaki Iwashita , Satoshi Kowatari , Tsuneo Nakata , Fumiyasu Hirose, Automatic test program generation for pipelined processors, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.580-583, November 06-10, 1994, San Jose, California, United States
• 10: www-cad.eecs.berkeley.edu/~kenmcmil/smv. Cadence SMV.
• 11: Ilya Wagner , Valeria Bertacco , Todd Austin, StressTest: an automatic approach to test generation via activity monitors, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA [doi>10.1145/1065579.1065788]
• 12: John L. Hennessy , David A. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
• 13: Michael Behm , John Ludden , Yossi Lichtenstein , Michal Rimon , Michael Vinov, Industrial experience with test generation languages for processor verification, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996578]
• 14: Per Bjesse , James Kukula, Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Proceedings of the conference on Design, automation and test in Europe, p.10156, February 16-20, 2004
• 15: Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289082]
• 16: P. Mishra and N. Dutt. Graph-based functional test program generation for pipelined processors. DATE, 182--187, 2004.
• 17: P. Mishra and N. Dutt. Functional Verification of Programmable Embedded Architectures -- A Top-Down Approach. Springer, 2005.
• 18: Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, Proceedings of the 22nd annual international symposium on Computer architecture, p.404-413, June 22-24, 1995, S. Margherita Ligure, Italy
• 19: Ranjit Jhala , Kenneth L. McMillan, Microarchitecture Verification by Compositional Model Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.396-410, July 18-22, 2001
• 20: Shai Fine , Avi Ziv, Coverage directed test generation for functional verification using bayesian networks, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775907]
• 21: Shmuel Ur , Yaov Yadin, Micro architecture coverage directed generation of test programs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.175-180, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309909]