Title: Exploiting vanishing polynomials for equivalence verification of fixed-size arithmetic datapaths
Abstract: This paper addresses the problem of equivalence verification of high-level/RTL descriptions. The focus is on datapath-oriented designs that implement univariate polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of over Z/sub 2//sup m/ in other words, to prove f(x)%2/sup m/ /spl equiv/ g(x)%2/sup m/. This paper transforms the equivalence verification problem into proving (f(x) - g(x))%2/sup m/ /spl equiv/ 0. Exploiting the theory of vanishing polynomials over finite integer rings, a systematic algorithmic procedure is derived to establish whether or not a given polynomial vanishes (always evaluates to 0) over Z/sub 2//sup m/. Experiments demonstrate the effectiveness of our approach over contemporary techniques.
Publication Year: 2006
Publication Date: 2006-08-15
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 10
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot