|
|
Equivalence checking between SLM and TLM using coverage directed simulation |
Jian HU(), Tun LI, Sikun LI |
School of Computer, National University of Defense Technology, Changsha 410073, China |
|
|
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
|
Corresponding Author(s):
Jian HU
|
Just Accepted Date: 31 December 2014
Issue Date: 10 November 2015
|
|
1 |
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
|
28 |
L De Moura, N Bjørner. Z3: an efficient SMT solver. Lecture Notes in Computer Science, 2008, 4963: 337−340
https://doi.org/10.1007/978-3-540-78800-3_24
|
[1] |
Supplementary Material-Highlights in 3-page ppt
|
Download
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|