|
|
GrO¨bner基法验证乘法器的设计与实现
|
Abstract:
当今形式化验证工具在大规模集成电路的设计过程中起着非常重要的作用。最有效的方法是以Gr？bner基方法为基本原理，将乘法器电路建模为一组伪布尔多项式，通过Gr？bner基来既约由多项式表示的字级规范。本文将基于Gr？bner基方法，使用C++语言重新实现验证工具，将整个代码分成多个模块的形式，并利用容器类对变量进行分类存储。实验结果表明：C++语言设计的验证工具不仅可以实现成功，而且也为之后的研究提供了有利的验证工具。
Today’s formal verification tools play a very important role in the design of large-scale integrated circuits. The most effective method is based on the Gr？bner basis method. The multiplier circuit is modeled as a set of pseudo-Boolean polynomials, and the word-level specification represented by the polynomial is reduced through the Gr？bner basis. This article will re-implement the verification tool based on the Gr？bner base method and use the C++ language, divide the entire code into multiple modules, and use the container class to classify and store the variables. The experimental results show that the verification tool designed by C++ language can not only achieve success, but also provide a favorable verification tool for subsequent research.
| [1] | 杨宗凯. 数字专用集成电路的设计与验证[M]. 北京: 电子工业出版社, 2004. |
| [2] | Seligman, E., Schubert, T. and Kirankumar, M. (2015) Formal Verification: An Essential Toolkit for Modern VLSI Design. Elsevier Science, Amsterdam. |
| [3] | Randal, Y. and Bryant, E. (1995) Verification of Arithmetic Circuits with Binary Moment Diagrams. 32nd Design Automation Conference, San Francisco, 12-16 June 1995, 1-7. |
| [4] | Kaufmann, D., Biere, A. and Kauers, M. (2019) Verifying Large Multipliers by Combining SAT and Computer Algebra. FMCAD 2019: 2019 Formal Methods in Computer Aided Design, San Jose, 22-25 October 2019, 28-36.
https://doi.org/10.23919/FMCAD.2019.8894250 |
| [5] | 游珍, 薛锦云. 基于Isabelle定理证明器算法程序的形式化验证[J]. 计算机工程与科学, 2009, 31(10): 89-93. |
| [6] | Mahzoon, A., Groβe, D. and Drechsler, R. (2018) PolyCleaner: Clean Your Polynomials before Backward Rewriting to Verify Million-Gate Multipliers. Proceedings of the International Conference on Computer-Aided Design, San Diego, 5-8 November 2018, Article No. 129. https://doi.org/10.1145/3240765.3240837 |
| [7] | Mahzoon, A., Groβe, D. and Drechsler, R. (2020) Towards Formal Verification of Optimized and Industrial Multipliers. DATE 2020: 2020 Design, Automation & Test in Europe Conference & Exhibition, Grenoble, 9-13 March 2020, 544- 549. https://doi.org/10.23919/DATE48585.2020.9116485 |
| [8] | Ritirc, D., Biere, A. and Kauers, M. (2017) Column-Wise Verification of Multipliers Using Computer Algebra. FMCAD 2017: 2017 Formal Methods in Computer Aided Design, Vienna, 2-6 October 2017, 23-30.
https://doi.org/10.23919/FMCAD.2017.8102237 |
| [9] | Ritirc, D., Biere, A. and Kauers, M. (2018) Improving and Extending the Algebraic Approach for Verifying Gate-Le- vel Multipliers. Design, Automation & Test in Europe Conference & Exhibition, Dresden, 19-23 March 2018, 1556- 1561. https://doi.org/10.23919/DATE.2018.8342263 |
| [10] | 李雁妮, 陈平, 王献青. C++程序设计语言[M]. 西安: 西安电子科技大学出版社, 2009. |
| [11] | Cox, D., Little, J. and O’Shea, D. (2015) Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry & Commutative Algebra, Springer International Publishing, Switzerland, 307-338.
https://doi.org/10.1007/978-3-319-16721-3 |
| [12] | 陈玉福, 张智勇. 计算机代数[M]. 北京: 科学出版社, 2020. |
| [13] | 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. DATE 2016: 2016 Design, Automation & Test in Europe Conference & Exhibition, Dresden, 14-18 March 2016, 1048-1053. https://doi.org/10.3850/9783981537079_0248 |
| [14] | Biere, A. (2007) The AIGER And-Inverter Graph(AIG) Format Version 20071012. http://fmv.jku.at/aiger |
| [15] | Wolfram Research (1991) Writed, I. Mathematica: A System for Doing Mathematics by Computer. Wolfram Research, Inc., Champaign. |
| [16] | Decker, W., Greuel, G.M., Pfifister, G. and Schonemann, H. (2016) SINGULAR. |
| [17] | Lutz, M., Ascher, D., 陈革. Python语言入门[J]. Internet: 共创软件, 2002(10): 86-86. |
| [18] | 吴建平, 尹霞, 冯晓冬. Java程序设计语言[M]. 北京: 清华大学出版社, 1997. |
