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 条
  • [1] Sequential equivalence checking between system level and RTL descriptions
    Shobha Vasudevan
    Vinod Viswanath
    Jacob A. Abraham
    JiaJin Tu
    [J]. Design Automation for Embedded Systems, 2008, 12 : 377 - 396
  • [2] Sequential equivalence checking between system level and RTL descriptions
    Vasudevan, Shobha
    Viswanath, Vinod
    Abraham, Jacob A.
    Tu, JiaJin
    [J]. DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2008, 12 (04) : 377 - 396
  • [3] Solver Technology for System-level to RTL Equivalence Checking
    Koelbl, Alfred
    Jacoby, Reily
    Jain, Himanshu
    Pixley, Carl
    [J]. DATE: 2009 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, VOLS 1-3, 2009, : 196 - 201
  • [4] Embedded Tutorial: Formal equivalence checking between system-level models and RTL
    Koelbl, A
    Lu, Y
    Mathur, A
    [J]. ICCAD-2005: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, 2005, : 965 - 971
  • [5] A Path-Based Equivalence Checking Method Between System Level and RTL Descriptions Using Machine Learning
    Hu, Jian
    Hu, Yongyang
    Lv, Qi
    Wang, Wentao
    Wang, Guanwu
    Chen, Guilin
    Wang, Kang
    Kang, Yun
    Yang, Haitao
    [J]. JOURNAL OF CIRCUITS SYSTEMS AND COMPUTERS, 2021, 30 (04)
  • [6] Automatic decomposition for sequential equivalence checking of system level and RTL descriptions
    Vasudevan, Shobha
    Viswanath, Vinod
    Abraham, Jacob A.
    Tu, Jiajin
    [J]. FOURTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2006, : 71 - +
  • [7] On equivalence checking between behavioral and RTL descriptions
    Fujita, M
    [J]. NINTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2004, : 179 - 184
  • [8] Formal Equivalence Checking between High-Level and RTL Hardware Designs
    Castro Marquez, Carlos Ivan
    Strum, Marius
    Chau, Wang Jiang
    [J]. 2013 14TH IEEE LATIN-AMERICAN TEST WORKSHOP (LATW2013), 2013,
  • [9] Leveraging sequential equivalence checking to enable system-level to RTL flows
    Urard, Pascal
    Maalej, Asma
    Guizzetti, Roberto
    Chawla, Nitin
    Krishnaswamy, Venkatram
    [J]. 2008 45TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2008, : 816 - 821
  • [10] Formal Equivalence Checking Between SLM and RTL Descriptions
    Hu, Jian
    Li, Tun
    Li, Sikun
    [J]. 2015 28TH IEEE INTERNATIONAL SYSTEM-ON-CHIP CONFERENCE (SOCC), 2015, : 131 - 136