基于指针数组的Gr?bner基方法的优化
Optimization of Gr?bner Basis Method Based on Pointer Array
摘要: 门级整数乘法器电路的验证是形式化验证领域内的一个难题，目前最有效的方法是Grӧbner基方法。在基于此方法的验证过程中，多项式的表示对内存的使用情况有很大的影响。在验证工具Teluma中，多项式表示为单项式的链表。由于链表结点需要同时存储数据元素本身的信息和一个指示其直接后继的信息，这会占用较大的内存空间。针对这一问题，本文对多项式的数据结构进行了优化，采用了动态数组存储单项式，指针数组表示多项式的方法。实验结果表明，该优化方法减少了验证过程中内存的使用。
Abstract: The verification of gate-level integer multiplier circuit is a difficult problem in the field of formal verification, and the most effective method is Grӧbner basis method. In the verification process based on this method, the representation of the polynomial has a great influence on the amount of memory used. In the verification tool Teluma, polynomials are represented as linked list of mono-mials. Because linked list nodes need to store both information about the data element itself and a message indicating its immediate successor, this takes up a large amount of memory space. To solve this problem, this paper optimizes the data structure of polynomials. Dynamic array is used to store monomials and pointer array is to represent polynomials. The experimental results show that the optimization method can reduce memory usage in the verification process.
文章引用：齐爽, 冯天烁, 史美琦, 江建国. 基于指针数组的Gr?bner基方法的优化[J]. 计算机科学与应用, 2023, 13(7): 1485-1491. https://doi.org/10.12677/CSA.2023.137147

参考文献

[1] 闫硕. 基于多项式符号代数的电路形式验证[D]: [硕士学位论文]. 北京: 北京交通大学, 2011.
[2] Biere, A. (2016) Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. Proceedings of SAT Competition 2016—Solver and Benchmark Descriptions, Vol. B-2016-1, 65-66.
[3] Bryant, R.E. and Chen, Y. (2001) Verification of Arithmetic Circuits Using Binary Moment Diagrams. International Journal on Software Tools for Tech-nology Transfer, 3, 137-155. [Google Scholar] [CrossRef] 
[4] Temel, M., Slobodova, A. and Hunt, W.A. (2020) Automated and Scalable Verification of Integer Multipliers. Computer Aided Verification, Los Angeles, 21-24 July 2020, 485-507. [Google Scholar] [CrossRef] 
[5] Ciesielski, M.J., Su, T., Yasin, A. and Yu, C. (2020) 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. [Google Scholar] [CrossRef] 
[6] Kaufmann, D. (2022) Formal Verification of Multiplier Circuits Using Computer Algebra. IT—Information Technology, 64, 285-291. [Google Scholar] [CrossRef] 
[7] Kaufmann, D., Biere, A. and Kauers, M. (2019) Verifying Large Multi-pliers by Combining SAT and Computer Algebra. 2019 Formal Methods in Computer Aided Design (FMCAD), San Jo-se, 22-25 October 2019, 28-36. [Google Scholar] [CrossRef] 
[8] Sayed-Ahmed, A., Große, D., Kühne, U., Soeken, M. and Drechsler, R. (2016) Formal Verification of Integer Multipliers by Combining Gröbner Basis with Logic Reduction. 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE), Dresden, 14-18 March 2016, 1048-1053. [Google Scholar] [CrossRef] 
[9] Ritirc, D., Biere, A. and Kauers, M. (2017) Column-Wise Veri-fication of Multipliers Using Computer Algebra. 2017 Formal Methods in Computer Aided Design (FMCAD), Vienna, 2-6 October 2017, 23-30. [Google Scholar] [CrossRef] 
[10] Ritirc, D., Biere, A. and Kauers, M. (2018) Improving and Ex-tending the Algebraic Approach for Verifying Gate-Level Multipliers. 2018 Design, Automation & Test in Europe Con-ference & Exhibition (DATE), Dresden, 19-23 March 2018, 1556-1561. [Google Scholar] [CrossRef] 
[11] Kaufmann, D., Beame, P., Biere, A. and Nordström, J. (2022) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE), Antwerp, 14-23 March 2022, 1431-1436. [Google Scholar] [CrossRef] 
[12] 陈玉福, 张智勇. 计算机代数[M]. 北京: 科学出版社, 2020.
[13] Kaufmann, D. and Biere, A. (2021) AMulet 2.0 for Verifying Multiplier Circuits. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2021), Luxembourg City, 27 March-1 April 2021, 357-364. [Google Scholar] [CrossRef] 
[14] Kaufmann, D. and Biere, A. (2023) Improving AMulet2 for Verifying Multiplier Circuits Using SAT Solving and Computer Algebra. International Journal on Software Tools for Technology Transfer, 25, 133-144. [Google Scholar] [CrossRef] 
[15] Homma, N., Watanabe, Y., Aoki, T. and Higuchi, T. (2006) Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences, E89-A, 3500-3509. [Google Scholar] [CrossRef]