辽宁师范大学数学学院，辽宁 大连

收稿日期：2021年9月22日；录用日期：2021年10月15日；发布日期：2021年10月26日

摘要

当今形式化验证工具在大规模集成电路的设计过程中起着非常重要的作用。最有效的方法是以Gröbner基方法为基本原理，将乘法器电路建模为一组伪布尔多项式，通过Gröbner基来既约由多项式表示的字级规范。本文将基于Gröbner基方法，使用C++语言重新实现验证工具，将整个代码分成多个模块的形式，并利用容器类对变量进行分类存储。实验结果表明：C++语言设计的验证工具不仅可以实现成功，而且也为之后的研究提供了有利的验证工具。

关键词

Gröbner基，C++，形式化验证

Design and Implementation of Gröbner Basis Verification Multiplier

Yanying Lv, Xiaoying Zhang, Jianguo Jiang^*

School of Mathematics, Liaoning Normal University, Dalian Liaoning

Received: Sep. 22^nd, 2021; accepted: Oct. 15^th, 2021; published: Oct. 26^th, 2021

ABSTRACT

Today’s formal verification tools play a very important role in the design of large-scale integrated circuits. The most effective method is based on the Gröbner basis method. The multiplier circuit is modeled as a set of pseudo-Boolean polynomials, and the word-level specification represented by the polynomial is reduced through the Gröbner basis. This article will re-implement the verification tool based on the Gröbner base method and use the C++ language, divide the entire code into multiple modules, and use the container class to classify and store the variables. The experimental results show that the verification tool designed by C++ language can not only achieve success, but also provide a favorable verification tool for subsequent research.

Keywords:Gröbner Base, C++, Formal Verification

Copyright © 2021 by author(s) and Hans Publishers Inc.

This work is licensed under the Creative Commons Attribution International License (CC BY 4.0).

http://creativecommons.org/licenses/by/4.0/

1. 引言

验证数字电路的正确性是超大规模集成电路(VLSI)设计领域中的一个重要问题 [1]。随着工艺技术的进步，人们已经可以制造出相当复杂的电路，但这种复杂性也带来越来越多的错误。为了保证错误被及时的发现，需要对电路的正确性进行验证。但由于芯片越来越复杂，设计周期越来越短，产品竞争越来越激烈等诸多因素，导致电路验证成为VLSI设计领域内的一个瓶颈。传统的电路验证方法有动态测试法 [2]，它创建测试平台，在设计的可执行软件模型上运行这些测试。但测试平台的开发是一项漫长的过程，不仅容易出错，而且需要高昂的成本。

而当今最流行的电路验证方法是形式化验证，它利用数学方法来解决电路设计的问题。当它第一次被引入时，很少有人相信它是可行的。但现在形式化验证已在众多重大项目的各个领域中使用，不仅提高了生产力和识别棘手的极端情况错误，而且缩短了上市时间，并取得了宝贵的成果。

数字电路执行逻辑运算，这使其成为计算机和数字系统中的重要组成部分。如果电路执行算术运算，则称为算术电路。算术电路尤其是乘法器电路的验证在设计中是至关重要的一环，但即使到今天，也没有一个完美的解决方案。例如二叉判定图会出现指数级膨胀 [3]。布尔可满足性方法和可满足性模理论求解方法都无法验证更大规模的乘法器电路 [4]。使用定理证明器需要大量的手工工作和专业知识 [5]。

近几年来，基于Gröbner基理论的形式化方法受到了学术界的广泛关注与认同，并在验证整数乘法器方面已显示出非常好的结果 [6] [7]。Ritirc等人提出了逐列验证方法 [8]，该方法将问题分为几个较小的、易于计算的子问题，不需要既约整个字级规范，以此来提高验证速度。Ritirc等人并在此基础上提出了加法器重写优化 [9]，通过提取乘法器中的全加器和半加器，既约了Gröbner基，进一步加快了验证速度。

虽然已经研发出多种乘法器电路的验证工具，但都处于实验阶段，没有进入工业界。因为现在的验证工具仅仅热衷于寻找验证方法，对于验证工具的代码实现草草了之。在实现代码中，他们将上千行代码写在一个文件中，没有考虑过代码的架构，也不利于后期的开发和代码的调试。

