GrO^¨bner基法验证乘法器的设计与实现

Design and Implementation of GrO^¨bner Basis Verification Multiplier

摘要: 当今形式化验证工具在大规模集成电路的设计过程中起着非常重要的作用。最有效的方法是以Gröbner基方法为基本原理，将乘法器电路建模为一组伪布尔多项式，通过Gröbner基来既约由多项式表示的字级规范。本文将基于Gröbner基方法，使用C++语言重新实现验证工具，将整个代码分成多个模块的形式，并利用容器类对变量进行分类存储。实验结果表明：C++语言设计的验证工具不仅可以实现成功，而且也为之后的研究提供了有利的验证工具。

Abstract: 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.