基于多项式良性基的组合逻辑电路的等价性验证

范德会

(黑龙江工程学院 汽车与交通工程学院，黑龙江 哈尔滨 150050)

基于多项式良性基的组合逻辑电路的等价性验证

范德会

(黑龙江工程学院 汽车与交通工程学院，黑龙江 哈尔滨 150050)

虽然传统的等价性验证方法如BDD或布尔SAT等能够完成低层次的电路验证，但针对抽象层次较高的电路描述验证效率较低，基于多项式的数学方法能够从字级到位级形成统一的电路描述，为高效率地完成等价性验证提供理论依据。探讨组合逻辑电路的多项式描述方法，并以多项式理想的良性基为基础，给出一种高层次等价性验证算法，并针对多种基准电路进行实验，以验证算法的性能。

等价验证；多项式良性基；形式验证；组合逻辑电路

随着科学技术的发展，集成电路功能及其结构越来越复杂，为保证设计的正确性，在设计的早期就需要对电路的正确性进行验证，尤其在较高抽象层次上的等价性验证的需求日益突出。这是由于在设计初期越早发现问题越可以降低开发成本、减少设计周期。

目前，电路等价性验证方法主要分为两大类：图形表示以及代数表示。图形表示主要为BDD、*BMD，其在抽象层级较低的等价性验证中应用较好，但在高层次描述中受图形表示的能力及图形构造上的限制，往往验证效果不佳。与之相比，基于代数方法的等价性验证在抽象层级较高时表现出较好的效率，主要是因为高抽象层级，电路表示含有大量的字级描述，而代数方法的形式化表示更适合高层次验证。

1 组合逻辑电路多项式建模

1.1 基本算术运算

在组合逻辑电路中，常用的基本算术运算主要包括加法、减法、乘法、除法，针对这些简单的运算电路子模块，可以给出多项式表示。设X1，X2为对应运算的输入，Y为对应运算的输出。则有：

“+”运算表示为Y-(X1+X2)=0，

“-”运算表示为Y-(X1-X2)=0，

“×”运算表示为Y-X1·X2=0，

“÷”运算对于Y=X1÷X2的形式，可表示为Y·X2-X1=0且X2≠0。

1.2boole运算

用来进行逻辑运算的子模块，可考虑先完成基本逻辑运算的多项式表示，再按照子模块完成基本逻辑运算的顺序，将该子模块表示成一个多项式的形式。

数学上，一个布尔代数，必有一个对应的B=({0,1},+,·)结构，因此，有：

1)对于Y=notX1，有Y+X1-1=0，

2)Y=X1andX2， 有Y+X1·X2=0，

3)对于Y=X1orX2，通过变换,有多项式Y-X1-X2+X1·X2=0。

1.3 多路选择运算

多路选择子模块在组合逻辑电路中主要是用于连接其他相关的电路子模块，为方便，这里采用表达式Y=MUX(D,s)来表示该子模块，其中该模块的输入用D=(X0,X1,…,Xm-1)向量来描述，选通信号用s∈{0,1,…,m-1}来描述，即若s=i，有Y=Xi。该子模块的多项式表示可应用拉格朗日插值的方法给出：

1.4 比较运算

定理1[8]∀x∈R，R为实数域，有如下形式：

1)x≠0等价于∃v∈R,s.t.x·v-1=0，

2)x>0等价于∃v∈R,s.t.x·v2-1=0，

3)x<0等价于∃v∈R,s.t.x·v2+1=0，

4)x≤0等价于∃v∈R,s.t.x+v2=0，

5)x≥0等价于∃v∈R,s.t.x-v2=0.

对于Y=X1≥X2可表示为

由定理1将其表示为等价的等式形式

与

从而可表示为如下多项式集合形式

同理，其他的比较运算可类似表示出。

2 组合逻辑电路等价性验证

2.1 基本思路

组合逻辑电路在设计的不同阶段，或在不同抽象级别，或在同一电路优化前后会有不同的表示，等价性验证的主要目的就是要判定这些不同的表示是否在功能上具有一致性。

本文等价性验证的基本思路是通过第1节的讨论，将待验证的组合逻辑电路的不同表示抽象成对应不同的多项式集合，通过代数方法判定这些不同的多项式集合的零点集是否等价，进而判定多项式集合是否等价。具体的是采用多项式理想的判定方法。对多项式理想的处理有多种方法，本文采用多项式理想良性基的方法进行处理。

2.2 等价性验证算法

定义1[1]一个以多项式集PS作为基的多项式，理想Ideal(PS)的良性基定义为理想的一个基的一个自约化的多项式集合WAS，使得Ideal(WAS)=Ideal(PS)。

定义2[1]一个多项式理想Ideal(PS)的一个良性基定义为一个完备的多项式集合WB，且其是理想Ideal(PS)的一个基的收缩，且满足下述性质：对于完备的多项式集合WB中的任意一个多项式Hu和任意一个WB的次数组集CT中元素u的非乘子i，xi·Hu关于WB的N-部分为0。

