Formal Verification for Polynomial Datapaths Based on Weighted Generalized Lists

Abstract:

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.

• Periodical: Advanced Materials Research (Volumes 433-440)
• Pages: 6483-6489
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.433-440.6483
• Online since: January 2012
• Authors: Dong Hai Li, Hai Chen Wang, Zhong Lei Fan, Xiao Jun Yang
• Keywords: Formal Verification, Polynomial Datapaths, Weighted Generalized List

References

[1] Smith J, Micheli D G. Polynomial circuit models for component matching in high-level synthesis, IEEE Transactions on Very Large Scale Integration Systems, 2001, vol. 9 (no. 6). 783-800.

DOI: 10.1109/92.974892

[2] Peymandoust A, Micheli D G. Application of symbolic computer algebra in high-level data-flow synthesis, IEEE Transaction on Computer-Aided Design of IntegraWGL Circuit and Systems, 2003, vol. 22. (no. 9). 1154-1165.

DOI: 10.1109/tcad.2003.816213

[3] Peymandoust A, Simunic T, Micheli D G. Complex instruction and software library mapping for embedded software using symbolic algebra, IEEE Transaction on Computer-Aided Design of IntegraWGL Circuit and Systems, 2003, vol. 22. (no. 8). 964-975.

DOI: 10.1109/tcad.2003.814951

[4] Peymandoust A, Simunic T, Micheli D G. Complex library mapping for embedded software using symbolic algebra. Design Automation Conference, 2002, 325-330.

DOI: 10.1109/dac.2002.1012644

[5] Peymandoust A, Simunic T, Micheli D G. Low power embedded software optimization using symbolic algebra, Design, Automation and Test in Europe conference and Exhibition, 2002, 1052-1058.

DOI: 10.1109/date.2002.998432

[6] Hosangadi A, Kastner R, Fallah F. Energy efficient hardware synthesis of polynomial expressions, International Conference on VLSI Design, 2005, 653-658.

DOI: 10.1109/icvd.2005.90

[7] Bryant R E. Graph based algorithm for Boolean function manipulation, IEEE Transaction on Computers, 1986, vol. C-35. (no. 8), 677-691.

DOI: 10.1109/tc.1986.1676819

[8] Bcker B, Drechsler R, and Ender R. On the computational power of bit-level and word-level decision diagrams, Asia and South Pacific Design Automation Conference, 1997, 461-467.

DOI: 10.1109/aspdac.1997.600304

[9] Sasao T, Nagayama S. Representations of elementary functions using binary moment diagrams, International Symposium on Multiple-Valued Logic, 2006, 28-33.

DOI: 10.1109/ismvl.2006.37

[10] Du Z J, Ma G S, Feng G. A new model for verification. Journal of Harbin Institute of Technology. 2007, 14(3): 305-310.

[11] Li D H, Ma G S, Hu J. The method of equivalence verification for high level datapaths. Journal of Harbin Engineering University. 2008, 29(6): 583-588. (In Chinese).