基于队列的树形加法优化认证器

Queue-Based Tree Addition Optimization Authenticator

摘要: 目前验证乘法器电路依然是一个极其重要的问题，形式验证给出系统的正确性，但为了增加形式验证结果的可靠性，我们在验证过后加入了认证过程，以检验其结果的正确性。同时运用Amulet工具生成Nullstellensatz (NSS)证明来提高对自动化推理的信心，并由独立的认证器Nuss-Checker进行检查。本文在认证器生成规范多项式过程中，运用基于队列的树形加法优化该认证器，降低了求和过程中形成多项式的项的数目，提高了认证器的检查效率。

Abstract: At present, the verification of the multiplier circuit is still an extremely important problem. The formal verification gives the correctness of the system, but in order to increase the reliability of the formal verification results, we add the authentication process after the verification to check the correctness of the results. The AMULET tool is also used to generate Nullstellensatz (NSS) proofs to increase confidence in automated reasoning and to be checked by the independent certifier USS Checker. In this paper, the authenticator is optimized by tree addition based on queue, which reduces the number of polynomials and improves the checking efficiency of the authenticator.

1. 引言

基于计算机代数的自动推理技术被广泛的应用于算术电路的形式验证，是门级乘法电路形式化验证的重要组成部分。形式验证的目的是保证系统的正确性，然而为了增加验证过程和实现过程的可靠性，一种常见的技术是生成证明文件，该方法监视整个验证过程并形成证明文件，同时该证明文件可以由独立的认证器进行检查。

形式验证的很多应用可以运用可满足性(SAT)求解，电路被转化为合取范式(CNF)来进行解算，这些结果可以通过产生并检查分辨率证明或子句证明进行验证。而在某些应用中，SAT求解无法应用，例如算数电路的形式验证，验证乘法器的斜接需要指数大小的分辨率证明，即使很小的乘法器，斜接也会产生非常困难的SAT问题 [1] ，这对于复杂的乘法器体系结构来说明显不适用，因此乘法器电路是SAT求解的难点。

目前有效的方法是基于计算机代数，将电路中所有逻辑门以及其规范都用多项式表示，并生成Gröbner基进行计算，但乘法器部分，尤其是复杂的末级加法器部分很难用计算机代数进行验证，如今可以将SAT和计算机代数结合起来，用简单的纹波进位加法器(RCA)来代替生成和传播(GP)加法器 [2] 。在预处理之后，通过重写门多项式来减少指定多项式，直到不能减少为止，再通过检查返回值是否为零来判断乘法器电路是否正确。

除了电路验证，计算机代数与SAT求解相结合也被用于解决复杂的组合问题，例如，找到矩阵乘法的主方法 [3] ，计算色数为5 [4] 的小单位距离图，或解决Williamson猜想 [5] 。这些应用都证明了运用代数证明系统进行验证的必要性。在证明复杂度中，主要使用的有两个代数证明系统，多项式演算(PC)和Nullstellensatz (NSS) [6] ，其中由于PC不适用于实际的证明检查而引入了可以有效检查的实用代数演算(PAC) [7] 。NSS证明捕获的多项式是否可以表示为多项式集合的线性集合，该证明十分简洁，是由输入多项式和相应的协因子多项式序列组成，进而判断生成多项式是否等同于目标多项式，此外NSS证明拥有独立的认证器Nuss-Checker [8] ，对验证结果进行检查。

本文在认证器Nuss-Checker中基于队列通过树形加法方式生成多项式，将NSS证明中两个连续的多项式相加，并运用队列存储其所得和，同时在队列上反复迭代，总是将两个连续的多项式相加，直到只剩下一个多项式为生成多项式，再与目标多项式相比较，得到检查结果，减少了原本按顺序相加产生的中间的二次型多项式的项，提高了检查的效率。

2. 乘法器验证

计算机代数 [9] 是目前为门级乘法器做形式验证最有效的技术之一。计算机代数将电路建模成多项式，并将其规范也建模成多项式，这是由电路导出的多项式所表示的，也就是说，电路中的每个门都有其对应的多项式方程，该方程描述了门的输入与输出之间的关系，并将多项式按照与项顺序一致的拓扑顺序进行排序，这样做能够使门多项式自动生成Gröbner基 [10] ，并运用预处理技术来简化Gröbner基。同时，电路实现逻辑功能，运用其实现的逻辑函数计算二进制数字值，输入时给定二进制值，通常由简单布尔函数表示逻辑门，例如NOT，AND，OR。电路的规格就是电路输入和输出之间的期望关系。若电路的所有输入产生的输出都符合所期望的关系，则证明电路满足其规格，从而得出该电路的正确性。

