research-article

Automatic RTL Test Generation from SystemC TLM Specifications

Authors:

Prabhat Mishra,

Dhrubajyoti KalitaAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 11, Issue 2

Article No.: 38, Pages 1 - 25

https://doi.org/10.1145/2220336.2220350

Published: 01 July 2012 Publication History

Abstract

SystemC transaction-level modeling (TLM) is widely used to enable early exploration for both hardware and software designs. It can reduce the overall design and validation effort of complex system-on-chip (SOC) architectures. However, due to lack of automated techniques coupled with limited reuse of validation efforts between abstraction levels, SOC validation is becoming a major bottleneck. This article presents a novel top-down methodology for automatically generating register transfer-level (RTL) tests from SystemC TLM specifications. It makes two important contributions: i) it proposes a method that can automatically generate TLM tests using various coverage metrics, and (ii) it develops a test refinement specification for automatically converting TLM tests to RTL tests in order to reduce overall validation effort. We have developed a tool which incorporates these activities to enable automated RTL test generation from SystemC TLM specifications. Case studies using a router example and a 64-bit Alpha AXP pipelined processor demonstrate that our approach can achieve intended functional coverage of the RTL designs, as well as capture various functional errors and inconsistencies between specifications and implementations.

References

[1]

Abdi, S. and Gajski, D. 2005. A formalism for functionality preserving system level transformations. In Proceedings of the Asia and South Pacific Design Automation Conference (ASPDAC). 139--144.

Digital Library

[2]

Abrar, S. and Thimmapuram, A. 2010. Functional refinement: A generic methodology for managing ESL abstractions. In Proceedings of the International Conference on VLSI Design (VLSID). 122--127.

Digital Library

[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.

Digital Library

[4]

Ara, K. and Suzuki, K. 2003. A proposal for transaction-level verification with component wrapper language. In Proceedings of the Design, Automation and Test in Europe Conference: Designers’ Forum. 20082.

Digital Library

[5]

Beyer, D., Chlipala, A., Henzinger, T., Jhala, R., and Majumdar, R. 2004. Generating tests from counterexamples. In Proceedings of the International Conference on Software Engineering (ICSE). 326--335.

Digital Library

[6]

Bombieri, N., Fummi, F., and Pravadelli, G. 2006. On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL. In Proceedings of the Design, Automation, and Test in Europe Conference (DATE). 1--6.

Digital Library

[7]

Bombieri, N., Fummi, F., and Pravadelli, G. 2007. Incremental ABV for functional validation of TL-to-RTL design refinement. In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 882--887.

Digital Library

[8]

Bombieri, N., Fummi, F., Pravadelli, G., and Marques-Silva, J. 2007. Towards equivalence checking between TLM and RTL models. In Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE). 113--122.

Digital Library

[9]

Bruce, A., Hashmi, M., Nightingale, A., Beavis, S., Romdhane, N., and Lennard, C. 2006. Maintaining consistency between SystemC and RTL system designs. In Proceedings of the Design Automation Conference (DAC). 85--89.

Digital Library

[10]

Cai, L. and Gajski, D. 2003. Transaction level modeling: An overview. In Proceedings of the International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS). 19--24.

Digital Library

[11]

Chen, M. and Mishra, P. 2010. Functional test generation using efficient property clustering and learning techniques. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 29, 3, 396--404.

Digital Library

[12]

Chen, M. and Mishra, P. 2011. Decision ordering based property decomposition for functional test generation. In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 167--172.

[13]

Chen, M. and Mishra, P. 2011. Property learning techniques for efficient generation of directed tests. IEEE Trans. Comput. 60, 6, 852--864.

Digital Library

[14]

Chen, M., Mishra, P., and Kalita, D. 2007. Towards RTL test generation from SystemC TLM specifications. In Proceedings of the International High-Level Design Validation and Test Workshop (HLDVT). 91--96.

Digital Library

[15]

Chen, M., Qin, X., and Mishra, P. 2010. Efficient decision ordering techniques for SAT-based test generation. In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 490--495.

Digital Library

[16]

