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
相关论文
共 50 条
  • [41] AQUILA: An equivalence checking system for large sequential designs
    Huang, SY
    Cheng, KT
    Chen, KC
    Huang, CY
    Brewer, F
    IEEE TRANSACTIONS ON COMPUTERS, 2000, 49 (05) : 443 - 464
  • [42] High-level vs. RTL combinational equivalence: An introduction (invited paper)
    Hu, Alan J.
    PROCEEDINGS 2006 INTERNATIONAL CONFERENCE ON COMPUTER DESIGN, 2007, : 274 - 279
  • [43] Design for verification in system-level models and RTL
    Mathur, Anmol
    Krishnaswamy, Venkat
    2007 44TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2007, : 193 - 198
  • [44] Probabilistic Equivalence Checking Based on High-Level Decision Diagrams
    Karputkin, Anton
    Ubar, Raimund
    Tombak, Mati
    Raik, Jaan
    2011 IEEE 14TH INTERNATIONAL SYMPOSIUM ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS (DDECS), 2011, : 423 - 428
  • [45] Equivalence Checking of High-Level Designs Based on Symbolic Simulation
    Matsumoto, Takeshi
    Nishihara, Tasuku
    Kojima, Yoshihisa
    Fujita, Masahiro
    2009 INTERNATIONAL CONFERENCE ON COMMUNICATIONS, CIRCUITS AND SYSTEMS PROCEEDINGS, VOLUMES I & II: COMMUNICATIONS, NETWORKS AND SIGNAL PROCESSING, VOL I/ELECTRONIC DEVICES, CIRUITS AND SYSTEMS, VOL II, 2009, : 1129 - +
  • [46] BOOSTER: Speeding up RTL property checking of digital designs by word-level abstraction
    Johannsen, P
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2001, 2102 : 373 - 377
  • [47] Power Reduction Techniques and Flows at RTL and System Level
    Mathur, Anmol
    Wang, Qi
    22ND INTERNATIONAL CONFERENCE ON VLSI DESIGN HELD JOINTLY WITH 8TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS, PROCEEDINGS, 2009, : 28 - +
  • [48] Equivalence checking method for fixed-point arithmetic datapaths
    Li, Donghai
    Ma, Guangsheng
    Hu, Jing
    Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao/Journal of Computer-Aided Design and Computer Graphics, 2009, 21 (01): : 27 - 32
  • [49] Sequential Circuit Equivalence Checking Method Based on Minimizing Automation
    Gu, Yuwan
    Shi, Guodong
    Xie, Shiyan
    Sun, Yudiang
    ADVANCED RESEARCH ON INDUSTRY, INFORMATION SYSTEMS AND MATERIAL ENGINEERING, PTS 1-7, 2011, 204-210 : 251 - +
  • [50] An Enhanced Equivalence Checking Method to Handle Bugs in Programs with Recurrences
    Dutta, Sudakshina
    Sarkar, Dipankar
    ENASE: PROCEEDINGS OF THE 11TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL SOFTWARE APPROACHES TO SOFTWARE ENGINEERING, 2016, : 254 - 259