基于指针操作的乘法器验证程序优化

Optimization of Multiplication Circuit Verification Program Based on Pointer Operations

摘要: 乘法器电路验证是算术电路验证领域内的一个重大难题。Gröbner基方法是其中目前最为有效的验证方法之一。基于此方法开发的Amulet程序通过减少中间变量数量提高了验证效率，但是对于大型乘法器，验证速度慢的问题仍存在。本文对Amulet的关键算法进行了进一步优化，通过指针操作对函数进行重写，缩短了验证的时间，并根据实验数据体现了其在大型乘法器验证中的应用优势，为形式化验证技术的未来研究提供了参考。

Abstract: The verification of multiplier circuits is a significant challenge in the field of arithmetic circuit verification. The Gröbner basis method is currently one of the most effective verification methods available. The Amulet program, developed based on this method, improves verification efficiency by reducing the number of intermediate variables. However, for large multipliers, the verification speed remains an issue. This paper further optimizes the key algorithms of Amulet, by rewriting functions through pointer operations, reduces verification time. Experimental results demonstrate its advantages in the verification of large multipliers. It provides a reference for future research in formal verification techniques.

1. 引言

数字电路执行逻辑运算，因此成为计算机和数字系统的核心部分。特别是执行特定算术运算的算术电路，如加法器和乘法器电路，它们是处理器的关键组件。因此，保证这些电路的正确性至关重要，以避免类似于1994年奔腾FDIV错误的问题再次出现[1]。尤其是乘法器电路的正确性验证，至今仍充满挑战。

迄今为止，验证乘法器的方法多种多样。最初发现奔腾错误的方法依赖于二叉判定图[2]，这需要对乘法器的内部结构有所了解[3] [4]。另一种常见的方法是将问题建模为可满足性(SAT)问题，并将电路转换为合取范式(CNF)。此类方法在2016年的SAT竞赛中得到了大量应用[5]。然而，验证乘法器的CNF公式需要指数级的消解证明[6]，导致CDCLSAT求解器的运行时间呈指数增长。在此基础上，结合定理证明器如ACL2 [7]的方法也被用于证明工业级乘法器的正确性[8]，但这通常不是完全自动化的，并且需要专业知识。

目前，对于平面化乘法器的自动验证中最有效的方法是应用计算机代数，将电路的每一个门及其规范用多项式表示，并按其拓扑结构排序成Gröbner基[9]。通过对规范使用电路的Gröbner基进行约简，可以验证乘法器的正确性；如果约简结果为零，则乘法器被认为是正确的。然而，传统的代数方法面临着约简的中间变量数量急剧膨胀的问题，为解决这一问题，近年来开发了多种预处理技术和约化方法[10]-[12]。

Kaufmann团队针对Gröbner基方法进行了创新性改进，并开发了一款基于C语言的程序——Amulet [13]。该程序在Linux中运行，通过对乘法器的重写、替换和切片操作，有效地减少了在约简过程中生成的中间变量数量，从而提高了形式化验证的效率。尽管Amulet已显示出显著的性能提升，但程序本身的优化潜力仍然存在。

本文对Amulet的关键算法进行了深入改进，通过指针操作对其进行优化，进一步提升了验证效率，扩大了其在大型乘法器验证中的应用优势。本研究的成果不仅加深了我们对形式化验证技术的理解，也为未来在该领域的研究提供了参考。

2. Gröbner基法

2.1. Gröbner基理论

本节内容仅介绍Gröbner基法应用于电路验证中的预备知识，想要了解更加系统的内容请查阅[14]。

假设$k$ 是一个数域，$k\left[x_1,\cdots ,x_n\right]$ 是数域$k$ 上以$x_1,\cdots ,x_n$ 为变量的$n$ 元多项式环。在其中的单项式可以定义一定的序关系，得益于此每个多项式能够定义首项，记为$lm$ 。同时根据首项，对多项式进行排序，以保证除法运算中余式的唯一性。

定义2.1

设$I$ 是$k\left[x_1,\cdots ,x_n\right]$ 的一个非空子集，且：

1) $0\in I$ ；

2) 对任意的多项式$f,g\in I$ ，都有$af+bg\in I$ ，其中$a,b\in k\left[x_1,\cdots ,x_n\right]$ ；

则称I 是一个多项式理想。

定义2.2