Fedeli, A., Fummi, F., and Pravadelli, G. 2007. Properties incompleteness evaluation by functional verification. IEEE Trans. Comput. 56, 4, 528--544.

Digital Library

[17]

Ferrandi, F., Fummi, F., Gerli, L., and Sciuto, D. 1999. Symbolic functional vector generation for VHDL specifications. In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 442--446.

Digital Library

[18]

Fin, A., Fummi, F., Poncino, M., and Pravadelli, G. 2003. A SystemC-based framework for properties incompleteness evaluation. In Proceedings of the International Workshop on Microprocessor Test and Verification (MTV). 89--94.

[19]

Ghenassia, F. 2005. Transaction Level Modeling with SystemC. Springer, Dordrecht, Netherlands.

Digital Library

[20]

Habibi, A. and Tahar, S. 2004. Partial order reduction for scalable testing of SystemC TLM designs. In Proceedings of the International High-Level Design Validation and Test Workshop (HLDVT). 19--22.

[21]

Habibi, A. and Tahar, S. 2006. Design and verification of SystemC transaction-level models. IEEE Trans. Very Large Scale Integr. Syst. 14, 1, 57--68.

Digital Library

[22]

Jensen, K. 1997. A brief introduction to coloured Petri nets. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 203--208.

Digital Library

[23]

Jindal, R. and Jain, K. 2003. Verification of transaction-level SystemC models using RTL testbenches. In Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE). 199--203.

Digital Library

[24]

Karlsson, D., Eles, P., and Peng, Z. 2006. Formal verification of SystemC designs using a Petri-net based representation. In Proceedings of the Design, Automation, and Test in Europe Conference (DATE). 1228--1233.

Digital Library

[25]

Koo, H. and Mishra, P. 2009. Functional test generation using design and property decomposition techniques. ACM Trans. Embed. Comput. Syst. 8, 4.

Digital Library

[26]

Kroening, D. and Sharygina, N. 2005. Formal verification of SystemC by automatic hardware/software partitioning. In Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE). 101--110.

Digital Library

[27]

Kupferman, O. and Vardi, M. 1999. Vacuity detection in temporal model checking. In Proceedings of the Correct Hardware Design and Verification Methods Conference (CHARME). 82--96.

Digital Library

[28]

Lahbib, Y., Kamdem, R., Benalycherif, M., and Tourki, R. 2005. An automatic ABV methodology enabling PSL assertions across SLD flow for SoCs modeled in SystemC. Comput. Electr. Engi. 31, 4, 282--302.

Digital Library

[29]

Larsen, K., Pettersson, P., and Wang, Y. 1997. UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 1--2, 134--152.

Digital Library

[30]

Mishra, P. and Dutt, N. 2008. Specification-driven directed test generation for validation of pipelined processors. ACM Trans. Des. Autom. Electr. Syst. 13, 3, 1--36.

Digital Library

[31]

Moy, M., Maraninchi, F., and Maillet-Contoz, L. 2005. Lussy: A toolbox for the analysis of systems-on-a-chip at the transactional level. In Proceedings of the International Conference on Application of Concurrency to System Design. 26--35.

Digital Library

[32]

Rose, A., Swan, S., Pierce, J., and Fernandez, J. M. 2005. Transaction level modeling with SystemC. http://systemc.org.

[33]

Strichman, O. 2001. Pruning techniques for the SAT-based bounded model checking problem. In Proceedings of the Correct Hardware Design and Verification Methods Conference (CHARME). 58--70.

Digital Library

[34]

Wang, Z. and Ye, Y. 2005. The improvement for transaction level verification functional coverage. In Proceedings of the International Symposium on Circuits and Systems (ISCAS). 5850--5853.

Cited By