我们用来验证的工具是Amulet，它将有符号或无符号的整数乘法器C作为输入，电路通常用And-Inverter-Graphs (AIG) [11] 格式表示，考虑门级整数乘法器电路C的2n个输入变量 $a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1}\in \left\{0,1\right\}$ 和2n个输出变量 $s_0,\cdots ,s_{2n-1}\in \left\{0,1\right\}$ 。内部门变量由 $g_1,\cdots ,g_k\in \left\{0,1\right\}$ 表示。设R是一个有单位的交换环，并且 $R\left[a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1},g_0,\cdots ,g_k,s_0,\cdots ,s_{2n-1}\right]=R\left[X\right]$ 。乘法器C是正确的当且仅当对于所有可能的输入 $a_i,b_i\in \left\{0,1\right\}$ 下面的规范多项式 $L=0$ 成立：

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

每一个AIG节点都蕴含着一个多项式关系，如图1。设 $G\left(C\right)\subseteq Z\left[X\right]$ 为多项式集，其包含对于电路C的每个门均有相对应的多项式关系。其中的 $v,w$ 由对应的变量 $x\in X$ 表示，我们称这些多项式为门约束。

Figure 1. All polynomial encodings covered by AIG nodes

图1. AIG节点覆盖的多项式编码

定义 2.1. R是一个环，X表示一组变量 $\left\{x_1,\cdots ,x_l\right\}$ 。 $R\left[X\right]$ 表示X的系数在R中的多项式环。

定义 2.2. 项 $\tau =x_1^{d_1},\cdots ,x_l^{d_l}$ 是变量幂的乘积，其中 $d_i\in N$ ，单项式 $c\tau$ 是项的乘积，其中 $c\in R\backslash \left\{0\right\}$ ，多项式是具有成对不同项的单项式的有限和。

定义 2.3. 在项集 $\left[X\right]$ 上的序关系固定所有项 $\tau ,{\sigma }_1,{\sigma }_2$ ，当 $1\le \tau$ 时，且 ${\sigma }_1\le {\sigma }_2\Rightarrow \tau {\sigma }_1\le \tau {\sigma }_2$ ，这种顺序被称为字典序，如果多项式排序为 $x_1>x_2>\cdots >x_l$ ，对任意两个不同的项 ${\sigma }_1=x_1^{d_1}\cdots x_l^{d_l}$ ， ${\sigma }_2=x_1^{e_1}\cdots x_l^{e_l}$ ，我们有 ${\sigma }_1<{\sigma }_2$ 当且仅当存在变量i，有 $d_j=e_j$ 时，对于所有的 $j<i$ 有 $d_i<e_i$ 。我们有 ${\sigma }_1={\sigma }_2$ 当且仅当对于所有 $1\le j\le l$ 有 $d_j=e_j$ 。

定义 2.4. 对一个多项式 $p=c\tau +\cdots$ ，其中最大的项 $\tau$ 被称为首项 $lt\left(p\right)=\tau$ ，首项系数为 $lc\left(p\right)=c$ ，首项单项式为 $lm\left(p\right)=c\tau$ ，p的尾部为 $tail\left(p\right)=p-lm\left(p\right)$ 。

定义 2.5. 设 $P\subseteq R\left[X\right]$ ，如果对于一个项序，P所有的前导项都只由一个指数为1的变量构成，并且对于所有 $p\in P$ ，有 $lc\left(p\right)\in R^{\times }$ ，则称P有唯一的前导项(UMLT)。

所有变量 $x\in X$ 是布尔值，通过为每个变量添加布尔值约束 $x\left(x-1\right)=0$ 来强调，令 $B\left(Y\right)=\left\{y\left(1-y\right)|y\in Y\right\}\subseteq R\left[X\right]$ ，其中 $Y\subseteq X$ ，是Y的布尔值约束集合。设 $R=Z$ ，由于门多项式的UMLT性质，对于 $J\left(C\right)\subseteq Z\left[X\right]$ ， $G\left(C\right)\cup B\left(X_0\right)$ 定义了一个D-Gröbner基 [12] ，进一步得知 $J\left(C\right)=\langle G\left(C\right)\cup B\left(X\right)\rangle \subseteq Z\left[X\right]$ 即 $J\left(C\right)$ 包含 $x\in X$ 所有布尔值约束。因此，可以通过门多项式和所有布尔约束约简L，并通过检查结果是否为零来确定电路的正确性。将多项式进行简化的过程为算法1，该算法隐式处理 $B\left(X\right)$ ，而不是显式地从 $B\left(X\right)$ 中减少多项式，同时取消大于1比1的指数。

然而，乘法器的GP加法器部分很难用计算机代数来验证，而加法器电路的等效性检查则很容易由SAT求解。因此，将SAT和计算机代数相结合，验证工具Amulet可以自动将复杂的GP加法器替换为简单的纹波进位加法器。用SAT求解器可以验证替换的正确性，用计算机代数可以验证重写乘法器的正确性，同时Amulet中可以生成PAC证明和NSS证明。

3. 代数证明系统

已知在乘法器验证期间分为两个阶段，首先在预处理步骤中，从 $G\left(C\right)$ 中消除变量来获得更简单的多项式表示 $G\left(C\right)\text{'}$ 。其次，通过约简 $G\left(C\right)\text{'}$ 来确定所给的电路是否正确。这两个阶段都包含在NSS证明中，来生成规范多项式L作为初始的门多项式 $G\left(C\right)\in Z\left[X\right]$ 的线性组合。

定义 3.1. 对于一组给定的多项式 $G\subset Z\left[X\right]$ ，令 $\text{base}\left(r\right)=\left\{\left(p_i,q_i\right)|p_i\in G,q_i\in Z\left[X\right]\right\}$ ，如果存在多

项式 $v_1,\cdots ,v_l$ ， $r={\displaystyle {\sum }_{\left(p_i,q_i\right)\in \text{base}\left(r\right)}{q}_i{p}_i+{\displaystyle {\sum }_{i=1}^l{v}_i\left(x_i^2-x_i\right)}}$ ，则称base(r)是关于G的基表示。

为了得到L的NSS证明，需要找到L用 $G\left(C\right)$ 表示的基表示，对于所有多项式 $g\in G\left(C\right)$ ，则认为 $\text{base}\left(g\right)=\left\{\left(g,1\right)\right\}$ 是 $G\left(C\right)$ 的基表示。由于通过算法2导出的重写多项式r替换 $G\left(C\right)$ 的多项式，以此来重写 $G\left(C\right)$ ，也就是说，可以导出 $G\left(C\right)$ 的r的基表示，即base(r)中包含算法1中使用的元组 $\left(p,1\right),\left(p_v,h\right)$ 。

算法2展示了如何通过添加元组 $\left(f,h\right)$ 来更新base(r)，如果算法3的输入多项式f是 $G\left(C\right)$ 的一个元素，即 $\text{base}\left(f\right)=\left\{\left(f,1\right)\right\}$ ，则将 $\left(f,h\right)$ 添加到base(r)中，若base(r)的元组中没有f，需将 $\left(f,h\right)$ 加到base(r)的元组中，这样base(r)的元组 $\left(f,h_i\right)$ 则更新为 $\left(f,h_i+h\right)$ ，这是base(r)中的合并公因式。如果多项式f不是初始门多项式，对于某些初始多项式 $f_i$ 和 ${h^{\prime }}_i\in Z\left[X\right]$ ，f可以写成线性组合 $f={h^{\prime }}_1{f}_1+\cdot \cdot \cdot +{h^{\prime }}_l{f}_l$ 。因此元组 $\left(f,h\right)$ 对应为 $hf=h{h^{\prime }}_1{f}_1+\cdot \cdot \cdot +h{h^{\prime }}_l{f}_l$ ，我们遍历元组 $\left(f_i,{h^{\prime }}_i\right)\in \text{base}\left(g\right)$ ，将每个协因子 ${h^{\prime }}_i$ 乘以h，并将对应的元组 $\left(f_i,h{h}_i\right)$ 添加到base(r)中。

预处理完成后重复应用算法2，将规范多项式L约简 $G\left(C\right)$ ，通过推导L的基表示来生成NSS证明。因此在每次约简之后都要将元组 $\left(g,h\right)$ 添加到base(L)中，其中h是多项式g相应的协因子。在完成最后的约简之后，base(L)就表示NSS证明并将其打印到文件中。

