Mingsong Chen
Prabhat Mishra
Dhrubajyoti Kalita
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.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Chen, M. and Mishra, P. 2011. Property learning techniques for efficient generation of directed tests. IEEE Trans. Comput. 60, 6, 852--864. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Fedeli, A., Fummi, F., and Pravadelli, G. 2007. Properties incompleteness evaluation by functional verification. IEEE Trans. Comput. 56, 4, 528--544. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Ghenassia, F. 2005. Transaction Level Modeling with SystemC. Springer, Dordrecht, Netherlands. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Koo, H. and Mishra, P. 2009. Functional test generation using design and property decomposition techniques. ACM Trans. Embed. Comput. Syst. 8, 4. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Larsen, K., Pettersson, P., and Wang, Y. 1997. UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 1--2, 134--152.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Rose, A., Swan, S., Pierce, J., and Fernandez, J. M. 2005. Transaction level modeling with SystemC. http://systemc.org.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
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 systemsSystemC 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 WorkshopSystemC 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 WorkshopMutation 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