An Equivalence Checking Method for C Descriptions Based on Symbolic Simulation with Textual Differences(Simulation and Verification, <Special Section>VLSI Design and CAD Algorithms)

概要

論文の詳細を見る
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.
社団法人電子情報通信学会の論文
2005-12-01