Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath

Tasuku NISHIHARA  Takeshi MATSUMOTO  Masahiro FUJITA 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E92-D  No.5  pp.972-984
Publication Date: 2009/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Hardware Verification
Keyword: 
high-level synthesis,  behavioral synthesis,  formal verification,  equivalence checking, 

Full Text: PDF(1020.2KB)

Summary: 
Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.