Witharana HJayasena AMishra P(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
https://dl.acm.org/doi/10.1145/3655621
Jayasena AMishra P(2023)Directed Test Generation for Hardware Validation: A SurveyACM Computing Surveys10.1145/363804656:5(1-36)Online publication date: 19-Dec-2023
https://dl.acm.org/doi/10.1145/3638046
Witharana HLyu YCharles SMishra P(2022)A Survey on Assertion-based Hardware VerificationACM Computing Surveys10.1145/351057854:11s(1-33)Online publication date: 9-Sep-2022
https://dl.acm.org/doi/10.1145/3510578
Show More Cited By

Index Terms

Automatic RTL Test Generation from SystemC TLM Specifications

Recommendations

A HW/SW co-verification framework for SystemC
Special section on ESTIMedia'12, LCTES'11, rigorous embedded systems design, and multiprocessor system-on-chip for cyber-physical systems

SystemC is widely used for modeling and simulation in hardware/software co-design. However, existing verification techniques are mostly ad-hoc and non-systematic. In this article, we present a systematic, comprehensive, and formally founded co-...
Towards RTL test generation from SystemC TLM specifications
HLDVT '07: Proceedings of the 2007 IEEE International High Level Design Validation and Test Workshop

SystemC Transaction Level Modeling (TLM) is widely used to reduce the overall design and validation effort of complex System-on-Chip (SOC) architectures. Due to lack of efficient techniques, the amount of reuse between abstraction levels is limited in ...
Mutation analysis for SystemC designs at TLM
LATW '11: Proceedings of the 2011 12th Latin American Test Workshop

Mutation analysis has been borrowed from the software testing domain as a technique for evaluating the quality of testbenches in validating digital systems. This paper presents a new method for applying mutation analysis on SystemC hardware designs at ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 11, Issue 2

July 2012

342 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/2220336

Issue’s Table of Contents

Copyright © 2012 ACM.

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

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 01 July 2012

Accepted: 01 March 2011

Revised: 01 December 2010

Received: 01 August 2009

Published in TECS Volume 11, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

52
Total Citations
View Citations
427
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Witharana HJayasena AMishra P(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
https://dl.acm.org/doi/10.1145/3655621
Jayasena AMishra P(2023)Directed Test Generation for Hardware Validation: A SurveyACM Computing Surveys10.1145/363804656:5(1-36)Online publication date: 19-Dec-2023
https://dl.acm.org/doi/10.1145/3638046
Witharana HLyu YCharles SMishra P(2022)A Survey on Assertion-based Hardware VerificationACM Computing Surveys10.1145/351057854:11s(1-33)Online publication date: 9-Sep-2022
https://dl.acm.org/doi/10.1145/3510578
Solt FJattke PRazavi KHardavellas NCampanoni SGrot BKarpuzcu U(2022)RemembERR: Leveraging Microprocessor Errata for Design Testing and ValidationProceedings of the 55th Annual IEEE/ACM International Symposium on Microarchitecture10.1109/MICRO56248.2022.00081(1126-1143)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1109/MICRO56248.2022.00081
Witharana HLyu YMishra P(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
https://dl.acm.org/doi/10.1145/3441297
Pomeranz I(2021)Equivalent Faults under Launch-on-Shift (LOS) Tests with Equal Primary Input VectorsACM Transactions on Design Automation of Electronic Systems10.1145/344001326:4(1-15)Online publication date: 15-Jan-2021
https://dl.acm.org/doi/10.1145/3440013
Fazzolari MBuccafurri FLax GPetrocchi M(2021)ExperienceJournal of Data and Information Quality10.1145/343930713:1(1-16)Online publication date: 13-Jan-2021
https://dl.acm.org/doi/10.1145/3439307
He EBai FHay CChen JBhagavatula V(2021)A Map Inference Approach Using Signal Processing from Crowd-sourced GPS DataACM Transactions on Spatial Algorithms and Systems10.1145/34317857:2(1-23)Online publication date: 15-Jan-2021
https://dl.acm.org/doi/10.1145/3431785
Costa RMiranda EDias PMoreira J(2021)ExperienceJournal of Data and Information Quality10.1145/342815513:1(1-13)Online publication date: 13-Jan-2021
https://dl.acm.org/doi/10.1145/3428155
Cohen MLee YSong Z(2021)Solving Linear Programs in the Current Matrix Multiplication TimeJournal of the ACM10.1145/342430568:1(1-39)Online publication date: 5-Jan-2021
https://dl.acm.org/doi/10.1145/3424305
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents