1. 引言

门级整数乘法器是数字电路系统中重要组成部分，也是如数学信号处理、密码学和机器学习中不可或缺的运算单元。复杂多样的乘法算法和大量的构建块使其成为许多设计中最复杂的部分之一，所以在今天，整数乘法器的全自动验证仍然是一项困难的工作。

形式验证可以用来证明或反驳给定系统相对于电路规范的正确性。为给定系统建立数学模型，并应用自动决策过程来导出所需的正确性属性。到目前为止，已经研究出多种用于验证乘法器电路正确性的求解技术。如1994年著名Pentium FDIV错误 [1] 使用的其中一种技术是基于二进制决策图 [2] ，然而，这种方法严重依赖于乘法器的架构，容易发生指数爆炸。基于可满足性检查(SAT)的方法 [3] 不具可扩展性，无法验证大规模的乘法器电路。基于定理证明器和SAT相结合的方法可以证明工业乘法器 [4] ，但定理证明器不是完全自动化的。最近，有学者优化了定理证明器的方法 [5] 。然而，乘法器必须以分层SVL网表的形式给出，这依赖于电路分层信息的保存，对我们研究的乘法器仍然是不适用的。对于扁平门级乘法器，目前最成功的技术是基于代数推理 [6] [7] [8] [9] [10] 。在这项工作中，电路被建模为一组生成Gröbner基的多项式，然后使用多项式归约算法检查规范是否由电路多项式隐含。

即使代数推理工作可以有效地验证乘法器电路，但验证过程可能不是没有错误的。为了保证验证结果的正确性，必须正式地检查验证结果。例如，使用定理证明器，需要繁琐的工作步骤，同时在结构复杂的工具上是不可行的。因此，增加对验证结果的信任的一种更常见的技术是生成证明证书，它监视验证过程的步骤并可以复制证明。现有一种涵盖代数推理的证明格式PAC。它基于多项式演算(PC) [11] ，通过捕捉门多项式，使用代数理想理论从给定的多项式集导出。与PC相比，PAC证明是它扩展后的实例化，还允许对多项式进行索引，添加删除规则和扩展规则，能够更有效地被认证器检查。

本文通过改进认证器中变量的排序方法，利用级别值对变量进行排序，大大减少了不能进行内部共享的冗余项的数量，进而减少认证器的内存使用。其次本文用C++语言实现了基于PAC证明格式的认证器。将不同操作的函数封装为各个类，避免了程序元素之间的高耦合性，为认证器之后的使用提供了更好的可维护性和可扩展性。

2. 基本概念

2.1. 乘法器电路

非循环的门级整数乘法器电路，电路规范表示其输入与输出之间的期望关系。如果电路对所有输入产生的输出都与这个期望的关系相匹配，那么就说它就满足电路规范。形式验证就是证明电路符合其规范。

对于具有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\}$ 的乘法器电路C。

当表示无符号整数的乘法器电路时，其电路规范为 $U_n=-{\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)$ ，乘法器是正确的当

且仅当对于所有输入，有 $U_n=0$ 成立。当表示有符号整数的乘法器电路时，最高有效位 $S_{2n-1}$ 、 $a_{n-1}$ 和 $b_{n-1}$ 具有决定符号作用，权重需要进行取反，此时电路规范为

$S_n=-2^{2n-1}{s}_{2n-1}+{\displaystyle \underset{i=0}{\overset{2n-2}{\sum }}{2}^i}{s}_i-\left(-2^{n-1}{a}_{n-1}+{\displaystyle \underset{i=0}{\overset{n-2}{\sum }}{2}^i}{a}_i\right)\left(-2^{n-1}{b}_{n-1}+{\displaystyle \underset{i=0}{\overset{n-2}{\sum }}{2}^i}{b}_i\right)$ ，乘法器是正确的当且仅当对于所有输

入，有 $S_n=0$ 成立。

2.2. 代数模型

