基于指针操作的乘法器验证程序优化
Optimization of Multiplication Circuit Verification Program Based on Pointer Operations
DOI: 10.12677/aam.2024.138349, PDF,   
作者: 王晨瑞, 江建国：辽宁师范大学数学学院，辽宁 大连
关键词: 乘法器验证；Gröbner基方法；C语言指针；Verification of Multipliers； Gröbner Basis Method； C Pointers
摘要: 乘法器电路验证是算术电路验证领域内的一个重大难题。Gröbner基方法是其中目前最为有效的验证方法之一。基于此方法开发的Amulet程序通过减少中间变量数量提高了验证效率，但是对于大型乘法器，验证速度慢的问题仍存在。本文对Amulet的关键算法进行了进一步优化，通过指针操作对函数进行重写，缩短了验证的时间，并根据实验数据体现了其在大型乘法器验证中的应用优势，为形式化验证技术的未来研究提供了参考。
Abstract: The verification of multiplier circuits is a significant challenge in the field of arithmetic circuit verification. The Gröbner basis method is currently one of the most effective verification methods available. The Amulet program, developed based on this method, improves verification efficiency by reducing the number of intermediate variables. However, for large multipliers, the verification speed remains an issue. This paper further optimizes the key algorithms of Amulet, by rewriting functions through pointer operations, reduces verification time. Experimental results demonstrate its advantages in the verification of large multipliers. It provides a reference for future research in formal verification techniques.
文章引用：王晨瑞, 江建国. 基于指针操作的乘法器验证程序优化[J]. 应用数学进展, 2024, 13(8): 3666-3676. https://doi.org/10.12677/aam.2024.138349

参考文献

[1] Sharangpani, H. and Barton, M.L. (1994) Statistical Analysis of Floating Point Flaw in the Pentium Processor. Intel Corporation.
[2] Bryant, R.E. (1986) Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35, 677-691. [Google Scholar] [CrossRef] 
[3] Bryant, R.E. and Chen, Y. (2001) Verification of Arithmetic Circuits Using Binary Moment Diagrams. International Journal on Software Tools for Technology Transfer, 3, 137-155. [Google Scholar] [CrossRef] 
[4] Chen, Y. and Bryant, R.E. (1995) Verification of Arithmetic Circuits with Binary Moment Diagrams. 32nd Design Automation Conference, San Francisco, 12-16 June 1995, 535-541. [Google Scholar] [CrossRef] 
[5] Biere, A. (2016) Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. SAT Competition 2016, 65-66.
[6] Biere, A. (2016) Weaknesses of CDCL Solvers, August 2016. Fields Institute Workshop on Theoretical Foundations of SAT Solving.
http://www.fields.utoronto.ca/talks/weaknesses-cdcl-solvers
[7] Kaufmann, M. and Moore, J.S. (2019) ACL2 Version 8.2.
http://www.cs.utexas.edu/users/moore/acl2/
[8] Kaufmann, D. (2020) AMulet 1.5.
https://github.com/d-kfmnn/amulet
[9] Buchberger, B. (1965) Ein Algorithmuszum Auffinden der Basiselemente des Restklassenringesnacheinemnulldimensiona-lenPolynomideal. Ph.D. Thesis, University of Innsbruck.
[10] Ciesielski, M.J., Su, T., Yasin, A. and Yu, C. (2019) Understanding Algebraic Rewriting for Arithmetic Circuit Verification: A Bit-Flow Model. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39, 1346-1357.
[11] Kaufmann, D. (2020) Formal Verification of Multiplier Circuits using Computer Algebra. Ph.D. Thesis, Johannes Kepler University Linz.
[12] Mahzoon, A., Große, D. and Drechsler, R. (2019) RevSCA: Using Reverse Engineering to Bring Light into Backward Rewriting for Big and Dirty Multipliers. Proceedings of the 56th Annual Design Automation Conference 2019, Las Vegas, 2-6 June 2019, 1-6. [Google Scholar] [CrossRef] 
[13] Kaufmann, D., Biere, A. and Kauers, M. (2019) Verifying Large Multipliers by Combining SAT and Computer Algebra. 2019 Formal Methods in Computer Aided Design (FMCAD), San Jose, 22-25 October 2019, 28-36 [Google Scholar] [CrossRef] 
[14] Cox, D., Little, J. and O’Shea, D. (2015) Ideals, Varieties, and Algorithms. 4th Edition, Springer-Verlag.
[15] Becker, T., Weispfenning, V. and Kredel, H. (1993) Gröbner Bases, volume141 of Graduate Texts in Mathematics. Springer. [Google Scholar] [CrossRef] 
[16] Sayed-Ahmed, A., Groβe, D., Kühne, U., Soeken, M. and Drechsler, R. (2016) Formal Verification of integer Multipliersby Combining Gröbner basis with Logic Reduction. DATE 2016: 2016 Design, Automation & Test in Europe Conference & Exhibition, Dresden, 14-18 March 2016, 1048-1053. [Google Scholar] [CrossRef] 
[17] Biere, A. (2017) The AIGER And-Inverter Graph (AIG) Format, 20071012. Institute for Formal Models and Verification.
[18] Kernighan, B.W. and Ritchie, D.M. (1988) The C Programming Language. 2nd Edition, Prentice Hall.
[19] Niemetz, A., Preiner, M. and Biere, A. (2015) Boolector 2.0 System Description. Journal on Satisfiability, Boolean Modeling and Computation, 9, 53-58 [Google Scholar] [CrossRef] 

为你推荐