Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths

  • Masahiro Fujita
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


A behavior-RTL equivalence checking method based on bottom-up reasoning is presented. Behavior and RTL descriptions are converted into dependence graphs from which virtual controllers/datapaths are generated. Actual equivalence checking is based on isomorphism analysis on dependence graphs and also virtual controllers/datapaths. First equivalence classes on partial computations are extracted by using Boolean reasoning on virtual controllers/datapaths. Then these equivalence classes are used to prove the equivalence of the entire descriptions in a bottom-up way.


  1. 1.
    Kuehlmann, A., Krohm, F.: Equivalence Checking Using Cuts and Heaps. In: Proceedings of the 34th ACM/IEEE Design Automation Conference 1997 (1997)Google Scholar
  2. 2.
    Fujita, M.: On equivalence checking between behavioral and RTL descriptions. In: HLDVT 2004 (November 2004); Also see (for more reference)
  3. 3.
    Weiser, M.: Program slices: Formal, psychological, and practical investigations of an automatic program abstraction. PhD thesis, University of Michigan (1979)Google Scholar
  4. 4.
    Tanabe, K., Sasaki, S., Fujita, M.: Program slicing for system level designs in SpecC. In: IASTED Conference on Advances in Computer Science and Technology (November 2004)Google Scholar
  5. 5.
    SoC Environment, University of California, Irvine,

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Masahiro Fujita
    • 1
  1. 1.VLSI Design and Education CenterThe University of TokyoTokyoJapan

Personalised recommendations