Equivalence Checking Method for Fixed-Point Arithmetic Datapaths

Based on the minimal strong Grébner 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 Grébner 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.