skip to main content
research-article

Specification-driven directed test generation for validation of pipelined processors

Published: 25 July 2008 Publication History

Abstract

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 effort, since shorter tests can obtain the same coverage goal compared to the random tests. This article presents a specification-driven directed test generation methodology. The proposed methodology makes three important contributions. First, a general graph model is developed that can capture the structure and behavior (instruction set) of a wide variety of pipelined processors. The graph model is generated from the processor specification. Next, we propose a functional fault model that is used to define the functional coverage for pipelined architectures. Finally, we propose two complementary test generation techniques: test generation using model checking, and test generation using template-based procedures. These test generation techniques accept the graph model of the architecture as input and generate test programs to detect all the faults in the functional fault model. Our experimental results on two pipelined processor models demonstrate several orders-of-magnitude reduction in overall validation effort by drastically reducing both test-generation time and number of test programs required to achieve a coverage goal.

References

[1]
Adir, A., Almog, E., Fournier, L., Marcus, E., Rimon, M., Vinov, M., and Ziv, A. 2004. Genesys-Pro: Innovations in test program generation for functional processor verification. IEEE Des. Test Comput. 21, 2 (Mar.-Apr.), 84--93.]]
[2]
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 the Design Automation Conference (DAC), 279--285.]]
[3]
Ammann, P., Black, P., and Majurski, W. 1998. Using model checking to generate tests from specifications. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM), 46--54.]]
[4]
Bhadra, J., Krishnamurthy, N., and Abadir, M. 2004. Enhanced equivalence checking: Towards a solidarity of functional verification and manufacturing test generation. IEEE Des. Test Comput. 21, 6 (Nov.-Dec.), 494--502.]]
[5]
Bjesse, P. and Kukula, J. 2004. Using counter example guided abstraction refinement to find complex bugs. In Proceedings of the Conference on Design Automation and Test in Europe (DATE), 156--161.]]
[6]
Cadence Design. 2008. Cadence home-page. http://www.cadence.com.]]
[7]
Campenhout, D., Mudge, T., and Hayes, J. 1999. High-Level test generation for design verification of pipelined microprocessors. In Proceedings of the Design Automation Conference (DAC), 185--188.]]
[8]
Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA.]]
[9]
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), 427--432.]]
[10]
Fine, S. and Ziv, A. 2003. Coverage directed test generation for functional verification using Bayesian networks. In Proceedings of the Design Automation Conference (DAC), 286--291.]]
[11]
FreeScale. 2005. PowerPC#8482; e500 Core Family Reference Manual. http://www.freescale.com/files/32bit/doc/ref_manual/e500CORERM.pdf.]]
[12]
Gaisler. 2008. LEON2 processor. http://www.gaisler.com/products/leon2/leon.html.]]
[13]
Gyllenhaal, J., Rau, B., and Hwu, W. 1996. HMDES version 2.0 specification. Tech. Rep. IMPACT-96-3, IMPACT Research Group, University of Illinois, Urbana. Illinois.]]
[14]
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 Conference on Design Automation and Test in Europe (DATE), 485--490.]]
[15]
Hennessy, J. and Patterson, D. 2003. Computer Architecture: A Quantitative Approach. Morgan Kaufmann.]]
[16]
Ho, P., Isles, A., and Kam, T. 1998. Formal verification of pipeline control using controlled token nets and abstract interpretation. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), 529--536.]]
[17]
Ho. R., Yang, C., Horowitz, M., and Dill, D. 1995. Architecture validation for processors. In Proceedings of the International Symposium on Computer Architecture (ISCA).]]
[18]
Iwashita, H., Kowatari, S., Nakata, T., and Hirose, F. 1994. Automatic test program generation for pipelined processors. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), 580--583.]]
[19]
Jacobi, C. 2002. Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving. In Proceedings of the Conference on Computer Aided Verification (CAV), E. Brinksma and K. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. Springer, 309--323.]]
[20]
Jhala, R. and McMillan, K. 2001. Microarchitecture verification by compositional model checking. In Proceedings of the Conference on Computer Aided Verification (CAV), G. Berry et al., Eds. Lecture Notes in Computer Science, vol. 2102. Springer, 396--410.]]
[21]
Koo, H. and Mishra, P. 2006a. Functional test generation using property decompositions for validation of pipelined processors. In Proceedings of the Conference on Design Automation and Test in Europe (DATE), 1240--1245.]]
[22]
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 Sympoisum on VLSI (GLSVLSI).]]
[23]
Koo, H.-M., Mishra, P., Bhadra, J., and Abadir, M. 2006. Directed micro-architectural test generation for an industrial processor: A case study. In Proceedings of the Conference on Microprocessor Test and Verification (MTV).]]
[24]
Krstic, A., Lai, W., Cheng, K-T., Chen, L., and Dey, S. 2002. Embedded software-based self-test for programmable core-based designs. IEEE Des. Test Comput. 19, 4, 18--27.]]
[25]
Mishra, P. and Dutt, N. 2005. Functional coverage driven test generation for validation of pipelined processors. In Proceedings of the Conference on Design Automation and Test in Europe (DATE), 678--683.]]
[26]
Mishra, P. and Dutt, N. 2004. Graph-Based functional test program generation for pipelined processors. In Proceedings of the Conference on Design Automation and Test in Europe (DATE), 182--187.]]
[27]
Mishra, P. and Dutt, N. 2002. Architecture description language driven functional test program generation for microprocessors using SMV. Tech. Rep. CECS 02-26, University of California, Irvine.]]
[28]
Mishra, P., Kejariwal, A., and Dutt, N. 2004. Synthesis-Driven exploration of pipleined embedded processors. In Proceedings of the International Conference on VLSI Design, 921--926.]]
[29]
Mishra, P., Dutt, N., and Nicolau, A. 2001. Functional abstraction driven design space exploration of heterogeneous programmable architectures. In Proceedings of the International Symposium on System Synthesis (ISSS), 256--261.]]
[30]
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.]]
[31]
Parthasarathy, G., Iyer, M., Feng, T., Wang, L-C., Cheng, K-T., and Abadir, M. 2002. Combining ATOG and symbolic simulation for efficient validation of array systems. In Proceedings of the International Test Conference (ITC), 203--212.]]
[32]
Piziali, A. 2004. Functional Verification Coverage Measurement and Analysis. Kluwer Academic.]]
[33]
Sparc. 2008. The Sparc Architecture Manual, version 8. http://www.sparc.com/resource.htm#V8.]]
[34]
SuperScalar. 2008. A superscalar version of the DLX processor. http://www.rs.e-technik.tu-darmstadt.de/TUD/res/dlxdocu/SuperscalarDLX.html.]]
[35]
Symbolic Model Verifier. 2008 SMV homepage. http://www.cs.cmu.edu/~modelcheck.]]
[36]
Tasiran, S. and Keutzer, K. 2001. Coverage metrics for functional validation of hardware designs. IEEE Des. Test Comput. 18, 4 (Jul.-Aug.), 36--45.]]
[37]
Thatte, S. and Abraham, J. 1980. Test generation for microprocessors. IEEE Trans. Comput. C-29, 6, 429--441.]]
[38]
Ur, S. and Yadin, Y. 1999. Micro architecture coverage directed generation of test programs. In Proceedings of the Design Automation Conference (DAC), 175--180.]]
[39]
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), 783--788.]]
[40]
Zivojnovic, V., Pees, S., and Meyr, H. 1996. LISA - Machine description language and generic machine model for HW/SW co-design. In Proceedings of the IEEE Workshop on VLSI Signal Processing, 127--136.]]