因此，本文利用C++语言 [10] 重新实现乘法器的验证工具，相比于一个C语言编写的程序，该程序被拆分为多个模块，不仅有利于代码的调试与运行，而且为之后的优化提供了方便。其中添加了顺序容器对其进行优化，并且实现成功。

2. 验证原理

2.1. Gröbner基理论

本文主要给出Gröbner基理论的定义，其它相关定义、定理及证明可以参考 [11] [12]。

设k是数域， $k\left[X\right]$ 或 $k\left[x_1,\cdots ,x_n\right]$ 是一个多项式环。单项式常见项序有字典序、分次字典序和分次逆字典序等。单项式序可以定义出任意多项式的首项，并保证多项式除法得到的余式唯一。

定义2.1设I是 $k\left[x_1,\cdots ,x_n\right]$ 的非零理想，给定一个字典序。若存在I的有限子集 $G=\left\{g_1,\cdots ,g_m\right\}$ 满足

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

则G是I的一个Gröbner基。

理想I的Gröbner基一般不是唯一的，它与项序的选择密切相关。

2.2. 代数模型

乘法器电路具有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}$ 表示。该电路由许多逻辑门表示，其中某些门的输出可能是其它门的输入，但不允许在电路中循环 [13]。我们假设

$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}$

将门输出u与门输入 $v,w$ 用以下多项式表示：

$\begin{array}{ccc}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}$ (2.1)

电路中的所有变量均为布尔变量，为确保仅找到多项式的布尔解，我们为每个变量u添加关系式 $u\left(u-1\right)=0$，并称这种关系式为域多项式。

定义2.2设C是一个电路， $G\subseteq Q\left[X\right]$ 为包含电路C中每一个门对应的多项式(见(2.1))和输入域多项式 $a_i\left(a_i-1\right)$ 以及 $b_i\left(b_i-1\right)$ 构成的多项式集合，其中 $0\le i<n$。环 $Q\left[X\right]$ 中G生成的理想记为 $J\left(C\right)$。

定理2.1设C是一个电路，G是定义2.2中的多项式集合，给定一个字典序 ${>}_{lex}$，那么G为 $J\left(C\right)$ 的一个Gröbner基。

定义2.3设C是一个电路，如果将每个 $\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\in Q\left[X\right]$ 称为电路C的规范多项式(PCC)。

以下推论表明 $J\left(C\right)$ 包含电路C中变量之间的所有关系。

推论2.1任一多项式 $p\in \left[x_1,\cdots ,x_n\right]$，p是PPC当且仅当 $p\in J\left(C\right)$。

一个给定的字级规范适用于C，当且仅当它是理想 $J\left(C\right)$ 中的元素。因此，我们可以使用多元除法来确定理想成员。因此，验证乘法器的正确性可以归为理想成员问题。

定义2.4若

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

是一个PPC，则电路C被称为乘法器。

2.3. Gröbner基法

当G是理想 $I=\langle G\rangle =\langle g_1,\cdots ,g_m\rangle \subseteq Q\left[X\right]$ 的一个Gröbner基，多项式 $q\in Q\left[X\right]$，则 $q\in I$ 当且仅当q除以G的余式r为0。结合多元多项式除法，Gröbner基可以用来判定任意多项式是否属于该理想。

在Gröbner基方法中，SP是根据乘法器的输入和输出确定的规范多项式。例如，2位乘法器的规范多项式为 $SP=8S\left[3\right]+4S\left[2\right]+2S\left[1\right]+S\left[0\right]-\left(2A\left[1\right]+A\left[0\right]\right)\left(2B\left[1\right]+B\left[0\right]\right)$，其中 $8S\left[3\right]+4S\left[2\right]+2S\left[1\right]+S\left[0\right]$ 表示2位乘法器的输出，而 $\left(2A\left[1\right]+A\left[0\right]\right)\left(2B\left[1\right]+B\left[0\right]\right)$ 表示2位乘法器的输入。

Gröbner基方法的一般思想：