设多项式$f_1,\cdots f_s\in k\left[x_1,\cdots ,x_n\right]$ ，若理想$I=\langle f_1,\cdots ,f_s\rangle =\left\{{\displaystyle \sum _{i=1}^s{h}_i{f}_i|h_i\in k\left[x_1,\cdots ,x_n\right]}\right\}$ ，则称$\left\{f_1,\cdots ,f_s\right\}$ 是$I$ 的一组基。

一个理想可以有很多组基。在定义一定序关系后，我们可以根据基中元素首项之间的关系找出一种特殊的理想基。

定义2.3

对于数域$ℝ$ 上的多项式环，理想$I\left(C\right)$ 的一个基$P$ 若满足$\forall q\in I,\exists p\in P:lm\left(p\right)|lm\left(q\right)$ ，则称$P$ 为$I$ 的一个D-Gröbner基。

利用D-Gröbner基的某种良好性质，我们可以解决理想成员问题，即给定$y\in k\left[x_1,\cdots ,x_n\right]$ ，$I=\langle f_1,\cdots ,f_s\rangle$ ，判断$y$ 是否属于$I$ 。具体方法将在稍后进行介绍。

定义2.4

对于每个布尔值变量$x\in \left\{x_1,\cdots ,x_n\right\}$ ，$x\left(1-x\right)=0$ 表示其布尔值约束；对于布尔值变量集$Y\subseteq \left\{x_1,\cdots ,x_n\right\}$ ，记$B\left(Y\right)=\left\{y\left(y-1\right)=0|y\in Y\right\}$ 为$Y$ 的布尔值约束集，其中$B\left(Y\right)\subseteq ℝ\left[x_1,\cdots ,x_n\right]$ 。

定义2.5

$G\left(C\right)\subseteq ℝ\left[x_1,\cdots ,x_n\right]$ 表示电路$C$ 中所有门多项式集。设$P\subseteq ℝ\left[x_1,\cdots ,x_n\right]$ 。如果对于某个规定的序关系，$P$ 的所有首项仅由指数为1的单个变量组成并且是唯一的，且对于所有$p\in P$ 满足$lc\left(p\right)\in {ℝ}^{\times }$ ，那么我们说$P$ 具有唯一的单项首项，记作UMLT。令$X_0\left(P\right)\subseteq X$ 为$P$ 中不为首项的所有变量的集合，并记为

$B_0\left(P\right)=B\left(X_0\left(P\right)\right)$ 。

定理2.1

如果$C$ 是无环电路，$l\in \mathbb{N}$ 。那么集合$G\left(C\right)\cup B_0\left(C\right)\cup \left\{l\right\}$ 是理想$I\left(C\right)+\langle l\rangle \subseteq \mathbb{Z}\left[x_1,\cdots ,x_n\right]$ 的一个D-Gröbner基。

定理2.2 (约简算法)

给定$p,q,r$ 属于$ℝ\left[x_1,\cdots ,x_n\right]$ 。如果存在q中的单项式$m^{\prime }$ ，满足$m^{\prime }=m\cdot lm\left(p\right)$ 并且$r=q-mp$ ，那么我们称$q$ 关于$p$ 被约简为$r$ [15]。使用此算法对D-Gröbner基进行运算可以解决理想成员问题：

定理2.3

设$G$ 是理想$I$ 的一组D-Gröbner基，多项式$q\in ℝ\left[x_1,\cdots ,x_n\right]$ ；$q$ 被$G$ 约简的余式$r$ 满足$q-r\in G$ ；$q\in I$ 当且仅当$r=0$

2.2. 电路代数模型

先前的Gröbner基法想要应用于电路，需要对电路建立代数模型，将电路中的逻辑门结构抽象成为门多项式。一个输入、输出位数均为$2n$ 的无环电路，设其输入变量为$a_1,\cdots ,a_n,b_1,\cdots ,b_n$ ，输出变量为$s_0,\cdots ,s_{2n-1}$ ，并设其内部逻辑门变量为$g_0,\cdots ,g_{i-1}$ [16]，则可以定义多项式环$ℝ\left[a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1},g_1,\cdots ,g_k,s_0,\cdots ,s_{2n-1}\right]$ ，定义布尔值变量$a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1},g_1,\cdots ,g_k,s_0,\cdots ,s_{2n-1}$

并根据逆拓扑序定义字典序关系$\succ$ ：

