中文摘要：

以vanishing多项式理想的极小强Grobner基为理论基础，提出一种针对定点算术数据通路的等价性检验方法．通过使用多项式函数建模定点数据通路的设计规范和寄存器传输级实现，将等价性检验问题转化为判断一个多项式函数是否为vanishing多项式、vanishing多项式理想的极小强Grobner基被用来有效地解决该问题．理论分析和实验结果表明，与现有的算法相比，该方法在时间消耗上具有一定的优势．

英文摘要：

Based on the minimal strong Grobner basis of the ideal of vanishing polynomials, an algorithm of equivalence checking for fixed-point arithmetic datapaths was proposed. By modeling design specifications and register transfer level implementations for fixed-point datapaths as polynomial functions, the equivalence checking was reduced to verify whether a polynomial function is a vanishing polynomial, which can be solved by the minimal strong Grobner basis of the ideal of vanishing polynomials efficiently. Theoretical analysis and experimental results demonstrated the superiority in time consumption of the proposed algorithm in comparison with the existent algorithms.