An Equivalence Checking Method for C Descriptions Based on Symbolic Simulation with Textual Differences

Takeshi MATSUMOTO  Hiroshi SAITO  Masahiro FUJITA  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E88-A   No.12   pp.3315-3323
Publication Date: 2005/12/01
Online ISSN: 
DOI: 10.1093/ietfec/e88-a.12.3315
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: Simulation and Verification
Keyword: 
equivalence checking,  C-based system level design,  symbolic simulation,  textual difference,  program slicing,  

Full Text: PDF(869.2KB)
>>Buy this Article


Summary: 
In this paper, an efficient equivalence checking method for two C descriptions is described. The equivalence of two C descriptions is proved by symbolic simulation. Symbolic simulation used in this paper can prove the equivalence of all of the variables in the descriptions. However, it takes long time to verify the equivalence of all of the variables if large descriptions are given. Therefore, in order to improve the verification, our method identifies textual differences between descriptions. The identified textual differences are used to reduce the number of equivalence checkings among variables. The proposed method has been implemented in C language and evaluated with several C descriptions.