乘法器电路是复杂芯片系统和集成电路中必不可少的组成部分,它在图像处理、语言加密等数字信号领域中占有重要地位。乘法器的验证问题是超大规模集成电路设计领域内的一大难题。传统的动态仿真技术和形式化验证是乘法器电路验证的两种重要方法。动态仿真技术的优势在于操作简单,原理通俗易懂,但需要选择合理的覆盖率对电路进行功能测试,无法满足大型乘法器电路的验证需求。形式化验证作为一种新型且主流的验证方式,将电路验证问题转化为数学问题,利用理论性的概念、方法和工具来验证电路的正确性。目前,最受关注且最为有效的形式化验证方法是Gr?bner基方法。逐位验证和加法器重写是Gr?bner基方法中的两项重要突破。逐位验证将乘法器电路按和位输出进行切片,并对每一个切片分别定义切片Gr?bner基,利用理想成员算法分别验证每一个切片的正确性,将整个验证问题分解为若干个易于解决的子问题,提高验证效率。加法器重写是Gr?bner基方法中的一个关键步骤,能够缩小电路Gr?bner基的规模,极大地加快规范多项式的约化进程。然而,目前这两种优化策略还存在着明显的不足。若将逐位验证与加法器重写相结合,那么加法器重写的时间主要花费在搜索加法器的过程中,通过穷举遍历电路中门变量的方式来搜索加法器是相当低效的;若单独使用逐位验证,那么验证的时间主要花费在进位变量识别算法中,受到遍历序和穷举遍历的影响,该算法的实现存在大量的冗余。本文在逐位验证和加法器重写的基础上,提出如下两点优化:第一,提出一种在电路中搜索全部加法器的快速算法,该算法使用动态数组存储搜索加法器所需的门变量,并按逆拓扑序来搜索加法器,极大地减少冗余遍历。第二,结合乘法器电路的结构性知识,根据电路AIG图中变量的父结点个数对进位变量识别算法进行优化。两种优化的实验结果表明,结合动态数组的加法器重写快速算法和优化后的进位变量识别算法都能够通过减少冗余遍历来提高乘法器电路的验证效率。