乘法器电路在数字电路系统中占有重要的地位,但随着乘法器电路的结构越来越复杂,给乘法器电路的验证带来了新的挑战。如果不及时找到其中存在的错误,将导致严重的后果。因此,乘法器电路的验证在现代电路设计中成为至关重要的一环,而模拟仿真和形式化验证方法是验证乘法器电路的两种主要方法。模拟仿真是通过使用数学模型对电子电路的真实行为进行模拟的工程方法,但模拟仿真一直存在较多根本性问题无法有效解决。为解决此类问题,形式化验证方法就应运而生,成为乘法器电路验证的最有效方法之一。近几年来,已经开发出多种乘法器电路的验证方法及优化,但这些验证工具在遍历乘法器电路节点时会产生冗余,既约多项式时会因为代数计算系统Mathematica或Singular的限制导致验证效率缓慢或验证失败,并且没有给出相应的证明证书。本文基于Gr（?）bner基方法利用C++语言实现了一个验证工具,它包含解析器、优化策略、多项式求解器和证明系统四个模块,每个模块可以轻松集成到其他的工作当中。解析器包含对AIG文件的读取,优化策略中利用顺序容器存储每个切片中的节点,减少遍历节点过程中产生的冗余。而项可表示为节点变量的有序链表,单项式由一个系数和一个项组成,通过多项式表示为单项式的有序链表建立多项式库,实现了用多项式求解器代替以往的代数计算系统对规范多项式进行既约,一定程度上解决了代数计算系统中由于变量太多或计算时间过长导致验证失败的问题。实验结果表明,本文的验证工具不仅不会因为变量个数太多而停止运算,而且运算效率提高了几十倍,使其成为了一个强有力的验证工具。为了进一步增强验证工具的可靠性,确保验证过程没有出现偏差,在验证工具中添加了 Nullstellensatz证明系统。该证明系统将生成门约束、辅助因子和规范多项式三个文件,也就是证明证书。如果门约束依次乘辅助因子并相加可以得到规范多项式,就说该验证工具的验证过程是无误的。