中文摘要：

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路，但却难以满足高层次设计验证要求．由此，以多项式符号代数为理论基础，提出了一个高层次数据通路的等价验证算法．深入研究了使用多项式表达式描述复杂数据通路行为的方法，得到了高层次数据通路的多项式集合表示的一般形式．从多项式集合公共零点的角度定义了高层次数据通路的功能等价，给出了一个基于Groebner基计算的有效代数求解算法．针对不同基准数据通路的实验结果表明了该算法的有效性．

英文摘要：

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 Groebner basis computation is presented. Experimental results on a variety of public benchmark suites show the efficiency of the proposed approach.