Equivalence checking between SLM and TLM using coverage directed simulation

Abstract

The increasing complexity of digital systems makes designers begin to design using abstract system level modeling (SLM). However, SLM brings new challenges for verification engineers to guarantee the functional equivalence between SLM specifications and lower-level implementations such as those of transaction level modeling (TLM). This paper proposes a novel method for equivalence checking between SLM and TLM based on coverage directed simulation. Our method randomly simulates an SLM model and uses an satisfiability modulo theories (SMT) solver to generate stimuli for the uncovered area with the direction of a composite coverage metric (code coverage and functional coverage). Then we run all the generated stimuli (random stimuli and direct stimuli) on both SLM and TLM designs. At the same time, the selected observation variables are compared to evaluate the equivalence between SLM and TLM. Promising experimental results show that our equivalence checking method is more efficient with lower simulation cost.

Keywords

system level modeling / transaction level modeling / equivalence checking / composite coverage / SMT

References

[1] Chen M S, Mishra P. Assertion-based functional consistency checking between TLM and RTL models. In: Proceedings of VLSI Design and the 12th International Conference on Embedded Systems. 2012, 320−325

[2] Bombieri N, Fummi F, Pravadelli G. RTL-TLM equivalence checking based on simulation. In: Proceedings of IEEE East-West Design and Test symposium (EWDTS). 2008, 214−217

[3] Cai L K, Gajski D. Transaction level modeling in system level design. Center for Embedded Computer Systems, 2003

[4] Rose A, Swan S, Pierce J, Fernandez J M. Transaction level modeling in SystemC. Open SystemC Initiative, 2005

[5] Bombieri N, Fummi F, Pravadelli G. Automatic abstraction of RTL Ips into equivalent TLM descriptions. IEEE Transactions on Computers, 2010, 60(12): 1730−1743

[6] Hao K, Xie F, Ray S, Yang J. Optimizing equivalence checking for behavioral synthesis. In: Proceedings of the Conference on Design, Automation and Test in Europe. 2010, 1500−1505

[7] Fujita M. On equivalence checking between behavioral and RTL descriptions. In: Proceedings of the 9th IEEE International High-Level Design Validation and Test Workshop. 2004, 179−184

[8] Fujita M. Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths. ACM Transactions on Design Automation of Electronic Systems, 2005, 10(4): 610−626

[9] Nishihara T, Matsumoto T, Fujitat M. Equivalence checking with rulebased equivalence propagation and high-level synthesis. In: Proceedings of the 11th Annual IEEE International High-Level Design Validation and Test Workshop. 2006, 162−169

[10] Vasudevan S, Viswanath V, Abraham J A, Tu J. Sequential equivalence checking between system level and RTL descriptions. Design Automation for Embedded Systems, 2006, 12(4): 377−396

[11] Vasudevan S, Viswanath V, Abraham J A, Tu J. Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In: Proceedings of the 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design. 2006, 71−80

[12] Zhu D, Li T, Guo Y, Li S K. 2D Decomposition sequential equivalence checking of system level and RTL descriptions. In: Proceedings of the 9th International Symposium on Quality Electronic Design. 2008, 637−642

[13] Li T, Guo Y, Liu W W, Ma C Y. Efficient translation validation of highlevel synthesis. In: Proceedings of the 14th International Symposium on Quality Electronic Design. 2013, 516−523

[14] Li T, Guo Y, Liu W W, Tang M S. Translation validation of scheduling in high-level synthesis. In: Proceedings of the 23rd ACM International Conference on Great Lakes Symposium on VLSI. 2013, 101−106

[15] Bombieri N, Fedeli A, Fummi F, Pravadelli G. Hybrid incremental ABV for functional validation in TLM design flows. IEEE Design and Test of Computer, 2007, 24(2): 140−152

[16] Bombieri N, Fummi F, Pravadelli G. Incremental ABV for functional validation of TL-to-RTL design refinement. In: Proceedings of the Conference on Design, Automation and Test in Europe. 2007, 882−887

[17] Große D, Groß M, Kühne U, Drechsler R. Simulation-based equivalence checking between SystemC models at different levels of abstraction. In: Proceedings of the 21st Edition of the Great Lakes Symposium on Great Lakes Symposium on VLSI. 2011, 223−228

[18] Beizer B. Software testing techniques. New Delhi: Dreamtech Press, 2003.

[19] Stewart R. Unit test coverage as leading indicator of rework. Proceedings of EuroSTAR, 1997, 97

[20] Frate F D, Garg P, Mathur A P, Pasquini A. On the correlation between code coverage and software reliability. In: Proceedings of the 6th International Symposium on Software Reliability Engineering. 1995, 124−132

[21] Malaiya Y K, Li N, Bieman J, Karcich R, Skbbe B. The relationship between test coverage and reliability. In: Proceedings of the 5th IEEE International Symposium on Software Reliability Engineering. 1994, 186−195

[22] Briand L, Pfahl D. Using simulation for assessing the real impact of test coverage on defect coverage. In: Proceedings of the 10th IEEE International Symposium on Software Reliability Engineering, 1999, 148−157

[23] Cai X, Lyu M R. The effect of code coverage on fault detection under different testing profiles. ACM SIGSOFT Software Engineering Notes, 2005, 30(4): 1−7

[24] Sanguinetti J, Zhang E. The relationship of code coverage metrics on high-level and RTL code. In: Proceedings of IEEE International Highlevel Design Validation and Test Workshop. 2010, 138−141

[25] Chen M S, Mishra P, Kalita D. Automatic RTL test generation from SystemC TLM specifications. ACM Transactions on Embedded Computing Systems, 2012, 11(2): 38

[26] Cytron R, Ferrante J, Rosen B K, Wegman M N, Zadeck F K. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 1991, 13(4): 451−490

[27] Ranise S, Tinelli C. The satisfiability modulo theories library (SMTLIB). http://smtlib.cs.uiowa.edu/, 2006, 164

[28] De Moura L, Bjørner N. Z3: an efficient SMT solver. Lecture Notes in Computer Science, 2008, 4963: 337−340

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg