Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths

被引：18
作者：
Fujita, M [1 ]
机构：
[1] Univ Tokyo, VLSI Design & Educ Ctr, Tokyo 1138656, Japan
来源：
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS | 2005年 / 10卷 / 04期
关键词：
verification; languages; high-level synthesis; behavior synthesis; formal verification; equivalence checking;
D O I：
10.1145/1109118.1109121
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this article, we present techniques for comparison between behavioral level and register transfer level (RTL) design descriptions by mapping the designs into virtual controllers and virtual datapaths. We also discuss about how the equivalence between behavioral level and RTL designs can be defined precisely using the proposed "attribute statements" in an interactive fashion. Implementation issues as well as considerations on real life industrial design examples are also presented.
引用
收藏
页码：610 / 626
页数：17
相关论文
共 19 条
  • [1] ABDI S, 2003, CECSTR0341 U CAL
  • [2] Tool support for fine-grained software inspection
    Anderson, P
    Reps, T
    Teitelbaum, T
    Zarins, M
    [J]. IEEE SOFTWARE, 2003, 20 (04) : 42 - +
  • [3] BALL T, 2000, P WORKSH ADV VER
  • [4] BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819
  • [5] Clarke E., 2003, Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451), P368
  • [6] Clarke EM, 1999, LECT NOTES COMPUT SC, V1703, P298
  • [7] Automatic formal verification of DSP software
    Currie, DW
    Hu, AJ
    Rajan, S
    Fujita, M
    [J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 130 - 135
  • [8] The standard SpecC language
    Fujita, M
    Nakamura, H
    [J]. ISSS'01: 14TH INTERNATIONAL SYMPOSIUM ON SYSTEM SYNTHESIS, 2001, : 81 - 86
  • [9] Gajski D.D., 2000, SpecC: Specification Language and Methodology
  • [10] JAIN J, 1995, DES AUT CON, P420
12