Formal Verification for Polynomial Datapaths Based on Weighted Generalized Lists
Dong Hai Li, Hai Chen Wang, Zhong Lei Fan, Xiao‐Jun Yang · Advanced materials research · 2012
Weighted generalized list (WGL) can effectively express multi-variate polynomial. In this paper, variable ordering algorithm, variable replacement algorithm and variable mergence algorithm for WGL are presented. Based on variable replacement algorithm, variable ordering algorithm and variable merging algorithm, an algorithm of backward-construction WGL is proposed, which is used to verify the equivalence between the behaviors specification and register transfer level (RTL) implementation of polynomial datapaths. Experimental results show that the proposed method is effective.