1) 将乘法器中变量之间的关系生成一个Gröbner基 $G=\left\{g_1,\cdots ,g_m\right\}$，并将乘法器的输入和输出表示为规范多项式SP。

2) 将G中的多项式代入SP中或G对SP进行逐步除法(称为向后重写)，余式为r。

3) 如果SP为零或 $r=0$，则乘法器是正确的；否则，乘法器是错误的。

3. 架构设计

3.1. 需求分析

验证电路的正确性在设计领域是非常重要的，正确的电路设计可避免因重新设计浪费开发成本和设计周期。对于任意给定的乘法器，验证工具都应读取输入文件掌握乘法器的结构，并通过遍历乘法器的节点变量给出需要的信息，最后得出输出文件。但由于大乘法器的结构复杂，在验证乘法器的过程中，可能导致验证失败，因此，验证工具不仅需要正确的验证乘法器，而且还应该具有优化等功能，进一步提高验证速度以及验证更大的乘法器。

图1. 验证工具的流程图

图2. 验证工具的总体架构

3.2. 总体架构

验证工具是为了满足乘法器验证的需求而设计的，该验证工具的目标是将Gröbner基方法与形式化验证相结合，最终完成一个独特的、能够解决乘法器正确性问题和满足实际需求的验证工具。

根据需求分析，验证工具应具备以下功能：

1) 可以读取输入文件；

2) 可选择进行的操作；

3) 能直观的给出节点的相关信息；

4) 具有优化功能，可以提高验证速度；

5) 可以验证乘法器的正确性。

形式化验证主要是将乘法器建模为多项式，利用Gröbner基方法既约规范多项式，当既约结果为零时，则乘法器是正确的，否则是错误的。根据验证工具的需求分析，给出验证工具的一般工作流程：首先选择代数系统，随后读取AIG文件 [14]。针对AIG文件中的变量文字，确定输入、输出变量及与门节点信息。根据节点排列位置，对乘法器进行切片优化，并将切片中对应的门多项式打印到可计算文件中。如果选择了加法器重写优化，则需要查找乘法器中所包含的加法器和半加器，将全加器和半加器的规范多项式及其他门多项式打印到可计算文件中。最后将可计算文件传递给代数系统Mathematica [15] 和Singular [16] 进行计算，如果计算结果为零，则乘法器是正确的，否则是错误的，进而验证乘法器的正确性。验证工具的工作流程如图1所示。

结合验证工具的工作流程，设计了验证工具的总体架构。如图2所示，包括解析器、优化策略和代数系统。解析器实现读取AIG文件并确定输入序；将输入、输出和中间变量进行标记，并为其命名；通过遍历节点，给出所有节点的层次关系。优化策略包括切片优化、加法器重写优化和容器类优化，是验证工具的核心，对验证工具进行优化可提高验证速度，是验证乘法器中重要的一环。代数系统将全部门多项式打印到可计算文件中，如果进行了加法器重写，将全加器和半加器的规范多项式打印到可计算文件中；随后将可计算文件传递给代数系统进行计算，进而得出计算结果。

4. 模块的设计与实现

本文的验证工具将采用C++语言开发，因为虽然C语言的运行速度比较快，但当验证工具的代码达到一定长度时，很容易崩溃。而Python是一种脚本语言 [17]，简单易学，但机器运行时间很长。Java代码需由Java虚拟机读取运行，所以效率偏低 [18]。而C++语言不仅拥有计算机高效运行的实用性特征，同时还致力于提高大规模程序的编程质量，在核心的功能和需要大量代码运行的部分更倾向于选择C++语言，并且在验证乘法器方面也更倾向于用C++语言进行编译。下面将给出各模块的设计与实现。

4.1. 解析器

与非图(And-Inverter-Graphs)是电路的常见表示，也称为AIG。它是由表示逻辑与的两个输入节点组成的有向无环图，边可以包含指示逻辑否定的标记，每个节点的语义蕴含了多项式关系。通过多个AIG描述电路形成AIGER格式，也就是AIG文件。解析器应实现AIG文件的读取和处理，包括3方面功能：读取AIG文件、确定输入序和给出基础信息。

