基于GrO¨bner基方法的乘法器等价性验证
Equivalence Verification of Multipliers Based on GrO¨bner Basis Method
摘要: 乘法器的等价性验证目前仍是大规模算术集成电路设计领域内的一大难题。本文利用逻辑门与多项式之间的对应关系，构建了乘法器的代数模型，将乘法器等价性验证问题转化成理想成员判定问题，然后再用计算机代数系统中的Gröbner基方法进行求解。提出了一种对乘法器结构进行切片后再采用增量式验证的新方法。在Linux平台上的计算机代数系统Mathematica上所做的实验结果也表明了该方法的有效性。
Abstract: The equivalence verification of multipliers is still a difficult problem in the field of LSI design. In this paper, the algebraic model of multipliers is constructed by using the corresponding relationship between logic gates and polynomials. The problem of equivalence verification of multipliers is transformed into the problem of determining ideal members. Then, the problem is solved by the Gröbner basis method in computer algebra system. This paper presents a new method of incremental verification after slicing the multiplier structure. The experimental results on Mathematica, a computer algebra system on Linux platform, also show the effectiveness of the method.
文章引用：张璇思, 刘佳姝, 江建国. 基于GrO¨bner基方法的乘法器等价性验证[J]. 应用数学进展, 2021, 10(1): 343-350. https://doi.org/10.12677/AAM.2021.101039

参考文献

[1] 包日辉. SoC设计平台中若干IP模块的设计[D]:[硕士学位论文]. 杭州: 杭州电子科技大学, 2019.
[2] Clarke, E.M., Grumberg, O. and Peled, D. (1999) Model Checking. The MIT Press, Cambridge.
[3] 韩俊刚, 杜敏慧. 数字硬件的形式化验证[M]. 北京: 北京大学出版社, 2001.
[4] 静思. 让科学之声以更强的力度震撼神州大地一从“奔腾芯片”的错误引发的联想[J]. 电子展望与决策, 1995(3): 23.
[5] Pruss, T., Kalla, P. and Enescu, F. (2014) Equivalence Verification of Large Galois Field Arithmetic Circuits Using Word- Level Abstraction via Gröbner Bases. Proceedings of the 51st Annual Design Automation Conference, San Francisco, June 2014. 1-6. [Google Scholar] [CrossRef] 
[6] Fan, Q.R., Pan, F. and Duan, X.D. (2011) Using Logic Synthesis and Circuit Reasoning for Equivalence Checking. Advanced Materials Research, 201-203, 836-840. [Google Scholar] [CrossRef] 
[7] Vedhus, H. (2020) Deep Bayesian Neural Networks for Damage Quantification in Miter Gates of Navigation Locks. Structural Health Monitoring, 19, 1391-1420. [Google Scholar] [CrossRef] 
[8] 周宁. 代数化符号模拟验证的应用研究[D]: [博士学位论文]. 北京: 北京交通大学, 2015.
[9] Cox, D., Little, J. and O’Shea, D. (1997) Ideals, Varieties, and Algorithms. Springer-Verlag, New York. [Google Scholar] [CrossRef] 
[10] Huang, G.L. and Zhou, M. (2015) On The Termination of Algorithm for Computing Relative Gröbner Bases. ACM Communications in Computer Algebra, 49, 28. [Google Scholar] [CrossRef] 
[11] 李春红. 基于乘法器的振幅调制实验特性研究[J]. 2020, 33(2): 33-37.
[12] Sayed-Ahmed, A., Große, D., Kühne, U. Soeken, M. and Drechsler, R. (2016) Formal Verification of Integer Multipliers by Combining Gröbner Bases with Logic Reduction. 2016 Design, Automation & Test in Europe Conference & Exhibition, Dresden, 14-18 March 2016, 1048-1053. [Google Scholar] [CrossRef] 
[13] Chen, J. and Chen, Y. (2001) Equivalence Checking of Integer Multipliers. Proceedings of the 2001 Asia and South Pacific Design Automation Conference, Yokohama, 169-174. [Google Scholar] [CrossRef] 
[14] Lv, J., Kalla, P. and Enescu, F. (2013) Efficient Gröbner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32, 1409-1420. [Google Scholar] [CrossRef] 
[15] Ritirc, D., Biere, A. and Kauers, M. (2017) Column-Wise Verification of Multipliers Using Computer Algebra. 2017 Formal Methods in Computer Aided Design, Vienna, 2-6 October 2017, 23-30. [Google Scholar] [CrossRef] 
[16] Ritirc, D., Biere, A. and Kauers, M. (2018) Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers. 2018 Design, Automation & Test in Europe Conference & Exhibition, Dresden, 19-23 March 2018, 1556-1561. [Google Scholar] [CrossRef] 

为你推荐