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.

For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. associative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates, and check the satisfiability of formulas under the constraint. In this report, we show an algorithm for checking satisfiability with equivalence constraint and also experimental results.

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.