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.
M S Chen, P Mishra. 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
N Bombieri, F Fummi, G Pravadelli. RTL-TLM equivalence checking based on simulation. In: Proceedings of IEEE East-West Design and Test symposium (EWDTS). 2008, 214−217 https://doi.org/10.1109/EWDTS.2008.5580149
3
L K Cai, D Gajski. Transaction level modeling in system level design. Center for Embedded Computer Systems, 2003
4
A Rose, S Swan, J Pierce, J M Fernandez. Transaction level modeling in SystemC. Open SystemC Initiative, 2005
5
N Bombieri, F Fummi, G Pravadelli. Automatic abstraction of RTL Ips into equivalent TLM descriptions. IEEE Transactions on Computers, 2010, 60(12): 1730−1743 https://doi.org/10.1109/TC.2010.187
6
K Hao, F Xie, S Ray, J Yang. Optimizing equivalence checking for behavioral synthesis. In: Proceedings of the Conference on Design, Automation and Test in Europe. 2010, 1500−1505
7
M Fujita. 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 https://doi.org/10.1109/hldvt.2004.1431267
8
M Fujita. 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 https://doi.org/10.1145/1109118.1109121
9
T Nishihara, T Matsumoto, M Fujitat. 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
S Vasudevan, V Viswanath, J A Abraham, J Tu. Sequential equivalence checking between system level and RTL descriptions. Design Automation for Embedded Systems, 2006, 12(4): 377−396 https://doi.org/10.1007/s10617-008-9033-z
11
S Vasudevan, V Viswanath, J A Abraham, J Tu. 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 https://doi.org/10.1109/memcod.2006.1695903
12
D Zhu, T Li, Y Guo, S K Li. 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 https://doi.org/10.1109/isqed.2008.4479812
13
T Li, Y Guo, W W Liu, C Y Ma. Efficient translation validation of highlevel synthesis. In: Proceedings of the 14th International Symposium on Quality Electronic Design. 2013, 516−523
14
T Li, Y Guo, W W Liu, M S Tang. 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 https://doi.org/10.1145/2483028.2483070
15
N Bombieri, A Fedeli, F Fummi, G Pravadelli. Hybrid incremental ABV for functional validation in TLM design flows. IEEE Design and Test of Computer, 2007, 24(2): 140−152 https://doi.org/10.1109/MDT.2007.48
16
N Bombieri, F Fummi, G Pravadelli. 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 https://doi.org/10.1109/date.2007.364404
17
D Große, M Groß, U Kühne, R Drechsler. 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 https://doi.org/10.1145/1973009.1973054
18
B Beizer. Software testing techniques. New Delhi: Dreamtech Press, 2003.
19
R Stewart. Unit test coverage as leading indicator of rework. Proceedings of EuroSTAR, 1997, 97
20
F D Frate, P Garg, A P Mathur, A Pasquini. On the correlation between code coverage and software reliability. In: Proceedings of the 6th International Symposium on Software Reliability Engineering. 1995, 124−132
21
Y K Malaiya, N Li, J Bieman, R Karcich, B Skbbe. The relationship between test coverage and reliability. In: Proceedings of the 5th IEEE International Symposium on Software Reliability Engineering. 1994, 186−195 https://doi.org/10.1109/issre.1994.341373
22
L Briand, D Pfahl. 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 https://doi.org/10.1109/issre.1999.809319
23
X Cai, M R Lyu. The effect of code coverage on fault detection under different testing profiles. ACM SIGSOFT Software Engineering Notes, 2005, 30(4): 1−7 https://doi.org/10.1145/1083274.1083288
24
J Sanguinetti, E Zhang. 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 https://doi.org/10.1109/hldvt.2010.5496649
25
M S Chen, P Mishra, D Kalita. Automatic RTL test generation from SystemC TLM specifications. ACM Transactions on Embedded Computing Systems, 2012, 11(2): 38 https://doi.org/10.1145/2220336.2220350
26
R Cytron, J Ferrante, B K Rosen, M N Wegman, F K Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 1991, 13(4): 451−490 https://doi.org/10.1145/115372.115320
27
S Ranise, C Tinelli. The satisfiability modulo theories library (SMTLIB). http://smtlib.cs.uiowa.edu/, 2006, 164