NSS证明系统推导出是否多项式 $f\in R\left[X\right]$ 可以表示为给定集合 $G=\left\{g_1,\cdots ,g_m\right\}$ ，也就是说，对于给定多项式f和集合 $G=\left\{g_1,\cdots ,g_m\right\}$ 是数组 $P=\left(h_1,\cdots ,h_m\right)$ 的多项式，例如

${\displaystyle \underset{i=1}{\overset{m}{\sum }}{h}_i{g}_i=f}$ (2)

NSS证明的健全性和完备性论证都可以推广到环 $R\left[X\right]$ ，当G具有UMLT时，在NSS证明中，布尔值约束被隐式处理以产生更短的证明。因此对于给定多项式 $f\in R\left[X\right]$ 和多项式集 $G=\left\{g_1,\cdots ,g_m\right\}\subseteq R\left[X\right]$ 是一组协因子 $P=\left(h_1,\cdots ,h_m\right)$ 的多项式，使得存在多项式 $r_1,\cdots ,r_l\in R\left[X\right]$ ，有

${\displaystyle \underset{i=1}{\overset{m}{\sum }}{h}_i{g}_i+{\displaystyle \underset{i=1}{\overset{l}{\sum }}{r}_i\left(x_i^2-x_i\right)}}=f$ (3)

4. 检查器及优化

4.1. NSS认证器

NSS认证器Nuss-Checker是运用C语言实现的。Nuss-Checker需要读入三个输出文件 ，

和 ，文件 包含初始约束 $g_i\in G$ ， 按同样的顺序包含对应的协因子 $h_i$ 。Nuss-Checker读取文件 和 生成乘积，并将乘积进行求和，验证所得的多项式和f是否与文件 中所给的多项式L相等。

认证器通过检查是否 ${\displaystyle {\sum }_{i=1}^l{h}_i{g}_i}=f\in Z\left[X\right]$ ， $p_i\in G\subseteq Z\left[X\right]$ ， $f,h_i\in Z\left[X\right]$ 来判断NSS证明的正确性。理论上来讲，只需要将初始门约束 $g_i$ 乘以协因子 $h_i$ ，然后计算乘积的和。这听起来是很简单的，但是根据实现的不同，分配的时间和最大内存量是会出现数量级变化。

Nuss-Checker中的多项式在内部存储为单项式的有序链表，系数则用GMP库表示，项是变量的有序链表，内部使用散列表来分配项。在运行过程中，Nuss-Checker动态的生成乘积 $h_i{g}_i$ ，也就是说要同时解析文件 和 ，并从两个文件中分别读取出两个多项式 $g_i$ 和 $h_i$ ，并计算 $h_i{g}_i$ 。两个多项式的相加是通过将这两个多项式的单项式推入堆栈中实现的，用固定项顺序在堆栈上进行排序，将拥有相同项的单项式进行合并来生成最终的和式，乘法也是运用的类似的方法。在计算多项式求和的过程中， $Z\left[X\right]$ 中的加法方式是结合式的，将l个乘积 $h_i{g}_i$ 的所有单项式都推到一个大堆栈中，之后对堆栈上的单项式进行排序和合并，所有的乘积的单项式被推到堆栈上进行存储以及排序和合并，这都增加了Nuss-Checker的使用时间。同时按顺序相加，只在内存中存储一个多项式，总是添加最新的乘积 $h_i{g}_i$ ，但目标多项式L包含着n ²个多项式的中间项 $a_i{b}_j$ ，这使得中间和的指数大小为二次，也增加了验证的时间。

4.2. 队列及树状加法

队列(queue)是一种线性结构，与同为线性数据结构的栈不同的是，队列中的元素遵循的是先入先出规则，当将数据存入队列称为“addQueue”，需要两个步骤：

1. 将尾指针往后移：rear + 1，当 $\text{front}=\text{rear}$ 时为空。

2. 若尾指针rear小于队列的最大下标MaxSize−1，则将数据存入rear所指的数组元素中，否则无法存入数据， $\text{rear}=\text{maxsize}-1$ ，则队列满。

如图2所示，在初始化队列时，令 $\text{front}=\text{rear}=0$ ，当有新元素插入队尾时，尾指针增1；当元素需从队头出队时，头指针增1。因此在非空队列中，头指针始终指向队列头元素，而尾指针始终指向队尾元素的下一个位置。在本文中由于需要将每相邻的两个多项式的和作为新元素重新放入存储空间中等待下一次相加，所以选择使用队列对检查器的多项式相加过程进行优化。

