A Hybrid Method for Equivalence Checking Between System Level and RTL

被引:0
作者
Hu, Jian [1 ]
Hu, Minhui [1 ]
Zhao, Kuang [1 ]
Kang, Yun [1 ]
Yang, Haitao [1 ]
Cheng, Jie [1 ]
机构
[1] Natl Univ Def Technol, Res Inst 63, Nanjing 210000, Peoples R China
基金
中国国家自然科学基金;
关键词
Equivalence checking; system level model; finite state machine with datapath; deep state sequence; VERIFICATION; VALIDATION; TLM;
D O I
10.1142/S0218126622501687
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Deep State Sequence-based (DSS) equivalence checking and path-based equivalence checking have been successfully applied for verification of digital designs between System Level Model (SLM) and Register Transfer Level (RTL). The DSS-based equivalence checking method can validate designs without mapping information, but the query size for each DSS is large compared with path-based verification. The query size for path-based methods is small, but the number of comparisons is large. In this work, we combine the advantages of DSS-based methods and path-based methods. We use DSS-based methods to find the corresponding paths and use cut-points like in path-based methods to split the DSS to reduce the query size. Finite State Machine with Datapath (FSMD) is used to represent the SLM and RTL models. Experimental results demonstrate that our method can effectively validate the designs and reduce the query size for DSS-based equivalence checking method.
引用
收藏
页数:18
相关论文
共 22 条
[1]  
[Anonymous], 1967, P S APPL MATH
[2]   Verification of Code Motion Techniques Using Value Propagation [J].
Banerjee, Kunal ;
Karfa, Chandan ;
Sarkar, Dipankar ;
Mandal, Chittaranjan .
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2014, 33 (08) :1180-1193
[3]  
Bombieri N., P DES TEST S LVIV UK, P214
[4]  
Bombieri N, 2007, DES AUT TEST EUROPE, P882
[5]   Assertion-Based Functional Consistency Checking between TLM and RTL Models [J].
Chen, Mingsong ;
Mishra, Prabhat .
2013 26TH INTERNATIONAL CONFERENCE ON VLSI DESIGN AND 2013 12TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS (VLSID), 2013, :320-325
[6]   Translation Validation of Loop Invariant Code Optimizations Involving False Computations [J].
Chouksey, Ramanuj ;
Karfa, Chandan ;
Bhaduri, Purandar .
VLSI DESIGN AND TEST, 2017, 711 :767-778
[7]   EFFICIENTLY COMPUTING STATIC SINGLE ASSIGNMENT FORM AND THE CONTROL DEPENDENCE GRAPH [J].
CYTRON, R ;
FERRANTE, J ;
ROSEN, BK ;
WEGMAN, MN ;
ZADECK, FK .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1991, 13 (04) :451-490
[8]  
Gajski D., 1999, High-level synthesis
[9]  
GroSSsse D., 2011, PROC 21 GREAT LAKES, P223
[10]   Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition [J].
Gupta, Shubhani ;
Saxena, Aseem ;
Mahajan, Anmol ;
Bansal, Sorav .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 :365-382