$s_{2n-1}\succ \cdots \succ s_0\succ b_n\succ \cdots \succ b_0\succ a_n\succ \cdots a_0$

因此电路的逻辑门中变量的关系可以通过多项式形式表达：

$\begin{array}{c}\begin{array}{ccc}u=\neg v& \Rightarrow & 0=-u+1-v\\ u=v\wedge w& \Rightarrow & 0=-u+vw\\ u=v\vee w& \Rightarrow & 0=-u+v+w-vw\end{array}\\ \begin{array}{ccc}u=v\oplus w& \Rightarrow & 0=-u+v+w-2vw\end{array}\end{array}$

定义2.6

设$C$ 是一个电路，$p\in ℝ\left[x_1,\cdots ,x_n\right]$ 是多项式。将$C$ 中所有输入变量、逻辑门变量和输出变量的任一组赋值代入到$p$ 中，若结果为0，则称$p$ 是电路$C$ 的一个多项式电路约束，记为$PCC$ ，电路$C$ 是无环电路，那么$C$ 的$PCC$ 实际上就是$G\left(C\right)\cup B_0\left(C\right)$ ，根据定理2.1的内容，电路$C$ 中所有$PCC$ 构成的集合就构成电路的D-Gröbner基，记为$I\left(C\right)$ 。

定义2.7

设$C$ 是一个电路，如果多项式

${\displaystyle \sum _{i=0}^{2n-1}{2}^i{s}_i}-\left({\displaystyle \sum _{i=0}^{n-1}{2}^i{a}_i}\right)\left({\displaystyle \sum _{i=0}^{n-1}{2}^i{b}_i}\right)$

是一个$PCC$ ，则称电路$C$ 是一个乘法器电路，称该多项式为$C$ 的规范多项式$L$ 。

定理2.4

无环电路$C$ 满足规范$L$ 当且仅当$L\in I\left(C\right)$ 。

总结上面的定义定理，我们可以得到如下结论：

验证乘法器电路$C$ ，只需使用定理2.3来验证$L$ 是否属于理想$I\left(C\right)$ 。当且仅当$L$ 属于$I\left(C\right)$ ，乘法器电路$C$ 正确。为此我们利用定理2.3对电路规范进行约简，查看最终结果$r$ 的取值，进而对电路正确性做出判断。

3. 电路验证程序与优化

3.1. 电路验证程序Amulet

在最近的研究中，Linz大学的Kaufman团队研发的Amulet验证程序为电路验证领域做出了重大贡献[13]。Amulet是一个先进的验证工具，它利用C语言编写，并在Linux环境下运行。该工具的开发集成了乘法器的识别、重写、切片、约简和验证等多个关键步骤，提供了一个全面的解决方案来处理电路验证难题。同时，Amulet还能够根据用户的需求，生成相应的证书证明，以支撑验证结果的透明度和可靠性。

本研究旨在基于Amulet验证器的现有架构和功能进行进一步的优化，目标是加速大型乘法器的验证过程，从而显著提高整体的验证效率。我的研究初步分析了使用Amulet进行电路验证时所产生的日志文件，发现在整个验证过程中，多项式的约简操作占据了大部分的计算时间。这一发现指出了一个有待提升的性能瓶颈，即多项式运算函数的效率直接影响到验证器的运行速度。

针对上述问题，本文的核心工作集中于探讨和改进Amulet中的多项式运算函数。通过对这些核心函数进行优化，减少多项式约简步骤所需的时间，从而在不牺牲验证准确性的前提下，提升整个验证流程的效率。

验证器运行过程中，电路以aig (And-InverterGraph)格式输入[17]，并在验证器中被识别。

电路中的变量均以结构体Var形式储存变量名称，变量序，所属链表等形式的信息。电路中通过访问Var指针对变量进行访问赋值。

电路中门多项式的项利用结构体指针Term*表示，其中主要包含：变量的结构体指针Var*variable，储存对应变量的地址；指向相连接的下一个链表的指针Term* rest，利用链表的特性，变量联系起来作为项的整体(见图1)。

单项式Monomial*，多项式Polynomial*的数据结构与项的结构大概一致，都使用了单向链表相互进行联系，方便进行访问和赋值。

Figure 1. Linked list structure diagram

图1. 链表结构示意图

代码1：单向链表的储存逻辑

