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] DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis
    Abderehman, Mohammed
    Reddy, Theegala Rakesh
    Karfa, Chandan
    PROCEEDINGS OF THE TWENTY THIRD INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2022), 2022, : 64 - 70
  • [42] Content Learning Indicator in Equivalence Checking between Skills Module and Academic Module for APEL Process
    Amin, N. F. M. M.
    Kaprawi, N.
    INTERNATIONAL JOURNAL OF EMERGING TECHNOLOGIES IN LEARNING, 2019, 14 (20) : 58 - 72
  • [43] Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems
    Soudjani, Sadegh Esmaeil Zadeh
    Majumdar, Rupak
    Nagapetyan, Tigran
    QUANTITATIVE EVALUATION OF SYSTEMS (QEST 2017), 2017, 10503 : 351 - 367
  • [44] The ODYSSEY approach to early simulation-based equivalence checking at ESL level using automatically generated executable transaction-level model
    Goudarzi, Maziar
    Hessabi, Shaahin
    MohammadZadeh, Naser
    Zainolabedini, Nasim
    MICROPROCESSORS AND MICROSYSTEMS, 2008, 32 (07) : 364 - 374
  • [45] Formal Model for Checking the Interoperability Between the Components of the IoT system
    Timenko, A., V
    Shkarupylo, V. V.
    Oliinyk, A. O.
    Hrushko, S. S.
    PROBLEMELE ENERGETICII REGIONALE, 2019, (1-1): : 69 - 78
  • [46] System-level optimisation of hybrid energy powered irrigation system
    Alam, Marzia
    Imran, Muhammad
    Sultan, Muhammad
    Manzoor, Umar
    Khan, Zafar A.
    Rezk, Ahmed
    Alaswad, Abed
    RENEWABLE ENERGY, 2024, 234
  • [47] Hybrid Control Method for Adaptive Optics System
    Wang Jiaying
    Guo Youming
    Kong Lin
    Chen Kele
    Rao Changhui
    LASER & OPTOELECTRONICS PROGRESS, 2020, 57 (23)
  • [48] System safety property-oriented test sequences generating method based on model checking
    Zhang, Y.
    Zhao, X. Q.
    Zheng, W.
    Tang, T.
    COMPUTERS IN RAILWAYS XII: COMPUTER SYSTEM DESIGN AND OPERATION IN RAILWAYS AND OTHER TRANSIT SYSTEMS, 2010, 114 : 747 - +
  • [49] A hybrid domain overlapping method for coupling System Thermal and CFD codes
    Huxford, Aaron
    Leite, Victor Coppo
    Merzari, Elia
    Zou, Ling
    Petrov, Victor
    Manera, Annalisa
    ANNALS OF NUCLEAR ENERGY, 2023, 189
  • [50] High Level Fault Injection Method for Evaluating Critical System Parameter Ranges
    Roux, Julie
    Beroulle, Vincent
    Morin-Allory, Katell
    Leveugle, Regis
    Bossuet, Lilian
    Cezilly, Frederic
    Berthoz, Frederic
    Genevrier, Gilles
    Cerisier, Francois
    2020 27TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS (ICECS), 2020,