设X表示变量 $\left\{x_1,\cdots ,x_l\right\}$ 的集合，我们用 $Z\left[X\right]$ 表示变量X中的多项式环，系数在Z中。如上节讨论的具有2n个输入和输出的整数乘法器电路， $l_0,\cdots ,l_k\in \left\{0,1\right\}$ 表示其内部AIG节点，变量集X在字典序下定义为 $X=\left\{a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1},l_0,\cdots ,l_k,s_0,\cdots ,s_{2n-1}\right\}$ 。

电路中的每个逻辑门被编码为多项式，常见的多项式如下：

$u=\neg v\iff -u+1-v=0$

$u=v\wedge w\iff -u+vw=0$ (1)

$u=v\vee w\iff -u+v+w-vw=0$

$u=v\oplus w\iff -u+v+w-2vw=0$

设 $G\left(C\right)\subseteq Z\left[X\right]$ 是多项式集，根据反向拓扑序排序，包含每个AIG节点的对应多项式关系。所有变量 $x\in X$ 都是布尔的，通过布尔值约束集 $B\left(x\right)=\left\{x\left(1-x\right)|x\in X\right\}\subseteq Z\left[X\right]$ 来约束。

定义2.1. 如果 $\forall p,q\in I:p+q\in I$ 和 $\forall p\in Z\left[X\right],\forall q\in I:pq\in I$ ，则非空子集 $I\subseteq Z\left[X\right]$ 被称为理想。如果集合 $I=\left\{p_1{q}_1+\cdots +p_s{q}_s|q_1,\cdots ,q_s\in Z\left[X\right]\right\}$ ，则集合 $P=\left\{p_1,\cdots ,p_s\right\}\subseteq Z\left[X\right]$ 称为I的基，称I是由P生成的，写作 $I=\langle P\rangle$ 。理想I和J的和定义为 $I+J=\left\{p+q|p\in I,q\in J\right\}$ 。

定义2.2. 设 $P\subseteq Z\left[X\right]$ ，如果对于某个项阶，P的所有前导项只由指数为1的唯一单个变量组成，并且对所有 $p\in P$ ， $lc\left(p\right)\in \left\{-1,1\right\}$ ，则称P具有唯一的单前导项(UMLT)。设 $X_0\left(P\right)\subseteq X$ 不作为P中的前导项出现的所有变量的集合。进一步定义 $B_0\left(P\right)=B\left(X_0\left(P\right)\right)$ 。

此外，由于可以进行模块化推理，只有在 $Z\left[X\right]$ 中才能添加常量，我们将常数2n添加到 $J\left(C\right)$ 的理想生成器中，从多项式中消除系数过大的单项式 [8] 。

定义2.3. 设C是一个电路， $J\left(C\right)=\langle G\left(C\right)\cup B_0\left(X\right)\rangle \subseteq Z\left[X\right]$ ，是由 $G\left(C\right)\cup B_0\left(X\right)$ 生成的理想。

定义2.4. 电路C满足规范L当且仅当 $L\in J\left(C\right)$ 。

定理2.1. 设 $J\left(C\right)=\langle G\left(C\right)\cup B_0\left(C\right)\cup \left\{2^n\right\}\rangle \subseteq Z\left[X\right]$ ，那么 $G\left(C\right)\cup B_0\left(C\right)\cup \left\{2^n\right\}$ 是 $J\left(C\right)$ 关于固定逆拓扑项序的一个D-Gröbner基。

在约简过程中，提前消除 $G\left(C\right)$ 中的变量，以避免在过程中出现指数级的中间结果，形成更紧凑的D-Gröbner基。利用多项式 $G\left(C\right)\cup B_0\left(C\right)\cup \left\{2^n\right\}$ ，对规范L进行D-Gröbner基约简，通过检验结果是否为0来判断电路正确性。

2.3. 实用代数演算

