A Unified Sequential Equivalence Checking Methodology to Verify RTL Designs with High-Level Functional and Protocol Specification Models

被引:0
|
作者
Carlos Ivan Castro Marquez
Marius Strum
Wang Jiang Chau
机构
[1] University of Sao Paulo,School of Engineering
来源
关键词
Functional verification; Formal methods; Equivalence checking; High-level specification; Interface protocol; RTL design;
D O I
暂无
中图分类号
学科分类号
摘要
Digital application complexity has steadily made it harder to discover and debug behavioral inconsistencies at register transfer level (RTL). Aiming to bring a solution, several techniques have appeared as alternatives to verify that a circuit description meets the requirements of its corresponding functional specification. Simulation-based verification is still far from reaching high state coverage because of cycle-accurate slowness. Formal approaches are exhaustive in theory, but due to computational limitations, workarounds must always be adopted to check only a portion of the design at a time. Bounded model checking is one of the most popular formal methods; however, a strong disadvantage resides in defining and determining the quality of the set of properties to verify. Sequential equivalence checking is also an effective alternative, but it can only be applied between circuit descriptions where a one-to-one correspondence for states and memory elements is expected. This paper presents a formal methodology to verify RTL descriptions through direct comparison with: 1) a high-level reference model and 2) a protocol reference model. Thus, it is possible to verify behavioral and interface protocol separately. Complete sequences of states are extracted from the reference models and the RTL design, and compared to determine if the design implementation is correct. The natural discrepancies between the models and RTL code are considered, including non-matching interface and memory elements, state mapping, and process concurrency. The validity of the methodology is formally justified and a related tool was developed to show, through examples, that the approach may be applied on real designs.
引用
收藏
页码:255 / 273
页数:18
相关论文
共 5 条
  • [1] A Unified Sequential Equivalence Checking Methodology to Verify RTL Designs with High-Level Functional and Protocol Specification Models
    Castro Marquez, Carlos Ivan
    Strum, Marius
    Chau, Wang Jiang
    [J]. JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2015, 31 (03): : 255 - 273
  • [2] A Unified Sequential Equivalence Checking Approach to Verify High-Level Functionality and Protocol Specification Implementations in RTL Designs
    Castro Marquez, Carlos Ivan
    Strum, Marius
    Chau, Wang Jiang
    [J]. 2014 15TH LATIN AMERICAN TEST WORKSHOP - LATW, 2014,
  • [3] 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,
  • [4] Equivalence Checking of High-Level Designs Based on Symbolic Simulation
    Matsumoto, Takeshi
    Nishihara, Tasuku
    Kojima, Yoshihisa
    Fujita, Masahiro
    [J]. 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 - +
  • [5] An Analog Behavioral Equivalence Checking Methodology for Simulink Models and Circuit Level Designs
    Saglamdemir, Muharrem Orkun
    Dundar, Gunhan
    Sen, Alper
    [J]. 2015 INTERNATIONAL CONFERENCE ON SYNTHESIS, MODELING, ANALYSIS AND SIMULATION METHODS AND APPLICATIONS TO CIRCUIT DESIGN (SMACD), 2015,