定理1[1]一个多项式P属于理想ID当且仅当它关于ID的一个良性基WB的收缩约化式为0。

依据定义1、定义2与定理1给出如下等价性验证算法。

算法1 组合逻辑电路的等价验证。

输入：组合逻辑电路DataP1，DataP2。

输出：验证结果。

Function EQU (DataP1，DataP2)

{

建立DataP1对应的多项式集合PS1；

建立DataP2对应的多项式集合PS2；

计算PS1的良序基WAS1；

计算PS2的良序基WAS2；

if(WAS1=WAS2)

return YES；

else

{

for ∀p∈PS1

if(rest(p/WAS2)≠0)

return NO；

for ∀q∈PS2

if(rest(q/WAS1)≠0)

return NO；

return YES;

}

}

3 实验结果

本文验证算法基于Maple 1.0.0.2，实验平台i5 6400 2.7 GHz处理器，8 GB内存的个人计算机，采用算法1针对不同的基准电路进行实验。基准电路包括16阶累加电路(Accumulator)，MP3解码器的反走样电路(Anti-alias)[12]，Horner多项式(Horner Polynomial)[9]，16阶FIR滤波器(16thFIR filter)，8阶IIR滤波器(8thIIR filter)，离散余弦变换函数(DCT)[9]和相移键控调制器(PSK)[9]。实验结果如表1所示。

表1 基准电路实验结果

4 实验结果分析

从表1的数据可以看出，算法1能够在较短的运行时间内正确地验证相关的基准电路。 *BMD方法在验证过程中需要创建大量的描述节点。因此，对于变量幂次较低的基准电路能够建立电路的描述节点，并成功地进行电路验证，而对于变量幂次较高的基准电路，其创建描述节点会占用大量的时间，若变量幂次过高，会导致创建描述模型失败，无法验证电路功能。而ILP方法能够较好地描述字级电路，但对于电路中一些非线性模块，必须在位级上建立约束，导致约束的数量迅速膨胀，使验证效率下降。

通过以上对比讨论，本文算法对高级别抽象电路的验证时间消耗要好于*BMD与ILP。

5 结束语

集成电路设计自动化领域中，形式验证是电路抽象层级较高时常用的验证方法，而多项式理论由于其描述电路时抽象建模能力强，表示具有规范性、无歧义性，使其成为理想的电路建模工具。本文采用多项式及其理想理论，给出了高层次等价性验证的算法，实验证明其有效性，由于其强大的抽象表示能力，更适合于复杂电路的高抽象级别的验证。

[1] 吴文俊. 数学机械化[M]. 北京: 科学出版社, 2003.

[2] BRYANT R E. Graph-based algorithms for Boolean function manipulation [J]. IEEE Trans on Computers, 1986, C-35(8): 677-691.

[3] BRYANT R E, CHEN Y A. Verification of arithmetic circuits with binary moment diagrams [C]. The 32nd Design Automation Conf, San Francisco, 1995.

[4] CIESIELSKI M, KALLA P, ASKAR S. Taylor expansion diagrams: a canonical representation for verification of data flow designs [J]. IEEE Trans on Computers, 2006, 55(9): 1188-1201.

[5] GOLDBERG E I, PRASAD M R, BRAYTON R K. Using SAT for combinational equivalence checking [C]. IEEE/ ACM Design, Automation and Test in Europe Conf, Munich, 2001.

[6] 李光辉，李晓维. 基于增量可满足性的等价性检验方法[J]. 计算机学报, 2004, 27(10): 1388-1394.

[7] BRINKMANN R, DRECHSLER R. RTL-datapath verification using integer linear programming [C]. The 7th Asia and South Pacific Design Automation Conf, Bangalore, 2002.

[8] SMITH J, MICHELI G D. Polynomial circuit models for component matching in high-level synthesis [J]. IEEE Trans on VLSI Systems, 2001, 9(6): 783-800.

[9] PEYMANDOUST A, MICHELI G D. Using symbolic algebra in algorithmic level DSP synthesis [C]. The 38th Design Automation Conf, Las Vegas, 2001

[责任编辑：郝丽英]

Equivalence verification of combinational logic circuit on polynomial well-behaved bases

FAN Dehui

(College of Automobile and Traffic Engineering, Heilongjiang Institute of Technology, Harbin 150001, China)

The traditional equivalence verification methods such as BDD or Boole SAT can verify the circuits described at low-level, but those methods can not efficiently verify the circuits with high-level describing. The mathematic methods based on polynomial can give a uniform describing from bit-level to word-level which are the theory basement for efficient verification. This paper discusses a polynomial method of combinational logic circuit and gives a high-level equivalence verification method on the polynomial well-behaved bases, of which the experiment with some benchmark circuits can test the performance of this algorithm.

equivalence verification; polynomial well-behaved bases; formal verification; combinational logic circuit

10.19352/j.cnki.issn1671-4679.2017.03.008

2017-03-05

黑龙江工程学院博士基金项目(2012BJ08)

范德会(1973-),男,副教授，研究方向：集成电路设计自动化.

TW79

A

1671-4679(2017)03-0030-03