基于散列表的加法器重写优化算法

Hash Table Based Adder Rewriting Optimization Algorithm

摘要: 在大规模算术集成电路设计领域中，乘法器电路的验证是一重大难题。当前主流的方法是Gröbner基法。在此基础上，研究者们提出了加法器重写等优化方法，但重写过程依赖进位变量且需遍历全部变量，导致验证效率降低。为此，本文利用散列表对该方法进行优化，使用散列表存储所有和位输出变量，遍历表中元素进行扩充，再结合加法器的结构特性去识别加法器，从而不再依赖进位变量并且减少了需要遍历的变量数目。由实验结果可知，优化算法提高了Gröbner基的生成效率，也提高了乘法器的验证效率。

Abstract: In the field of very large scale integration design, the verification of multiplier circuits is a major problem. The current mainstream method is the Gröbner basic method. On this basis, researchers have proposed optimization methods such as adder rewriting, but the rewriting process relies on carrying variables and needs to traverse all variables, resulting in reduced verification efficiency. For this reason, this paper optimizes the method by using a hash table, uses a hash table to store all the sum bit output variables, expands the elements in the traversal table, and then identifies the adder by combining the structural characteristics of the adder, so that it no longer depends on car-rying variables and reduces the number of variables that need to be traversed. The experimental results show that the optimization algorithm improves the generation efficiency of Gröbner basis and the verification efficiency of multipliers.

1. 引言

在大规模集成电路设计领域中，电路正确性的验证是极其重要的一环。若不加以验证，可能会出现产品的研发失败、缺陷等等问题。例如最著名的“奔腾浮点运算错误 [1] ”，直接导致inter公司损失上亿美元的资产。为了防止此类错误的发生以及减少损失，需要对电路的正确性进行验证。

传统的模拟验证方法费时低效，后经研究发现，形式化验证方法 [2] 不仅可以发现类似“奔腾浮点运算错误”，而且还可以对错误进行改正。正是因其优越性，形式化验证方法在国内外不断地向更高的理论水平和实践领域蓬勃发展。

形式化验证是通过数学的方法去证明一个系统或电路满足所给的设计规范 [3]。形式化验证的方法分为三大类：模型验证、定理证明以及等价性验证。在乘法器电路验证问题上，常采用等价性验证方法。等价性验证分为图表示法和代数表示法 [4]。其中，图表示法是利用二叉判定图(BDD) [5]，将电路建模，然后基于有限状态机遍历算法去计算可达状态 [6]。此方法虽经长久发展，但状态集呈指数型增长，会出现状态空间爆炸问题；受到图形的限制，有些问题仍无法通过图表示法去解决。因此在乘法器电路验证中，代数表示方法更加适合。

基于Gröbner基的代数表示方法是当前主流的验证方法。在此方法中，会对规范进行归约，归约过程中的单项式数目会爆炸式增长，导致验证的速度和效率都会降低；当乘法器位数较高时，Gröbner基中的多项式数目会非常庞大。针对这类问题，研究者们提出了加法器重写 [7]、逐列验证 [8]、末级加法器替换 [9] 等方法，这些方法都有效的解决了规范归约过程中单项式数目爆炸增长的问题。

在加法器重写方法中，随着乘法器位数增加，需要遍历的变量数目会爆炸式增加，并且在识别加法器的过程中依赖进位变量，这些情况都会导致验证效率的降低。

针对以上存在的问题，文本提出了基于散列表的加法器重写优化算法。使用散列表储存电路中全部和位输出变量，结合电路逻辑门中输出和输入的关系，遍历散列表进行扩充，然后根据乘法器的结构特性，再次遍历去识别加法器。此算法有如下的几个优点：第一，优化算法针对全部和位输出变量，而非对全部变量进行遍历，减少了遍历的变量数目；第二，不依赖进位变量识别加法器，而是利用加法器的结构特性来进行识别，识别的速度和效率会提升；第三，加法器重写会出现重复遍历变量的问题，结构也比较混乱，而优化算法把搜寻加法器分为了两个遍历，算法的结构更加清晰明了。由实验结果可知，优化算法加快了Gröbner基的生成效率，提高了乘法器电路的验证效率。

2. Gröbner基理论

本节介绍Gröbner基方法的理论基础和理想成员的判定方法，更详尽的的定义及定理可参考 [10] [11] [12]。

设k是一任意数域， $x_1,\cdots ,x_n$ 是n个变量(或称文字)，称 $k\left[x_1,\cdots ,x_n\right]$ 是关于变量 $x_1,\cdots ,x_n$ 的n元多项式环。

