Equivalence checking with rule-based equivalence propagation and high-level synthesis

Equivalence checking is one of the most important issues in VLSI designs to guarantee that bugs do not enter the design 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 the same datapath so that the two designs have the same bit-level accuracy. Then the word-level equivalence checking techniques can be applied satisfying the bit-level accuracy. Also, as our method propagates equivalences from inputs to outputs with the equivalence rules of control structures, name correspondences among registers or variables are not required. By those rules, designs which have loops can be verified without unrolling. Experimental results with realistic examples show that our method can verify those designs in practical periods.