Equivalence checking of C programs by locally performing symbolic simulation on dependence graphs

In this paper, we propose a formal equivalence checking method for source-to-source refinements in C programs for hardware behavioral descriptions. In the method, the textual differences between the two programs are identified at first to get hints where the equivalence must be checked. Then, the equivalence of differences is verified by symbolic simulation and validity checking techniques. If the equivalence is not established, our method incrementally extends statements to be verified based on dependency until the equivalence is proved. For the extensions, the method uses dependence graphs of the programs. Finally, through the experimental results, we show the method can efficiently perform equivalence checking