Functional test generation using design and property decomposition techniques

ABSTRACT

Functional verification of microprocessors is one of the most complex and expensive tasks in the current system-on-chip design methodology. Simulation using functional test vectors is the most widely used form of processor validation. A significant bottleneck in the validation of such systems is the lack of automated techniques for directed test generation. While existing model checking--based approaches have proposed several promising ideas for automated test generation, many challenges remain in applying them to industrial microprocessors. The time and resources required for test generation using existing model checking--based techniques can be prohibitively large. This article presents an efficient test generation technique using decompositional model checking. The contribution of the article 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 and an industrial processor based on Power Architecture™ Technology demonstrate several orders-of-magnitude reduction in validation effort by drastically reducing both test generation time and test program length.

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: A. Adir , E. Bin , O. Peled , A. Ziv, Piparazzi: a test program generator for micro-architecture flow verification, Proceedings of the Eighth IEEE International Workshop on High-Level Design Validation and Test Workshop, p.23, November 12-14, 2003
• 3: 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 annual ACM/IEEE Design Automation Conference, p.279-285, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217542]
• 4: Amla, N., Kurshan, R., McMillan, K., and Medel, R. 2003. Experimental analysis of different techniques for bounded model checking. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, Berlin, 34--48.
• 5: Amla, N. and McMillan, K. 2004. A hybrid of counterexample-based and proof-based abstraction. In Proceedings of the 5th International Formal Methods in Computer-Aided Design (FMCAD). Springer, Berlin, 260--274.
• 6: Amla, N., Du, X., Kuehlmann, A., Kurshan, R., and McMillan, K. 2005. An analysis of SAT-based model checking techniques in an industrial environment. In Proceedings of Correct Hardware Design and Verification Methods (CHARME). Springer, Berlin, 254--268.
• 7: Biere, A., Cimatti, A., and Clarke, E. M. 2003. Bounded model checking. Adv. Comput. 58.
• 8: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 9: 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
• 10: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 11: David Van Campenhout , Trevor Mudge , John P. Hayes, High-level test generation for design verification of pipelined microprocessors, Proceedings of the 36th annual ACM/IEEE Design Automation Conference, p.185-188, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309912]
• 12: Cadence SMV. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv.
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd annual ACM/IEEE Design Automation Conference, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 15: Fady Copty , Limor Fix , Ranan Fraer , Enrico Giunchiglia , Gila Kamhi , Armando Tacchella , Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proceedings of the 13th International Conference on Computer Aided Verification, p.436-453, July 18-22, 2001
• 16: Shai Fine , Avi Ziv, Coverage directed test generation for functional verification using bayesian networks, Proceedings of the 40th annual Design Automation Conference, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775907]
• 17: Freescale. PowerPCTM e500 Core Family Reference Manual. http://www.freescale.com/files/32bit/doc/ref manual/e500CORERM.pdf 2005.
• 18: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.146-162, Nov. 1999
• 19: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 20: Alon Gluska, Practical methods in coverage-oriented verification of the merom microprocessor, Proceedings of the 43rd annual Design Automation Conference, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1146996]
• 21: 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]
• 22: 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]
• 23: 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
• 24: 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
• 25: 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
• 26: 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
• 27: Jin, H. and F. Somenzi, F. 2005. An incremental algorithm to check satisfiability for bounded model-checking. In Proceedings of the International Workshop on Bounded Model-Checking (BMC'04). Elsevier, 51--65.
• 28: Heon-Mo Koo , Prabhat Mishra, Functional test generation using property decompositions for validation of pipelined processors, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 29: Heon-Mo Koo , Prabhat Mishra, Test generation using SAT-based bounded model checking for validation of pipelined processors, Proceedings of the 16th ACM Great Lakes symposium on VLSI, April 30-May 01, 2006, Philadelphia, PA, USA [doi>10.1145/1127908.1127991]
• 30: Heon-Mo Koo , Prabhat Mishra , Jayanta Bhadra , Magdy Abadir, Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study, Proceedings of the Seventh International Workshop on Microprocessor Test and Verification, p.33-36, December 04-05, 2006 [doi>10.1109/MTV.2006.10]
• 31: John L. Hennessy , David A. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
• 32: Kazuyoshi Kohno , Nobu Matsumoto, A new verification methodology for complex pipeline behavior, Proceedings of the 38th annual Design Automation Conference, p.816-821, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379072]
• 33: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 34: Deepak A. Mathaikutty , Sandeep K. Shukla , Sreekumar V. Kodakara , David Lilja , Ajit Dingankar, Design fault directed test generation for microprocessor validation, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 35: Deepak A. Mathaikutty , Sumit Ahuja , Ajit Dingankar , Sandeep Shukla, Model-driven test generation for system level validation, Proceedings of the 2007 IEEE International High Level Design Validation and Test Workshop, p.83-90, November 07-09, 2007 [doi>10.1109/HLDVT.2007.4392792]
• 36: P. Mishra , N. Dutt, Automatic functional test program generation for pipelined processors using model checking, Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop, p.99, October 27-29, 2002
• 37: Prabhat Mishra , Nikil Dutt, Graph-Based Functional Test Program Generation for Pipelined Processors, Proceedings of the conference on Design, automation and test in Europe, p.10182, February 16-20, 2004
• 38: Prabhat Mishra , Nikil Dutt, Functional Coverage Driven Test Generation for Validation of Pipelined Processors, Proceedings of the conference on Design, Automation and Test in Europe, p.678-683, March 07-11, 2005 [doi>10.1109/DATE.2005.162]
• 39: Mishra, P. and Dutt, N. (Eds.). 2008. In Processor Description Languages. Morgan Kaufmann, St. Louis, MO.
• 40: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th annual Design Automation Conference, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 41: NuSMV. http://nusmv.irst.itc.it/.
• 42: 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]
• 43: Hiren D. Patel , Sandeep K. Shukla, Model-driven validation of SystemC designs, Proceedings of the 44th annual Design Automation Conference, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278489]
• 44: Prasad, M., Biere, A., and Gupta, A. 2005. A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Tech. Trans. 7, 2, 156--173.
• 45: Property Specification Language. http://vhdl.org/ieee-1850/.
• 46: Jian Shen , Jacob A. Abraham, An RTL Abstraction Technique for Processor MicroarchitectureValidation and Test Generation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.67-81, Feb/April 2000 [doi>10.1023/A:1008388623771]
• 47: Ofer Shtrichman, Pruning Techniques for the SAT-Based Bounded Model Checking Problem, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.58-70, September 04-07, 2001
• 48: Tuerk, T., Schneider, K., and Gordon, M. 2007. Model-checking PSL using HOL and SMV. In Proceedings of the International Haifa Verification Conference (HVC 2006). Springer, Berlin, 1--15.
• 49: Shmuel Ur , Yaov Yadin, Micro architecture coverage directed generation of test programs, Proceedings of the 36th annual ACM/IEEE Design Automation Conference, p.175-180, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309909]
• 50: Noppanunt Utamaphethai , R. D. Shawn Blanton , John Paul Shen, Effectiveness of Microarchitecture Test Program Generation, IEEE Design & Test, v.17 n.4, p.38-49, October 2000 [doi>10.1109/54.895005]
• 51: Ilya Wagner , Valeria Bertacco , Todd Austin, StressTest: an automatic approach to test generation via activity monitors, Proceedings of the 42nd annual Design Automation Conference, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065788]
• 52: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th annual Design Automation Conference, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]

INDEX TERMS

General Terms:
Algorithms, Verification

Keywords:
Model checking, design decomposition, functional validation, pipelined processor, property decomposition, test generation