定义2.1. 设非空子集 $I\subseteq k\left[x_1,\cdots ,x_n\right]$，若I满足下列条件：

1) $0\in I$ ；

2) 对任意的多项式 $f,g\in I$，都有 $f+g\in I$ ；

3) 对任意的多项式 $f\in I$， $p\in k\left[x_1,\cdots ,x_n\right]$ 都有 $pf\in I$。

则称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 \underset{i=1}{\overset{s}{\sum }}{h}_i{f}_i|h_i\in k\left[x_1,\cdots ,x_n\right]}\right\}$ (1)

成立，则I是一个多项式理想，称 $\left\{f_1,\cdots ,f_s\right\}$ 是I的一组基。

定义2.3. 给定多项式环 $k\left[x_1,\cdots ,x_n\right]$ 特定的序关系<，I为任意一个多项式理想，对于非空有限子集 $G=\left\{g_1,\cdots ,g_s\right\}\subseteq I$，若满足

$\langle LT\left(g_1\right),\cdots ,LT\left(g_s\right)\rangle =\langle LT\left(I\right)\rangle$ (2)

则称G是I关于序关系<的一组Gröbner基，其中 $LT\left(g_i\right)$ 表示 $g_i$ 的首项。

对于上述的G并不唯一，它与序关系<的选择有关，同时，Gröbner基理论为理想成员的判定提供了方法：

定理2.4. 设I为任意一个多项式理想，G是I的一组Gröbner基， $q\in k\left[x_1,\cdots ,x_n\right]$，q除以G所得的余式r满足 $q-r\in I$，当且仅当 $r=0$ 时， $q\in I$。

3. 代数模型

由上文可知验证乘法器电路的正确性需要得到理想的一组Gröbner基。利用Buchberger算法虽然可以计算出某一序下的Gröbner基，但该算法的时间和空间复杂度都是呈指数级的，所以本文将电路直接建模为一组Gröbner基。

设乘法器电路C有2n个输入变量 $a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1}$ 和2n个输出变量 $s_0,\cdots ,s_{2n-1}$，电路中每个内部门变量由 $g_0,\cdots ,g_{k-1}$ 表示，给定字典序 ${<}_{lex}$ ：

$X=a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1},g_0,\cdots ,g_{k-1},s_0,\cdots ,s_{2n-1}$ (3)

把电路中的逻辑门建模为多项式，其中常见逻辑门的多项式如下u所示：

$\begin{array}{l}u=\neg v\iff -u+1-v=0\\ u=v\wedge w\iff -u+vw=0\\ u=v\vee w\iff -u+v+w-vw=0\\ u=v\oplus w\iff -u+v+w-2vw=0\end{array}$ (4)

由于(3)中的变量均是布尔变量，所以变量取值是0或1。对于(3)中任意变量设为u，称 $-u^2+u$ 为域多项式，它们所构成的集合称为域多项式集。

定义2.5. 设C是一个电路，G是所有逻辑门的多项式(4)和域多项式集构成的集合，G生成的理想 $\langle G\rangle$ 记为 $J\left(C\right)$。

由定义2.3和定义2.5可知，在字典序 ${<}_{lex}$ 下，G是 $J\left(C\right)$ 的一组Gröbner基。

定义2.6. 设C是一个电路，多项式 $p\in k\left[x_1,\cdots ,x_n\right]$。任意 $\left(a_0,\cdots ,a_{n-1},b_0,\cdots ,b_{n-1}\right)\in {\left\{0,1\right\}}^{2n}$ 及 $g_0,\cdots ,g_{k-1},s_0,\cdots ,s_{2n-1}$ 的结果值代入p中使得p为0，则称p为电路C的规范多项式，记为PCC，记 $I\left(C\right)$ 为所有PCC的集合。

定理2.7. 对于任意无回路电路C，有 $I\left(C\right)=J\left(C\right)$。

定义2.8. 设C是一个电路，若多项式

${\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)$ (5)

是一个PCC，则称电路C为乘法器电路，称上述多项式为规范多项式sp。

根据本节的定理、定义及推论可知，验证乘法器电路的正确性问题转化为了理想成员的判定问题，即验证规范多项式sp是否属于 $J\left(C\right)$。再由定理2.4，等价于验证sp除以G所得余式r是否为0。若为0，则电路C是乘法器电路；若不为0，则电路C不是乘法器电路。

