Heon-Mo Koo
Prabhat Mishra
Skip Abstract Section
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.
- ]]Adir, A., Almog, E., Fournier, L., Marcus, E., Rimon, M., Vinov, M., and Ziv, A. 2004. Genesyspro: Innovations in test program generation for functional processor verification. IEEE Des. Test Comput. 21, 2, 84--93. Google Scholar
Digital Library
- ]]Adir, A., Bin, E., Peled, O., and Ziv, A. 2003. Piparazzi: A test program generator for micro-architecture flow verification. In Proceedings of High-Level Design Validation and Test Workshop (HLDVT). IEEE, Los Alamitos, CA, 23--28. Google ScholarDigital Library
- ]]Aharon, A., Goodman, D., Levinger, M., Lichtenstein, Y., Malka, Y., Metzger, C., Molcho, M., and Shurek, G. 1995. Test program generation for functional verification of PowerPC processors in IBM. In Proceedings of Design Automation Conference (DAC). ACM, New York, 279--285. Google ScholarDigital Library
- ]]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. Google ScholarDigital Library
- ]]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.Google ScholarCross Ref
- ]]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. Google ScholarDigital Library
- ]]Biere, A., Cimatti, A., and Clarke, E. M. 2003. Bounded model checking. Adv. Comput. 58.Google Scholar
- ]]Biere, A., Cimatti, A., Clarke, E., and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, Berlin, 193--207. Google ScholarDigital Library
- ]]Bjesse, P. and Kukula, J. 2004. Using counter example guided abstraction refinement to find complex bugs. In Proceedings of Design Automation and Test in Europe (DATE). IEEE, Los Alamitos, CA, 156--161. Google ScholarDigital Library
- ]]Bryant, R. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35, 8, 677--691. Google ScholarDigital Library
- ]]Campenhout, D., Mudge, T., and Hayes, J. 1999. High-level test generation for design verification of pipelined micro-processors. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 185--188. Google ScholarDigital Library
- ]]Cadence SMV. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv.Google Scholar
- ]]Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- ]]Clarke, E., Grumberg, O., McMillan, K., and Zhao, X. 1995. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 427--432. Google ScholarDigital Library
- ]]Copty, F., Fix, L., Fraer, R., Giunchiglia, G., Kamhi, G., Tacchella, A., and Vardi, M. 2001. Benefits of bounded model checking at an industrial setting. In Proceedings of Computer-Aided Verification (CAV). Springer, Berlin, 436--453. Google ScholarDigital Library
- ]]Fine, S. and Ziv, A. 2003. Coverage directed test generation for functional verification using Bayesian networks. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 286--291. Google ScholarDigital Library
- ]]Freescale. PowerPCTM e500 Core Family Reference Manual. http://www.freescale.com/files/32bit/doc/ref manual/e500CORERM.pdf 2005.Google Scholar
- ]]Gargantini, A. and Heitmeyer, C. 1999. Using model checking to generate tests from requirements specifications. ACM SIGSOFT Software Engin. Notes. 24, 146--162. Google ScholarDigital Library
- ]]Goldberg, E. and Novikov, Y. 2002. BerkMin: A fast and robust SAT-solver. In Proceedings of Design Automation and Test in Europe (DATE). IEEE, Los Alamitos, CA, 142--149. Google ScholarDigital Library
- ]]Gluska, A. 2006. Practical methods in coverage-oriented verification of the Merom micro-processor. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 332--337. Google ScholarDigital Library
- ]]Halambi, A., Grun, P., Ganesh, V., Khare, A., Dutt, N., and Nicolau, A. 1999. EXPRESSION: A language for architecture exploration through compiler/simulator retargetability. In Proceedings of Design Automation and Test in Europe (DATE). IEEE, Los Alamitos, CA, 485--490. Google ScholarDigital Library
- ]]Ho, P., Isles, A., Kam, T. 1998. Formal verification of pipeline control using controlled token nets and abstract interpretation. In Proceedings of International Conference on Computer-Aided Design (ICCAD). ACM, New York, 529--536. Google ScholarDigital Library
- ]]Ho, R., Yang, C., Horowitz, M. A., Dill, D. 1995. Architecture validation for processors. In Proceedings of International Symposium on Computer Architecture (ISCA). ACM, New York. Google ScholarDigital Library
- ]]Iwashita, H., Kowatari, S., Nakata, T., Hirose, F. 1994. Automatic test program generation for pipelined processors. In Proceedings of International Conference on Computer-Aided Design (ICCAD). ACM, New York, 580--583. Google ScholarDigital Library
- ]]Jacobi, C. 2002. Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving. In Proceedings of Computer-Aided Verification (CAV). Springer-Verlag, Berlin, 309--323. Google ScholarDigital Library
- ]]Jhala, R. and McMillan, K. L. 2001. Micro-architecture verification by compositional model-checking. In Proceedings of Computer-Aided Verification (CAV). Springer-Verlag, Berlin, 396--410. Google ScholarDigital Library
- ]]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.Google Scholar
- ]]Koo, H. and Mishra, P. 2006a. Functional test generation using property decompositions for validation of pipelined processors. In Proceedings of Design Automation and Test in Europe (DATE). IEEE, Los Alamitos, CA. Google ScholarDigital Library
- ]]Koo, H. and Mishra, P. 2006b. Test generation using SAT-based bounded model-checking for validation of pipelined processors. In Proceedings of the ACM Great Lakes Symposium on VLSI (GLSVLSI). ACM, New York. Google ScholarDigital Library
- ]]Koo H., Mishra, P., Bhadra, J., and Abadir, M. 2006. Directed micro-architectural test generation for an industrial processor: A case study. In Proceedings of Micro-processor Test and Verification (MTV). IEEE, Los Alamitos, CA. Google ScholarDigital Library
- ]]Hennessy, J. and Patterson, D. 2003. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, St. Louis, MO. Google ScholarDigital Library
- ]]Kohno, K. and Matsumoto, N. 2001. A new verification methodology for complex pipeline behavior. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 816--821. Google ScholarDigital Library
- ]]Marques-Silva, J. and Sakallah, K. 1999. Grasp: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 5, 506--521. Google ScholarDigital Library
- ]]Mathaikutty, D., Kodakara, S., Dingankar, A., Shukla, S., and Lilja, D. 2007. Design fault directed test generation for micro-processor validation. In Proceedings of Design Automation and Test in Europe (DATE). IEEE, Los Alamitos, CA. Google ScholarDigital Library
- ]]Mathaikutty, D., Ahuja, S., Dingankar, A., and Shukla, S. 2007. Model-driven test generation for system level validation. In Proceedings of High-Level Design Validation and Test (HLDVT). IEEE, Los Alamitos, CA. Google ScholarDigital Library
- ]]Mishra, P. and Dutt, N. 2002. Automatic functional test program generation for pipelined processors using model-checking. In Proceedings of High-Level Design Validation and Test (HLDVT). IEEE, Los Alamitos, CA, 99--103. Google ScholarDigital Library
- ]]Mishra, P. and Dutt, N. 2004. Graph-based functional test program generation for pipelined processors. In Proceedings of Design Automation and Test in Europe. IEEE, Los Alamitos, CA, 182--187. Google ScholarDigital Library
- ]]Mishra, P. and Dutt, N. 2005. Functional coverage driven test generation for validation of pipelined processors. In Proceedings of Design Automation and Test in Europe. IEEE, Los Alamitos, CA, 678--683. Google ScholarDigital Library
- ]]Mishra, P. and Dutt, N. (Eds.). 2008. In Processor Description Languages. Morgan Kaufmann, St. Louis, MO. Google ScholarDigital Library
- ]]Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 530--535. Google ScholarDigital Library
- ]]NuSMV. http://nusmv.irst.itc.it/.Google Scholar
- ]]Parthasarathy, G., Iyer, M., Cheng, K. T., and Wang, L. 2004. Safety property verification using sequential SAT and bounded model-checking. IEEE Des. Test Comput. 21, 2, 132--143. Google ScholarDigital Library
- ]]Patel, H. and Shukla, S. 2007. Model-driven validation of SystemC designs micro-processor. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 29--34. Google ScholarDigital Library
- ]]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.Google ScholarDigital Library
- ]]Property Specification Language. http://vhdl.org/ieee-1850/.Google Scholar
- ]]Shen, J. and Abraham, J. 2000. An RTL abstraction technique for processor micro-architecture validation and test generation. J. Electron. Test. 16, 1-2, 67--81. Google ScholarDigital Library
- ]]Strichman, O. 2001. Pruning techniques for the SAT-based bounded model-checking problem. In Proceedings of Correct Hardware Design and Verification Methods (CHARME). Springer-Verlag, Berlin, 58--70. Google ScholarDigital Library
- ]]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. Google ScholarDigital Library
- ]]Ur, S. and Yadin, Y. 1999. Micro-architecture coverage directed generation of test programs. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 175--180. Google ScholarDigital Library
- ]]Utamaphethai, N., Blanton, R. D. S., and Shen, J. P. 2000. Effectiveness of micro-architecture test program generation. IEEE Des. Test 17, 4, 38--49. Google ScholarDigital Library
- ]]Wagner, I., Bertacco, V., and Austin, T. 2005. Stresstest: An automatic approach to test generation via activity monitors. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 783--788. Google ScholarDigital Library
- ]]Whittemore, J., Kim, J., and Sakallah, K. 2001. SATIRE: A new incremental satisfiability engine. In Proceedings of the Design Automation Conference (DAC). ACM, New York, 542--545. Google ScholarDigital Library
Recommendations
Test generation using SAT-based bounded model checking for validation of pipelined processors
GLSVLSI '06: Proceedings of the 16th ACM Great Lakes symposium on VLSIFunctional verification is one of the major bottlenecks in microprocessor design. Simulation-based techniques are the most widely used form of processor verification. Efficient test generation is crucial for the simulation-based verification. We present ...
Specification-driven directed test generation for validation of pipelined processors
Functional validation is a major bottleneck in pipelined processor design due to the combined effects of increasing design complexity and lack of efficient techniques for directed test generation. Directed test vectors can reduce overall validation ...
Instruction-level test methodology for CPU core self-testing
TIS is an instruction-level methodology for processor core self-testing that enhances instruction set of a CPU with test instructions. Since the functionality of test instructions is the same as the NOP instruction, NOP instructions can be replaced with ...
Comments