Figure 2. All polynomial encodings covered by AIG nodes

图2. 队列运行示意图

树形加法是通过在树结构中相加，将NSS证明的两个连续的乘积结果相加并加以存储，如图3所示。

这样在一次遍历相加之后，在队列中会存在 $\frac{l}{2}$ 个多项式，经过在队列中反复迭代，总是对两个连续的多

项式求和，并把新的结果推送到队尾，直到最后只剩下一个多项式，这样减少了指数为二次的中间和，因此本文采用树形加法对队列上的多项式求和进行优化。

Figure 3. All polynomial encodings covered by AIG nodes

图3. 树状结构的加法示意图

4.3. 优化算法

基于队列的树形加法优化是将堆栈上存储的多项式 $p_1,p_2,\cdots ,p_l$ 重新推送到队列内进行存储，同时运用树状加法将p₁与p₂相加，p₃与p₄相加，直至 $p_{l-1}$ 与 $p_l$ 相加，相加所得和推送至队尾入列。此时队列内存储了 $\frac{l}{2}$ 个多项式，之后重复该步骤进行反复迭代，直至队列中只剩下一个多项式，即为生成多项式f，则求和过程结束，随之便可将所得的生成多项式与目标多项式进行对比得出结论。

如下所展示的算法给出了优化的具体过程：(1)初始化一个队列，检查队列是否为空，是否已满；(2)入队，将l个多项式 $p_1,p_2,\cdots ,p_l$ 存储进队列；(3)获取队列长度，并获取队列前端元素进行打印；(4)取整个队列长度的一半，利用for循环，将相邻多项式分别赋值给 $p,q$ ，并将 $p,q$ 相加，随后删除 $p,q$ ；(5)将相加所得的和添加至队尾重新入列；(6)重复前面步骤进行反复迭代；(7)判断队列长度是否为1，若为1，则将唯一的多项式输出。

基于队列的树形加法优化使得在最终求和的过程中，面对庞大、繁杂的单项式与多项式，总是能尽快的添加同一层的两个多项式来动态的运用树形加法，同时结合队列的灵活性，减少其相加求和时产生的中间项的次数，简化运算大小，更加方便、快捷、高效的完成认证器的检查过程，提高了认证器的检查效率。

5. 实验

本文中的实验使用的是一台带有Ubuntu 18.04.6虚拟机的电脑，配置为Intel i5-6300HQ，2.30GHz和2GB内存，实验用的工具是Amult和Nuss-checker。选择了btor乘法器 [13] 和sp-ar-rc乘法器 [14] 电路进行验证。这两类的乘法器结构略有不同，btor乘法器是将全加器和半加器用网状结构累积，sp-ar-rc乘法器是将全加器和半加器用对角线结构累积。如图4、图5所示，是4位btor乘法器和4位sp-ar-rc乘法器的结构示意图。

实验时间表示从运行代码开始，到最后得出该乘法器是否为正确的乘法器结论为止所花费的时长，单位为秒，时间限制为600秒。内存的单位为MB，内存限制为2048 MB。实验结果如表1所示。

实验将按顺序相加所得多项式的时间与基于队列的树形加法所得的多项式的时间相对比，可以显著得知，基于同类型同位数的乘法器，相比于顺序相加，优化后所需的时间有了明显减少。随着乘法器复杂度的提升，这种差异会越来越明显。

Figure 4. 4-bit btor multiplier structure

图4. 4位btor乘法器结构

Figure 5. 4-bit sp-ar-rc multiplier structure

图5. 4位sp-ar-rc乘法器结构

Table 1. Resulting data of experiment

表1. 试验结果数据

6. 结论

本文对验证NSS证明时NSS认证器检验其生成多项式的过程进行优化。原本需要不断添加最新的乘积 $h_i{g}_i$ 到多项式中，但因为目标多项式L包含n²个多项式的中间项，导致中间和的指数大小为二次，而基于队列的树形加法改变了多项式的求和方式，将两个连续的乘积相加并求和存储，这样不会产生有n²个多项式的中间项的情况，使得认证器的检查时间有了明显的减少，提高了认证器的检验效率。未来的工作中，希望该算法方式也会运用于不同的应用程序。

参考文献

NOTES

^*通讯作者。