全加器是乘法器电路的重要构成部分，接下来以全加器电路为例，验证其正确性。

例1：如图1所示，验证全加器电路C的正确性。

Figure 1. Full-adder circuit

图1. 全加器电路

电路C的规范多项式 $sp=-2c_i-s_i+a_i+b_i+c_{i-1}$，将电路中的变量按逆拓扑序排序：

$a_i<b_i<c_{i-1}<g_0<g_1<g_2<s_i<c_i$ (6)

则电路C在该序下的Gröbner基为：

$\begin{array}{l}{G}_C=\{-c_i-g_2{g}_1+g_2+g_1,-s_i-2g_0{c}_{i-1}+g_0+c_{i-1},-g_2+b_i{a}_i,\\ -g_1+g_0{c}_{i-1},-g_0-2b_i{a}_i+b_i+a_i,-c_i^2+c_i,-s_i^2+s_i,\\ -g_2^2+g_2,-g_1^2+g_1,-g_0^2+g_0,-c_{i-1}^2+c_{i-1},-b_i^2+b_i,-a_i^2+a_i\}\end{array}$

接下来用规范多项式sp除以 $G_C$ ：

$\begin{array}{l}sp\stackrel{-c_i-g_2{g}_1+g_2+g_1}{\to }-s_i+2g_2{g}_1-2g_2-2g_1+c_{i-1}+b_i+a_i\\ \stackrel{-s_i-2g_0{c}_{i-1}+g_0+c_{i-1}}{\to }2g_2{g}_1-2g_2-2g_1+2g_0{c}_{i-1}-g_0+b_i+a_i\\ \stackrel{-g_2+b_i{a}_i}{\to }2g_1{b}_i{a}_i-2g_1+2g_0{c}_{i-1}-g_0-2b_i{a}_i+b_i+a_i\\ \stackrel{-g_1+g_0{c}_{i-1}}{\to }2g_0{c}_{i-1}{b}_i{a}_i-g_0-2b_i{a}_i+b_i+a_i\\ \stackrel{-g_0-2b_i{a}_i+b_i+a_i}{\to }-4c_{i-1}{b}_i^2{a}_i^2+2c_{i-1}{b}_i^2{a}_i+2c_{i-1}{b}_i{a}_i^2\\ \stackrel{-b_i^2+b_i}{\to }-4c_{i-1}{b}_i{a}_i^2+2c_{i-1}{b}_i{a}_i+2c_{i-1}{b}_i{a}_i^2\\ \stackrel{-a_i^2+a_i}{\to }0\end{array}$

由上述计算得到余式 $r=0$，所以全加器电路C是正确的。

4. 加法器重写及优化

4.1. 加法器重写

随着乘法器位数的增加，乘法器电路的Gröbner基中多项式数目会急剧增多，导致乘法器验证效率大大降低。为了解决此问题，研究者们提出了加法器重写算法 [7]。算法的基本思想是遍历所有变量去识别进位变量，然后利用进位变量去搜索加法器，再进行变量消去，即使用加法器的规范替换Gröbner基中对应的所有内部门多项式。该方法简化了Gröbner基，提高了乘法器电路的验证效率。

加法器分为全加器(Full-adder)和半加器(Half-adder)，定义如下：

定义4.1. 设C是一个电路，对于输入 $a,b,i$ 及输出 $c,s$，若 $-2c-s+a+b+i$ 是PCC，则称电路C是全加器；对于输入 $a,b$ 及输出 $c,s$，若 $-2c-s+a+b$ 是PCC，则称电路C是半加器。

对于例1中全加器电路C的Gröbner基 $G_C$ 经过简化，可得：

$\begin{array}{l}{H}_C=\{-c_i-g_2{g}_1+g_2+g_1,-s_i-2g_0{c}_{i-1}+g_0+c_{i-1},-g_2+b_i{a}_i,\\ -g_1+g_0{c}_{i-1},-g_0-2b_i{a}_i+b_i+a_i\}\end{array}$

其中 $\langle H_C\rangle =J\left(C\right)$， $H_C$ 是电路C的Gröbner基。

接下来给出相关定理及定义，消去 $H_C$ 中的内部门变量 $g_0,g_1,g_2$，用加法器关于输入 $a,b,i$ 的多项式表示输出 $s,c$。

设R为环， $R_{\text{elim}}$ 为环 $\mathbb{Q}\left[a_i,b_i,c_{i-1},s_i,c_i\right]$。