实用代数演算(PAC)是将多项式演算实例化为更具体的证明格式，其证明格式是包括加法和乘法运算的一系列证明规则。不仅隐式地处理布尔值约束上的操作，通过归一化指数来减少证明步骤的数量。还对多项式进行索引，为每个给定的多项式和证明步骤使用一一对应的正数标记。例如，第一个步骤产生的结论多项式在第三个证明步骤中被再次作为前提使用，这时我们只需使用索引标记第一个证明步骤，在第三个步骤使用该结论多项式的位置直接使用索引替代表示。并添加了删除规则，在每个证明步骤完成时，添加到约束集中的结论多项式若不再被需要，则使用删除规则来删除不需要的多项式。能够有效地生成更短和更简洁的PAC证明。

设P表示可以通过索引访问的多项式序列， $P\left(i\right)=\perp$ 表示在索引i处序列P不包含多项式， $P\left(i\mapsto p\right)$ 表示将索引i处设置为序列P。初始状态为 $\left(X=Var\left(G\cup \left\{f\right\}\right),P\right)$ 其中P包含G的所有多项式。证明规则如下：

$ADD\left(i,j,k,p\right)$ $\left(X,P\right)\Rightarrow \left(X,P\left(i\mapsto p\right)\right)$

假设 $P\left(j\right)\ne \perp ,P\left(k\right)\ne \perp ,P\left(i\right)\ne \perp ,且p=P\left(j\right)+P\left(k\right)\in Z\left[X\right]$

$MULT\left(i,j,q,p\right)$ $\left(X,P\right)\Rightarrow \left(X,P\left(i\mapsto p\right)\right)$ (2)

假设 $P\left(j\right)\ne \perp ,P\left(k\right)\ne \perp ,q\in Z\left[X\right],且p=q\cdot P\left(j\right)\in Z\left[X\right]$

$DELETE\left(i\right)$ $\left(X,P\right)\Rightarrow \left(X,P\left(i\mapsto p\right)\right)$

此外，PAC添加了扩展规则，它允许将任意新的多项式作为初始约束添加到初始集合G中进行扩展。并通过否定对任意 $x\in X$ 引入额外的新变量 $\bar{x}$ ，添加形式为 $-f_x+1-x$ 的多项式，同时保留原始变量集X 上的原始模型。

$EXT\left(i,v,p\right)$ $\left(X,P\right)\Rightarrow \left(X\cup \left\{v\right\},P\left(i\mapsto -v+p\right)\right)$ (3)

假设 $P\left(i\right)=\perp ,且v\notin X,p\in Z\left[X\right],p^2-p=0$

例如，目标多项式 $-c+1\in \langle G\cup B\left(X\right)\rangle \subseteq Q\left[X\right]$ 的PAC证明如下，其中。

3. 认证器的优化与实现

3.1. 类封装函数

封装性是C++面向对象语言 [12] 的三大特性之一，还包括继承性与多态性。我们可以将一切事物都视为对象，对象有其特定属性和行为，具有相同性质的对象，我们将其抽象为类。例如人属于人类，车属于车类。成员变量和成员函数是类函数的两个基本组成部分。成员变量(也称为属性或数据成员)是类的数据存储单元，用于存储对象的状态信息。成员函数(也称为方法或操作)是类的行为或功能，用于操作和处理成员变量。在本文的认证器中，我们封装了如表1所示的六个类：

接下来我们详细阐述表示变量幂积的类Class Power{}，如图1所示。项 $\tau =x_1^{d_1}\cdot \cdots \cdot x_r^{d_r}$ 是关于 $d_i\in N$ 的变量幂的乘积，单项式是项 $c\tau$ 的倍数，多项式是带有两两不同的项的单项式的有限和。成员变量variable用来存储变量 $x_1,x_2,\cdots ,x_r$ ，exponent用来存储指数 $d_1,d_2,\cdots ,d_r$ 。其成员函数包括print_power()，enlarge_powers()，sort_powers()分别用来表示为输出幂的乘积到文件中的函数，扩容申请原来所占内存二倍的空间进行存储的函数和根据变量顺序对幂积进行排序的函数。