AIG文件具有ASCII和二进制两种版本，通常以带有“aag”标头的ASCII格式进行查看。在ASCII格式的AIG文件中，列出了输入、输出以及与门的文字表示，获取文字的符号位需将其无符号整数表示取模2，符号位为1表示取反，符号位为0表示取正。因此，如果与门右侧的文字为奇数，则符号位为1，表示取反。而读取AIG文件需要确定文字之间的联系，其中与门是由三个正整数组成，第一个整数是偶数，代表文字或与门左侧(LHS)，另外两个整数表示“与”门右侧(RHS)的文字。通过AIG文件给出的输入，确定输入序，进而判断乘法器的基准类型。本文主要验证由boolector基准生成的“btor”乘法器和由AOKI基准生成的“sp-ar-rc”乘法器，因此需要进行判断。读取AIG文件和确定输入序等功能通过parser_aig()和determine_input_order()函数实现，如表1所示。

通过遍历AIG文件中的每个节点，掌握乘法器的结构，并针对需要的功能进行设计。实现基础功能为后续的设计打下坚实的基础。遍历全部节点时，为该节点的变量赋予唯一的名字和文字，并确定变量是否是输入、输出变量。而且每个节点在乘法器中的层次是固定的，通过节点所在层次，可以确定节点所在位置，为后续尽快找到该节点提供了基础。乘法器中应当有很多的异或门，给出一个节点如何判断该节点是否是异或门是一个关键。在运行验证工具时，给出运行的时间和内存，当出现错误时，给出错误说明也是很有必要的。这些功能在此验证工具中都已经实现。

表1. 解析器的部分函数实现

4.2. 优化策略

一个验证工具不仅要能正常运行，而且在速度上也有一定的需求。在验证大的乘法器时，常常因为乘法器过大，导致运行时间过长，进而验证失败。因此，验证工具的运行效率也是一个值得重视并为之付出努力的问题，其性能的优化也是一门复杂的学问。

首先，对乘法器进行切片优化，将一个大的乘法器问题分为更小更易于解决的子问题，逐步验证这些子问题进而验证整个乘法器，该方法也被称为逐位验证方法。如图3所示，是一个3位乘法器的结构图，按输出位开始，将每一个输出划分为一个切片。因此，在Gröbner基方法的基础上，该方法将Gröbner基G重写为变量较少的切片Gröbner基 $G_i$。通过 $G_i$ 对 $S{P}_i$ 进行逐步除法，将得到的余式 $r_i$ 添加到下一个切片Gröbner基 $G_i$ 中，重复此操作。如果最后得到的余式为零，则乘法器是正确的，否则是错误的。

图3. 3位乘法器的逐位验证方法示意图

其次，由于在遍历变量时，每次都需要从第一个变量进行遍历直到最后一个变量，其中包含许多无效变量，减慢了验证速度。因此本文利用C++命名空间中的顺序容器类对乘法器中的变量和文字进行分类存储，以便更快的找到符合条件的变量。vector容器相当于动态数组，它的随机访问效率高；list容器相当于列表，它的插入和删除效率高。因此我们将vector和list结合起来，实现变量随机存储的最佳状态。利用vector和list创建一个二维数组，list容器对象有一个push_back()成员函数，用于在list容器的最尾部中插入元素使用。通过此函数成员，在traverse_column()函数中完成对slices的赋值，即返回各个切片中包含的变量。例如std::vector > slices。表2中给出了相关函数的实现。

最后，通过图3可以发现该乘法器是完全由半加器和全加器组成的，因此，可以对其进行加法器重写。找到乘法器电路门级表示中的全加器和半加器，并把它们视为独立的电路。利用全加器和半加器的规范表示消去内部门多项式，使乘法器的Gröbner基更小、更紧凑，从而加快约化过程。下面给出全加器和半加器的规范多项式以及结构图，如图4所示。

定义4.1给定输出 $c,s$ 和输入 $a,b,i$。如果 $-2c-s+a+b+i$ 是一个PCC，则电路C称为全加器。如果 $-2c-s+a+b$ 是一个PCC，则电路C称为半加器。

