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.

Bounded model checking is a widely used formal technique in both hardware and software verification. However, it cannot be applied if the bounds (number of time frames to be analyzed) become large, and deep bugs which are observed only through very long counter-examples cannot be detected. This paper presents a method concatenating multiple bounded model checking results efficiently with symbolic simulation. A bounded model checking with a large bound is recursively decomposed into multiple ones with smaller bounds, and symbolic simulation on each counterexample supports smooth connections to the others. A strong heuristic for the proposed method that targets deep bugs is also presented, and can be applied together with other efficient bounded model checking methods since it does not touch the basic bounded model checking algorithm.