Cited By

View all
  • (2024)Incremental Concolic Testing of Register-Transfer Level DesignsACM Transactions on Design Automation of Electronic Systems10.1145/365562129:3(1-23)Online publication date: 3-May-2024
  • (2023)Directed Test Generation for Hardware Validation: A SurveyACM Computing Surveys10.1145/363804656:5(1-36)Online publication date: 19-Dec-2023
  • (2023)Mutation Analysis and Model Checking Guided Test Generation for SoC Run-Time Monitors2023 36th International Conference on VLSI Design and 2023 22nd International Conference on Embedded Systems (VLSID)10.1109/VLSID57277.2023.00057(240-245)Online publication date: Jan-2023
  • Show More Cited By

Index Terms

  1. Specification-driven directed test generation for validation of pipelined processors

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Transactions on Design Automation of Electronic Systems
      ACM Transactions on Design Automation of Electronic Systems  Volume 13, Issue 3
      July 2008
      370 pages
      ISSN:1084-4309
      EISSN:1557-7309
      DOI:10.1145/1367045
      Issue’s Table of Contents
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Journal Family

      Publication History

      Published: 25 July 2008
      Accepted: 01 March 2008
      Revised: 01 February 2008
      Received: 01 September 2007
      Published in TODAES Volume 13, Issue 3

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. Model checking
      2. functional validation
      3. test generation

      Qualifiers

      • Research-article
      • Research
      • Refereed

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)33
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 15 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2024)Incremental Concolic Testing of Register-Transfer Level DesignsACM Transactions on Design Automation of Electronic Systems10.1145/365562129:3(1-23)Online publication date: 3-May-2024
      • (2023)Directed Test Generation for Hardware Validation: A SurveyACM Computing Surveys10.1145/363804656:5(1-36)Online publication date: 19-Dec-2023
      • (2023)Mutation Analysis and Model Checking Guided Test Generation for SoC Run-Time Monitors2023 36th International Conference on VLSI Design and 2023 22nd International Conference on Embedded Systems (VLSID)10.1109/VLSID57277.2023.00057(240-245)Online publication date: Jan-2023
      • (2021)Directed Test Generation for Activation of Security Assertions in RTL ModelsACM Transactions on Design Automation of Electronic Systems10.1145/344129726:4(1-28)Online publication date: 15-Jan-2021
      • (2019)Random test program generation for verification and validation of the Samsung Reconfigurable ProcessorJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2019.05.00797:C(219-238)Online publication date: 1-Aug-2019
      • (2019)Automated Test Generation for Detection of Malicious FunctionalitySystem-on-Chip Security10.1007/978-3-030-30596-3_8(153-171)Online publication date: 23-Nov-2019
      • (2019)SoC Security Verification Using Property CheckingSystem-on-Chip Security10.1007/978-3-030-30596-3_7(137-152)Online publication date: 23-Nov-2019
      • (2019)Anomaly Detection Using Symbolic AlgebraSystem-on-Chip Security10.1007/978-3-030-30596-3_4(59-97)Online publication date: 23-Nov-2019
      • (2019)SoC Security Verification ChallengesSystem-on-Chip Security10.1007/978-3-030-30596-3_2(15-35)Online publication date: 23-Nov-2019
      • (2019)The Future of Security Validation and VerificationSystem-on-Chip Security10.1007/978-3-030-30596-3_12(273-279)Online publication date: 23-Nov-2019
      • Show More Cited By

      View Options

      Login options

      Full Access

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media