图4. 全加器(左)和半加器(右)的结构图

寻找乘法器中的全加器需要确定进位变量，表2给出了寻找进位变量的函数实现。在函数collect_carry()中，将切片中的进位变量赋给数组carry[k]，以便在寻找全加器时，直接从数组carry[k]中的变量进行遍历。确定了进位变量之后，通过进位变量的位置找到全加器的其他变量，进而找到乘法器电路中的全部全加器和半加器，其函数实现在表2中给出。

表2. 优化策略的部分函数实现

4.3. 代数系统

根据选择的优化方法和代数系统，进行综合运行，输出一个可计算文件。该文件需要传递给代数系统进行计算，得出验证结果。因此，输出的计算文件是至关重要的。首先，通过解析器找到乘法器中的与门、或门、非门和异或门，通过电路建模将乘法器中的所有门用多项式进行表示。在表3中，实现了一个具有这样功能的函数。由于代数系统Mathematica和Singular的计算方式不同，需要其他的辅助多项式。因此，在表3中实现了一个函数print_slice()，它将各个切片中的辅助多项式打印在计算文件中，并将两个切片之间的联系，通过余多项式进行了连接，使得验证正确的乘法器时，最后余式为零。不仅如此，当进行加法器重写优化时，需将乘法器中的全加器和半加器都用规范多项式表示，并打印到可计算文件中。当打印全部完成，将该文件生成代数系统的可计算文件，随后传递给Mathematica或Singular进行计算。

表3. 代数系统的部分函数实现

4.4. 实验结果

在实验中，本文使用了具有2n个输出位和两个大小为n的输入位向量的整数乘法器。使用了与 [9] 相同的乘法器类型“btor”乘法器和“sp-ar-rc”乘法器。

本次实验使用了一台带有Ubuntu18.04虚拟机的电脑，配备Intel i5-6200U 2.3GHz CPU和4GB主内存。并将时间限制为1200秒，主内存限制为4GB，并且时间都以秒为单位。我们从启动验证工具AIGMULTOPOLY开始计算到Mathematica或Singular完成计算为止，所包含的时间为验证工具生成Mathematica和Singular计算文件所需的时间和使用计算机代数系统计算的时间。本次实验选择Mathematica作为代数系统进行计算，其中n表示乘法器的位数，AR表示加法器重写。实验结果如下表(见表4)所示：

表4. 验证工具的实现

如表4所示，验证16~128位乘法器时，利用C++语言重新实现乘法器的验证工具可以对乘法器进行验证，通过得出可计算文件，将其传递给代数系统进行计算，得出总体验证时间。并且本文的验证工具使用模块的形式，使程序更简单易读，代码的运行与调试也是更方便了。由于C++语言编程的多样性，我们将来应该进一步优化验证工具和代数系统以提高乘法器的验证效率。但由于计算机的不同，软件版本的不同，得出的结果具有差异性。实验结果表明：通过C++语言实现的验证工具比C语言实现的验证工具更具有可读性和可行性，并为后期验证乘法器提供了更好的平台。

5. 结论

本文基于Gröbner基的验证原理，通过C++语言重新实现了乘法器的验证工具，并通过验证工具读取AIG文件，得出可传递到Mathematica或Singular计算的文件。不仅将整个繁琐的C语言代码整理成多文件的形式，使程序调试起来方便，也为后续验证乘法器提供了一个不错的工具。而且利用C++命名空间中的顺序容器类对代码进行了优化，并且可以正确地实现出来。

使用验证工具和代数系统可以有效验证简单的乘法器，而更复杂和优化的乘法器还需要更复杂的方法。在以后的工作中，我们希望将该方法扩展到浮点运算符，甚至扩展到更具挑战性的乘法器体系结构和其他算术电路。

文章引用

吕妍颖,张小盈,江建国. GrO^¨bner基法验证乘法器的设计与实现
Design and Implementation of GrO^¨bner Basis Verification Multiplier[J]. 应用数学进展, 2021, 10(10): 3495-3504. https://doi.org/10.12677/AAM.2021.1010369

参考文献