将变量和功能封装在一个类中，隐藏内部实现细节，避免外部直接访问内部的变量和方法，增强了数据的安全性。可以方便地在后面需要的地方重复使用，减少代码冗余，提高代码的可读性。此外类函数可以通过继承和多态的方式进行扩展。通过继承可以创建新的类，例如，多项式类Polynomial是单项式类Monomial的扩展，单项式类Monomial是项类Term的扩展，它们都继承原有类的属性和方法，然后在新类中添加新的功能。多态可以在运行时动态地选择调用不同的方法，从而实现不同的行为。因此，面向对象语言，各对象是一个独立体，各自完成不同的功能，耦合度低，扩展力强，复用性强。

3.2. 优化变量排序

验证工具Amulet2.0验证门级整数乘法器生成三个文件 、 和 。文件 为诱导约束集，验证生成的证明步骤在文件 中给出，文件 包含一个符合电路规格的规范多项式。认证器Pacheck [13] 将上述三个文件作为输入，目的在于验证目标规范多项式是否包含在约束集中的多项式生成的理想中。

多项式类Polynomial，表示为单项式的有序链表，用于完成所需计算的所有多项式的算数运算。类Monomial用于表示多项式中的单项式，每个单项式由一个系数和一个项组成。类Term用于表示多项式中的项，将项表示为变量的有序链表，这些变量使用哈希表在内部共享。不同的变量排序大大影响了产生项的数量，从而影响了认证器的内存使用。如图2所示，选择不同的变量排序方式来表示两个单项式 $uxy$ 和 $vxy$ 。关于 $v>u>x>y$ 的变量顺序，项x和项y可以进行内部共享，只需分配4个项。而关于 $x>u>y>v$ 的变量顺序，项不能进行共享，需要分配6个项。

如表2所示，我们提出了新的基于级别值对变量排序的函数cmp_variable_level()。替换掉原来的cmp_variable_name()函数，即通过比较变量存储的字符串进行排序的方法。选择与给定证明文件中变量输入顺序相同的排序方法，在读取给定证明文件时为新变量分配递增的级别值level，并根据该值进行排序。多项式中的项使用与变量相同的顺序进行排序。从而可以充分地内部共享项，减少没有必要的项的分配，从而减小证明检查器的内存使用。例如检查128位sp-ar-rc乘法器所生成的证明证书，按照原始比较字符串的方法排序产生了340,354个项占总项数64%，而选择变量级别值排序，产生项数占总项数57%，大大减少了生成的项的数量。

4. 实验

本文实验使用了一台带有 Ubuntu18.04虚拟机的电脑，配备Intel(R) Pentium(R) CPU G4560 3.50 GHz和限制为4 GB的主内存。实验时间以秒为单位，最高限制为300秒。首先使用工具Amulet2.0生成统一计算机代数和SAT证明的PAC证明格式的证书，验证输入位宽度为n的乘法器的正确性。实验上半部分选择架构为btor和sp-ar-rc类型的乘法器，以验证大型简单乘法器电路的正确性。下半部分选择aoki基准，其中乘法器的末级加法器都是GP加法器，以验证含有复杂末级加法器的复杂乘法器电路的正确性，实验结果如表3所示。

本文的实验中，我们首先对不同架构下的乘法器进行验证，生成统一PAC格式的证明证书。再比较由认证器检查证明证书所用时间和占用内存大小。通过表3的数据结果可以看出，优化后的认证器不仅能够检查带有复杂末级加法器的乘法器生成的证明证书，而且检查各个类型乘法器证明证书在时间上和内存上都得到了优化。

5. 结束语

本文优化了变量排序方法，根据证明文件中变量输入顺序排序的方法，能够充分地在内部共享项，减少了不必要项的分配。实验结果表明，优化后的认证器减少了认证过程中的内存使用。此外我们基于C++语言重新实现了检查PAC证明格式的认证器，引用类函数，将对象的属性和操作封装为一个独立的整体，大大提高了程序的安全性和复用性，同时降低了函数元素间的高耦合性，使我们的认证器更具扩展性和可维护性。在未来的工作中，我们希望对认证器进行扩展以检查更多不同格式的证明证书，并占用更小内存。

参考文献

NOTES

^*通讯作者。

参考文献