Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths
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.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.Fujita, M.: On equivalence checking between behavioral and RTL descriptions. In: HLDVT 2004 (November 2004); Also see http://www.cad.t.u-tokyo.ac.jp (for more reference)
- 3.Weiser, M.: Program slices: Formal, psychological, and practical investigations of an automatic program abstraction. PhD thesis, University of Michigan (1979)Google Scholar
- 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.SoC Environment, University of California, Irvine, http://www.cecs.uci.edu/~cad/sce.html