定义4.2. 对于 $J\subset R$， $J_{\text{elim}}=J\cap R_{\text{elim}}$，则称 $J_{\text{elim}}$ 是 $R_{\text{elim}}$ 的消去理想。

定理4.3. 设 $J\subset R$ 是理想，如果H是J关于给定序

$a_i<b_i<c_{i-1}<s_i<c_i<g_0<g_1<g_2$ (7)

的Gröbner基，则 $H_{\text{elim}}=H\cap R_{\text{elim}}$ 是 $J_{\text{elim}}$ 的Gröbner基 [10]。

根据定理4.3中的序关系(7)，计算全加器电路C在该序下的Gröbner基 ${H^{\prime }}_C$，然后把 ${H^{\prime }}_C$ 中关于 $g_0,g_1,g_2$ 的多项式删去，即可得出如下的多项式集合：

${H^{\prime }}_{\text{elim}}=\left\{-2c_i-s_i+a_i+b_i+c_{i-1},-s_i+4c_{i-1}{b}_i{a}_i-2c_{i-1}{a}_i+c_{i-1}-2b_i{a}_i+b_i+a_i\right\}$

由定理4.3可知 ${H^{\prime }}_{\text{elim}}$ 是 $J_{\text{elim}}$ 的Gröbner基。

同样地，对于半加器电路A也可以利用加法器重写简化Gröbner基，如图2。

Figure 2. Half-adder circuit

图2. 半加器电路

半加器电路A在逆拓扑序 $a_i<b_i<s_i<c_i$ 下的Gröbner基为：

$H_A=\left\{c_i-b_i{a}_i,s_i+2b_i{a}_i-b_i-a_i,c_i^2-c_i,s_i^2-s_i,b_i^2-b_i,a_i^2-a_i\right\}$

经过加法器重写之后的Gröbner基为：

$H_{\text{elim}}=\left\{2c_i+s_i-b_i-a_i,s_i+2b_i{a}_i-b_i-a_i\right\}$

比较加法器重写前后Gröbner基中的多项式数量可以发现，在全加器电路C中，Gröbner基的多项式数量由13变为2；在半加器电路A中，Gröbner基的多项式数量由6变为2。由此得出结论，加法器重写简化了Gröbner基，加快了验证效率。但加法器重写方法需要遍历全部变量，随着乘法器位数的增加，遍历的变量数目会急剧增多，验证效率会随之降低；另外，该方法需要借助进位变量去识别加法器，没有对乘法器的结构特点进行利用，也导致了乘法器验证的效率降低。

4.2. 散列表

针对上文提出的加法器重写方法出现的问题，本文将致力于对该方法进行优化，选择了散列表 [13] 数据结构来储存变量。

散列表又称哈希表或字典，在动态编程中常用于存储键/值(key/value)数据。散列表针对键执行一个散列计算，产生一个整数，使用这一整数找到一个桶(bucket)，然后进行取值或者设值 [14]。散列表包含多个桶，即包含多个动态数组，动态数组的数量可以根据需求进行改变，并且易于操作大量数据。当访问散列表某一结点的值时，只需取其key值，便可对应到固定的一个结点值。如果使用链表来访问某一元素，就需要遍历它前面所有的元素，消耗相对较长的时间。散列表速度很快，而且它针对任何数据都能工作，因此本文选择散列表对加法器重写方法进行优化。

4.3. 优化算法

基于散列表的优化算法是使用散列表存储乘法器电路中所有的和位输出变量 $s_0,s_1,\cdots ,s_{2n-1}$，结合电路逻辑门中输出和输入的关系，利用遍历函数增加表中的变量，根据加法器的结构特性再次遍历表中变量，搜索全加器和半加器，直到遍历结束。此算法相比之前的加法器重写方法，理论上速度更快且效率更高。

如下所示的算法1，给出了优化算法的实现过程。散列表Hashmap中不同的桶存放着不同的结点，结点HashmapNode中存放着和位输出变量vars。算法1包含如下几个步骤：1) 设置默认桶数量为1009，此值可根据和位输出变量数目灵活变动，并且声明变量hashmap；2) 为散列表hashmap分配内存，给定默认比较函数和散列函数my_hash，为了便于存储，my_hash为本文自行设计的散列函数；3) 将所有和位输出变量 $s_0,s_1,\cdots ,s_{2n-1}$ 存入hashmap中；4) 利用遍历函数Hashmap traverse以及参数里的函数指针traverse_good_cb在遍历vars时把识别为加法器的输入变量添加到hashmap中；5) 对于hashmap再次遍历，利用函数指针traverse_good_cc去搜索全加器和半加器，把识别为加法器对应的规范多项式加入Gröbner基中，将不属于加法器内部门变量的多项式也加入Gröbner基中；6) 由于变量vars数量有限，遍历过程得以终止，返回优化后的Gröbner基G，再提供给计算机代数系统进行之后的验证。

