High Level Formal Verification for Polynomial Datapath

Taylor expansion diagram (TED) is a compact, canonical, world level graph-based representation, and it can effectively express multi-variate polynomial. In this paper, variable replacement algorithm and variable mergence algorithm for TED are presented. Based on variable replacement algorithm, variable ordering algorithm and variable merging algorithm, an algorithm of backward-construction TED is proposed, which is used to verify the equivalence between the behaviors specification and register transfer level (RTL) implementation of polynomial datapath. Experimental results show that the proposed method is effective.