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

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

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

形式验证的很多应用可以运用可满足性(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]是目前为门级乘法器做形式验证最有效的技术之一。

计算机代数将电路建模成多项式， 并将其规范也建模成多项式，这是由电路导出的多项式所表示的，也就是说，电路中的每个门都有其对应的多项式方程，该方程描述了门的输入与输出之间的关系，并将多项式按照与项顺序一致的拓扑顺序