|
|
基于指针数组的Gr?bner基方法的优化
|
Abstract:
门级整数乘法器电路的验证是形式化验证领域内的一个难题，目前最有效的方法是Gr？bner基方法。在基于此方法的验证过程中，多项式的表示对内存的使用情况有很大的影响。在验证工具Teluma中，多项式表示为单项式的链表。由于链表结点需要同时存储数据元素本身的信息和一个指示其直接后继的信息，这会占用较大的内存空间。针对这一问题，本文对多项式的数据结构进行了优化，采用了动态数组存储单项式，指针数组表示多项式的方法。实验结果表明，该优化方法减少了验证过程中内存的使用。
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.
| [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. https://doi.org/10.1007/s100090100037 |
| [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. https://doi.org/10.1007/978-3-030-53288-8_23 |
| [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. https://doi.org/10.1109/TCAD.2019.2912944 |
| [6] | Kaufmann, D. (2022) Formal Verification of Multiplier Circuits Using Computer Algebra. IT—Information Technology, 64, 285-291. https://doi.org/10.1515/itit-2022-0039 |
| [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.
https://doi.org/10.23919/FMCAD.2019.8894250 |
| [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. https://doi.org/10.3850/9783981537079_0248 |
| [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.
https://doi.org/10.23919/fmcad.2017.8102237 |
| [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. https://doi.org/10.23919/DATE.2018.8342263 |
| [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. https://doi.org/10.23919/DATE54114.2022.9774587 |
| [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.
https://doi.org/10.1007/978-3-030-72013-1_19 |
| [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.
https://doi.org/10.1007/s10009-022-00688-6 |
| [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. https://doi.org/10.1093/ietfec/e89-a.12.3500 |