struct listnode { int data; char* name;//储存的数据 listnode* rest;//指向下一个节点地址的结构体指针 };

切片保存为结构体Slice形式，它是程序通过识别输出变量，标记输入变量父节点，分割输入锥后生成的。其中保存了切片的变量集合，门多项式集合，以便稍后的按列约简操作。程序根据输出的输入锥定义切片，并根据从电路输入读取的level对切片中的变量进行排序。这确保了变量是拓扑排序的，并且相应的多项式具有UMLT，从而形成D-Gröbner基。

在读取，切片，重写电路后，函数init_slices()对各个切片所有变量进行排序，将参与切片的变量存入变量集，并根据变量间的关系生成门多项式存入多项式集中。

根据D-reduction算法，验证电路需要用每个门多项式对电路规范进行约简，函数reducing_non_inc()实现了这一功能，它遍历所有生成的切片，并利用循环，用切片中的多项式集对电路规范约简。其中调用了函数generate_non_inc_spec()根据稍前读取的电路信息生成电路规范spec；使用变量tmp把约简的结果储存起来，每次循环后更新spec，在下一个循环中用新的spec进行约简；调用函数reduce_by_one_poly()进行两个多项式的约简运算；在最后判断spec是否被约简为0，并输出对应信息：

算法：约简过程

输入：指向Polynomial结构的指针p1, 指向Polynomial结构的指针p2 输出：指向Polynomial结构的指针 计算多项式p1和p2的首项之间的除法，结果存储于negfactor； 将negfactor取反； 将negfactor与多项式p2相乘，结果存储于mult； 将多项式p1与多项式mult相加，结果存储于rem； 返回多项式rem；

程序中约简算法的核心是函数reduce_by_one_poly()，它遵循约简原则对两个多项式在既定的序关系下进行约简。它首先调用函数divide_lm()，用除式p2的首项对被除式p1作用除法，获得商negfactor，最后调用多项式乘法函数multiply_poly()和加法函数add_poly()返回余式rem=p1-p2*negfactor。函数add_poly()将符合条件的单项式放入堆栈中，利用栈操作构建新的多项式，算法如下：

算法：函数add_poly的算法

输入：指向Polynomial结构的指针p1, 指向Polynomial结构的指针p2 输出：指向Polynomial结构的指针 当p1和p2都非空时循环： a. 如果p1的首项大于p2的首项： 将p1的首项复制入堆栈； 将p1更新为下一个节点； b. 如果p1的首项小于p2的首项： 将p2的首项复制入堆栈； 将p2更新为下一个节点； c. 否则： 复制p1的首项到m； 将p1，p2的首项系数相加并赋值给m的系数； 如果m的系数为0，则释放m； 否则将m放入堆栈； 将p1和p2分别更新为各自的下一个节点； 当p1非空时循环： a. 将p1的首项复制并按排序规则压入堆栈； b. 将p1更新为下一个节点； 当p2非空时循环： a. 将p2的首项复制并按排序规则压入堆栈； b. 将p2更新为下一个节点； 从堆栈构建新的多项式p； 返回p；

函数contianed()被函数divide_lm()调用作为条件判断，其功能是判断项p2是否包含p1全部变量；它使用了循环嵌套，对于每个p1中的元素，遍历p2，检查是否在其中；具体算法如下：

算法：函数contained的算法

输入：指向Term结构的指针m1, 指向Term结构的指针m2 输出：整型数字 初始化变量found为0； 将指针tmp1初始化为m1； 当tmp1不为空时循环： a. 将指针tmp2初始化为m2； b. 当tmp2不为空时循环： 如果tmp1等于tmp2，将found设为1并退出循环； 否则，将tmp2更新为下一个节点； c. 如果found等于0，则返回0； d. 将found重置为0； e. 将tmp1更新为下一个节点； 返回1；

3.2. 分析与优化

对add_poly函数的原始实现进行分析，我们发现其采用了一种基于全局栈的方法来处理多项式加法操作。在此方法中，多项式中的每个单项式首先被复制，随后推入一个全局栈中。待所有相关操作完成之后，栈中的元素被逐一取出，用以构建出最终的多项式。虽然这种方法在某些情况下比较有效，但它也带来了几个潜在的问题和挑战。

首先，该函数强烈依赖于全局栈的状态，这种依赖，尤其是在复杂的系统环境中，经常会导致数据竞争和同步问题，增加了软件的不稳定性。

其次，该函数中每次的调用都需要将单项式推入栈中，然后再将它们从栈中取出以构建最终的多项式。这种做法引入了栈操作的中间步骤，增加了执行过程的时间开销，也提高了处理每个单项式所需的计算资源需求。这种额外的时间和资源开销可能成为性能瓶颈，影响整体应用的响应速度和效率。

最后，使用栈作为中间数据结构增加了代码的复杂性，增加了程序的理解、维护和扩展的难度。对于维护者和开发者而言，去理解栈的操作逻辑及其与多项式处理之间的关联变得更加不易，这不仅降低了代码的可读性，也增加了开发和维护的工作量。

在分析contained()函数时，我们发现了一个效率问题，即该函数依赖于嵌套循环。为了确定一个多项式的所有项是否完全包含于另一个多项式中，该函数逐一比较第一个多项式(记为m1)中的每个项与第二个多项式(记为m2)中的所有项。这种方法在m1和m2都具有大量项时会显著增加计算的时间复杂度，尤其是每个项都必须与另一个多项式中的每个项进行比较的场景下。这种比较方法可能引发性能瓶颈，影响验证过程的效率。

此外，found变量的使用进一步增加了代码的复杂性。该变量的目的是标记在遍历m2时是否找到了与m1中当前项匹配的项。然而，found需要在每次外层循环迭代后重置，使得函数的逻辑变得难以理解，从而降低了代码的可读性和可维护性。这种管理机制不仅对于开发者来说增加了理解和维护代码的难度，也为优化和功能扩展设置了障碍。

在处理复杂且数量庞大的多项式时，上述函数逻辑存在明显的局限性，影响了程序的执行效率。本文提出了一种新的优化方案，利用C语言中指针的特性，通过指针操作优化多项式处理函数。

指针是C语言中一种强大的工具，允许程序直接访问内存地址，从而操作存储在相关位置的数据。通过指针，开发者可以实现更为高效和灵活的内存管理。尤其是在构建数据结构、实现函数参数的传递和操作等方面，指针操作展现出了无可比拟的优势：不仅提升了程序的执行效率，也极大地增强了代码的灵活性和复用性。

C语言的指针在软件开发和系统编程中占有重要地位。指针直接操作内存，可以创建更为高效的数据处理逻辑，如链表、树等动态数据结构的实现，这些结构在处理大量数据和实现复杂算法时表现出极高的效率和灵活性。此外，指针的使用减少了对额外内存的需求，直接操作内存地址以传递复杂的数据结构，避免了数据的不必要复制，进而降低了程序的内存消耗同时提升了性能[18]。

我们针对add_poly函数进行优化，对原始函数的实现逻辑进行了重新设计，并提出了一个新的实现方案，该方案通过指针操作，利用链表的结构特点，直接构建新的多项式链表来替代原始版本的栈操作进行加法，从而避免了对全局栈的依赖。

算法：优化函数add_poly

输入：指向Polynomial结构的指针p1,指向Polynomial结构的指针p2 输出：指向Polynomial结构的指针 1. 初始化指向Polynomial的指针result为空； 2. 创建一个指针ptr，指向result的地址； 3. 当p1和p2都非空时循环： a. 比较p1和p2当前首项的大小； b. 如果p1的首项较大： 在ptr指向的地址创建一个新Polynomial节点； 复制p1的首项到新节点的首项； 将p1更新为下一节点； c. 如果p1的首项较小： 在ptr的地址创建一个新的Polynomial节点； 复制p2的首项到新节点的首项； 将p2更新为下一节点； d. 如果p1和p2的首项相同： 复制p1的首项到临时单项式m； 将p1和p2的首项系数相加;如果不为0，则在ptr地址创建一个新的Polynomial节点，并将m设为该节点的首项； 如果结果为0，则释放m； 更新p1和p2为各自的下一节点； e. 如果ptr非空，则更新ptr为该节点的下一个地址； 4. 如果p1非空，则将p1剩余的项添加到结果多项式中； 5. 如果p2非空，则将p2剩余的项添加到结果多项式中； 6. 返回指向结果多项式的指针result；

重构后的add_poly函数彻底消除了全局变量的使用，显著提高了函数的重入性和线程安全性。在并发执行环境下，该函数展现出更为稳定的性能，减少了数据竞争的风险，保证了算法在高并发场景下的可靠性。

新的实现减少了不必要的中间步骤，直接在遍历输入多项式的过程中构建结果多项式，从而提升了整体操作的效率。这种效率的提升突出体现在处理包含大量项的复杂多项式时，能够加速如大型电路验证这样高复杂度的过程。

优化后的方案简化了加法逻辑，使得代码更加直观易懂，提高了程序的可读性和可维护性。此外，减少对全局状态的依赖不仅提升了代码的模块化程度，也为功能扩展和优化提供了便利。这种设计思路符合现代软件工程的实践逻辑。

算法：优化函数contained

输入：指向Term结构的指针m1, 指向Term结构的指针m2 输出：整型数字 初始化指针tmp1为m1； 初始化指针tmp2为m2； 当tmp1和tmp2都非空时循环： a. 如果tmp2当前变量的级别小于tmp1当前变量的级别，则 更新tmp2为下一个节点； b. 如果tmp2当前变量的级别等于tmp1当前变量的级别，则 更新tmp1为下一个节点； 更新tmp2为下一个节点； c. 如果tmp2当前变量的级别大于tmp1当前变量的级别，则 返回0； 如果tmp1仍然非空，则 a. 返回0； 返回1；

由于在init_slices()函数调用期间，每个变量的level值被更新为独一无二的值，所以允许我们使用这些level值作为索引进行直接比较，来确定变量的等价性。根据这个前提，我们使用双指针方法代替原来的循环嵌套优化函数contained：通过双指针同时遍历参数项，比较变量level值进行判断。修改后的contained函数的判断逻辑更为高效、更为清晰。与原始基于嵌套循环的实现相比，新方法能够以线性时间而非二次的时间复杂度完成相同的任务。

新函数通过比较变量的level值，更加充分地结合程序中的变量构造，允许函数在更抽象的层次上进行比较，提高了运用过程的灵活性，也为程序的功能扩展提供基础。如果有支持更复杂的多项式结构或者引入新的比较逻辑的需求，优化后的函数可以更容易地适应这些变化。同时，优化的函数移除found变量简化状态管理，避免了原有函数中的复杂逻辑，使得代码更加直观和易于维护。

4. 对比实验

实验对比分析了原始的y验证程序与其改进版本的性能。由于对任何结构的乘法器，程序在进行约简操作时采用的约简算法均相同，因此，本研究选择以btor乘法器和Kojevnikov乘法器作为案例来进行分析对比。二者的基准测试由Boolector工具生成，并以AIG格式进行存储[19]。

本文的实验分析将以表格形式阐述两种程序在处理乘法器时的效率与效果对比，以评估改进后的验证程序在实际应用中的性能表现。

本研究在配备AMDRyzen 9 5900HX处理器(主频为3293.816 MHz)和8 GB内存的Ubuntu 23.04操作系统环境下的虚拟机中进行了实验，通过图表对实验结果进行对比展示，以便评估优化后的验证程序对乘法器电路验证的性能提升。具体结果如表1。

根据以下数据我们发现，与原始程序相比，改进后的程序在执行效率上有所提升。特别是在处理大规模乘法器电路时，这种性能优势更为显著。

优化后的程序提高了验证程序处理复杂乘法器电路的能力，展示了其在大规模数字电路验证领域的潜在应用价值。因此，我们认为本文的优化不仅改善了程序的总体性能，而且对于那些涉及大量计算和数据处理的高复杂度电路验证任务，尤其有利。

Table 1. Multiplier experiment data

表1. 乘法器实验数据

乘法器	位数	原程序(秒)	优化程序(秒)
btor	128	6.18	6.09
btor	256	58.39	58.26
btor	512	616.39	575.57
Kojevnikov	128	5.67	4.91
Kojevnikov	256	46.84	44.96
Kojevnikov	512	454.42	443.18

5. 结语

本文通过对Amulet多项式算法的优化，特别是利用指针操作快捷清晰的优点对函数进行重写，将原算法中通过栈操作构建多项式的步骤转换为指针操作，成功缩短了验证时间，并通过实验数据验证了其在大型乘法器验证中的实际优势。

就目前而言，优化的效率提升在btor乘法器上更为明显，其他更为复杂的乘法器验证还有很大优化空间。在未来工作中，有希望通过重构多项式结构的形式，重写程序中的结构体，对程序中的多项式运算算法进行进一步优化。