图3为2位btor乘法器电路结构图，其中 $p_{i,j}=a_i{b}_j$，接下来对该电路应用优化算法。首先利用散列函数my_hash计算 $s_0,s_1,s_2,s_3$ 的key值，同时把 $s_0,s_1,s_2,s_3$ 存入散列表hashmap中；接着对表中元素遍历，只有 $s_1,s_2$ 识别出加法器， $s_1,s_2$ 对应加法器的输入变量分别是： $p_{10}$ 和 $p_{01}$ 、 $p_{11}$ 和 $c_1$，所以将这四个变量添加到hashmap中；再次遍历hashmap中的变量 $s_0,s_1,s_2,s_3,p_{10},p_{01},p_{11},c_1$。例如，当遍历到 $s_0$ 时，未识别出加法器，把该变量的多项式加入Gröbner基；当遍历到 $s_1$ 时，识别出了半加器，把该半加器规范加入Gröbner基，并且将 $s_1$ 标记为加法器的内部变量。其余变量均以此方式进行遍历，直至遍历结束，生成优化的Gröbner基G。

Figure 3. Circuit structure diagram of 2-bit btor multiplier

图3. 2位btor乘法器电路结构图

基于散列表的优化算法针对所有和位输出变量，而非对全部变量进行遍历，并且利用加法器的结构特性去完成识别，不再利用进位变量完成识别，减少了生成Gröbner基的时间，占用的内存也同时减少，算法结构也更加清晰明了。

5. 实验结果

加法器重写方法是Gröbner基法中的一个基本策略，目前它没有可替换的方法。本文提出的算法1是对加法器重写方法的优化，需要去验证其可行性和有效性，所以将优化算法与加法器重写方法在其他条件都相同的情况下进行实验，并对比分析实验结果。实验是在具有Ubuntu 18.04.6虚拟机的笔记本电脑上完成，配置为Intel i5-6300HQ 2.30 GHz CPU和4 GB内存。实验使用的工具为AIGMULTOPOLY [7]，计算机代数系统为Mathematica和Singular。选择了两类乘法器电路进行验证，分别是：btor乘法器、sp-ar-rc乘法器。这两类乘法器输入位都是部分积，但它们的电路结构有所不同，前者是全加器和半加器以网状结构累积，后者是全加器和半加器以对角结构累积 [7]。如图4所示，给出5位btor乘法器和4位sp-ar-rc乘法器电路结构图。

Figure 4. Circuit structure diagram of 5-bit btor multiplier (left) and 4-bit sp-ar-rc multiplier (right)

图4. 5位btor乘法器(左)与4位sp-ar-rc 乘法器(右)电路结构图

实验的时间表示从开始运行代码到生成Gröbner基所花费的时长，单位为秒，时间限制为1200秒。内存的单位是MB，内存限制为3072 MB。代码及相关文件包含在文件experiments中。实验结果如表1所示。

表1给出了加法器重写方法和优化算法下的实验结果。通过对比分析可以发现，在乘法器类型且位数相同的前提下，也就是同一个乘法器下，相比于加法器重写方法，优化算法耗费了更少的时间，占用了更少的内存。进一步可以发现，随着乘法器的位数增加，时间和内存差距会更加明显。由此可以得出结论，基于散列表的优化算法加快了Gröbner基生成速度，减少了内存的使用，提升了Gröbner基的生成效率。

Table 1. Comparison of adder-rewriting method and optimization algorithm based on hash table

表1. 加法器重写方法与基于散列表的优化算法对比

6. 结束语

本文旨在基于散列表产生的算法对加法器重写方法进行优化。优化算法使用散列表存储电路中所有的和位输出变量，结合电路逻辑门中输出和输入的关系，遍历表中元素来扩充散列表，结合加法器的结构性知识，再次遍历去识别加法器。结合实验结果可知，优化算法提高了Gröbner基的生成效率，减少了内存的使用，不再依赖进位变量并且减少了遍历的变量数目，也提高了乘法器电路的验证速度和验证效率。

在未来该领域的发展中，希望本文的算法可以应用于更加复杂的乘法器架构或除法器。

NOTES

^*通讯作者。