Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra

As the size and functional complexity of IC designs increase, it has become important to address verification issues at early stages of the IC design flow. This means that IC designers require automated verification tools at higher levels of abstraction. Because of this, formal verification methods, such as equivalence verification, have become important for register transfer level or behavioral level verification. However, most of the existing techniques for equivalence verification are based on BDD or Boolean SAT, which are generally geared towards verification of designs implemented at lower levels of abstraction, such as gate level and circuitlayout level, and can hardly satisfy the high-level verification requirements. So in this paper, a new algorithm for the equivalence verification of high-level datapaths based on polynomial symbolic algebra is proposed. After researching further the method to describe behaviors of complex datapaths using polynomial expressions, the general form of the polynomial set representations for high-level datapaths is obtained. The functional equivalence of high-level datapaths is then defined from the perspective of common zeros of polynomial sets, and an efficient algebraic solution based on Grbner basis computation is presented. Experimental results on a variety of public benchmark suites show the efficiency of the proposed approach.