范德會

(黑龍江工程學院 汽車與交通工程學院，黑龍江 哈爾濱 150050)

基于多項式良性基的組合邏輯電路的等價性驗證

范德會

(黑龍江工程學院 汽車與交通工程學院，黑龍江 哈爾濱 150050)

雖然傳統(tǒng)的等價性驗證方法如BDD或布爾SAT等能夠完成低層次的電路驗證，但針對抽象層次較高的電路描述驗證效率較低，基于多項式的數(shù)學方法能夠從字級到位級形成統(tǒng)一的電路描述，為高效率地完成等價性驗證提供理論依據(jù)。探討組合邏輯電路的多項式描述方法，并以多項式理想的良性基為基礎(chǔ)，給出一種高層次等價性驗證算法，并針對多種基準電路進行實驗，以驗證算法的性能。

等價驗證；多項式良性基；形式驗證；組合邏輯電路

隨著科學技術(shù)的發(fā)展，集成電路功能及其結(jié)構(gòu)越來越復(fù)雜，為保證設(shè)計的正確性，在設(shè)計的早期就需要對電路的正確性進行驗證，尤其在較高抽象層次上的等價性驗證的需求日益突出。這是由于在設(shè)計初期越早發(fā)現(xiàn)問題越可以降低開發(fā)成本、減少設(shè)計周期。

目前，電路等價性驗證方法主要分為兩大類：圖形表示以及代數(shù)表示。圖形表示主要為BDD、*BMD，其在抽象層級較低的等價性驗證中應(yīng)用較好，但在高層次描述中受圖形表示的能力及圖形構(gòu)造上的限制，往往驗證效果不佳。與之相比，基于代數(shù)方法的等價性驗證在抽象層級較高時表現(xiàn)出較好的效率，主要是因為高抽象層級，電路表示含有大量的字級描述，而代數(shù)方法的形式化表示更適合高層次驗證。

1 組合邏輯電路多項式建模

1.1 基本算術(shù)運算

在組合邏輯電路中，常用的基本算術(shù)運算主要包括加法、減法、乘法、除法，針對這些簡單的運算電路子模塊，可以給出多項式表示。設(shè)X1，X2為對應(yīng)運算的輸入，Y為對應(yīng)運算的輸出。則有：

“+”運算表示為Y-(X1+X2)=0，

“-”運算表示為Y-(X1-X2)=0，

“×”運算表示為Y-X1·X2=0，

“÷”運算對于Y=X1÷X2的形式，可表示為Y·X2-X1=0且X2≠0。

1.2boole運算

用來進行邏輯運算的子模塊，可考慮先完成基本邏輯運算的多項式表示，再按照子模塊完成基本邏輯運算的順序，將該子模塊表示成一個多項式的形式。

數(shù)學上，一個布爾代數(shù)，必有一個對應(yīng)的B=({0,1},+,·)結(jié)構(gòu)，因此，有：

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

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

3)對于Y=X1orX2，通過變換,有多項式Y(jié)-X1-X2+X1·X2=0。

1.3 多路選擇運算

多路選擇子模塊在組合邏輯電路中主要是用于連接其他相關(guān)的電路子模塊，為方便，這里采用表達式Y(jié)=MUX(D,s)來表示該子模塊，其中該模塊的輸入用D=(X0,X1,…,Xm-1)向量來描述，選通信號用s∈{0,1,…,m-1}來描述，即若s=i，有Y=Xi。該子模塊的多項式表示可應(yīng)用拉格朗日插值的方法給出：

1.4 比較運算

定理1[8]?x∈R，R為實數(shù)域，有如下形式：

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 基本思路

組合邏輯電路在設(shè)計的不同階段，或在不同抽象級別，或在同一電路優(yōu)化前后會有不同的表示，等價性驗證的主要目的就是要判定這些不同的表示是否在功能上具有一致性。

本文等價性驗證的基本思路是通過第1節(jié)的討論，將待驗證的組合邏輯電路的不同表示抽象成對應(yīng)不同的多項式集合，通過代數(shù)方法判定這些不同的多項式集合的零點集是否等價，進而判定多項式集合是否等價。具體的是采用多項式理想的判定方法。對多項式理想的處理有多種方法，本文采用多項式理想良性基的方法進行處理。

2.2 等價性驗證算法

定義1[1]一個以多項式集PS作為基的多項式，理想Ideal(PS)的良性基定義為理想的一個基的一個自約化的多項式集合WAS，使得Ideal(WAS)=Ideal(PS)。

定義2[1]一個多項式理想Ideal(PS)的一個良性基定義為一個完備的多項式集合WB，且其是理想Ideal(PS)的一個基的收縮，且滿足下述性質(zhì)：對于完備的多項式集合WB中的任意一個多項式Hu和任意一個WB的次數(shù)組集CT中元素u的非乘子i，xi·Hu關(guān)于WB的N-部分為0。

定理1[1]一個多項式P屬于理想ID當且僅當它關(guān)于ID的一個良性基WB的收縮約化式為0。

依據(jù)定義1、定義2與定理1給出如下等價性驗證算法。

算法1 組合邏輯電路的等價驗證。

輸入：組合邏輯電路DataP1，DataP2。

輸出：驗證結(jié)果。

Function EQU (DataP1，DataP2)

{

建立DataP1對應(yīng)的多項式集合PS1；

建立DataP2對應(yīng)的多項式集合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 實驗結(jié)果

本文驗證算法基于Maple 1.0.0.2，實驗平臺i5 6400 2.7 GHz處理器，8 GB內(nèi)存的個人計算機，采用算法1針對不同的基準電路進行實驗?；鶞孰娐钒?6階累加電路(Accumulator)，MP3解碼器的反走樣電路(Anti-alias)[12]，Horner多項式(Horner Polynomial)[9]，16階FIR濾波器(16thFIR filter)，8階IIR濾波器(8thIIR filter)，離散余弦變換函數(shù)(DCT)[9]和相移鍵控調(diào)制器(PSK)[9]。實驗結(jié)果如表1所示。

表1 基準電路實驗結(jié)果

4 實驗結(jié)果分析

從表1的數(shù)據(jù)可以看出，算法1能夠在較短的運行時間內(nèi)正確地驗證相關(guān)的基準電路。 *BMD方法在驗證過程中需要創(chuàng)建大量的描述節(jié)點。因此，對于變量冪次較低的基準電路能夠建立電路的描述節(jié)點，并成功地進行電路驗證，而對于變量冪次較高的基準電路，其創(chuàng)建描述節(jié)點會占用大量的時間，若變量冪次過高，會導(dǎo)致創(chuàng)建描述模型失敗，無法驗證電路功能。而ILP方法能夠較好地描述字級電路，但對于電路中一些非線性模塊，必須在位級上建立約束，導(dǎo)致約束的數(shù)量迅速膨脹，使驗證效率下降。

通過以上對比討論，本文算法對高級別抽象電路的驗證時間消耗要好于*BMD與ILP。

5 結(jié)束語

集成電路設(shè)計自動化領(lǐng)域中，形式驗證是電路抽象層級較高時常用的驗證方法，而多項式理論由于其描述電路時抽象建模能力強，表示具有規(guī)范性、無歧義性，使其成為理想的電路建模工具。本文采用多項式及其理想理論，給出了高層次等價性驗證的算法，實驗證明其有效性，由于其強大的抽象表示能力，更適合于復(fù)雜電路的高抽象級別的驗證。

[1] 吳文俊. 數(shù)學機械化[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-),男,副教授，研究方向：集成電路設(shè)計自動化.

TW79

A

1671-4679(2017)03-0030-03