范德會

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

基于多項(xiàng)式良性基的組合邏輯電路的等價性驗(yàn)證

范德會

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

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

等價驗(yàn)證；多項(xiàng)式良性基；形式驗(yàn)證；組合邏輯電路

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

目前，電路等價性驗(yàn)證方法主要分為兩大類：圖形表示以及代數(shù)表示。圖形表示主要為BDD、*BMD，其在抽象層級較低的等價性驗(yàn)證中應(yīng)用較好，但在高層次描述中受圖形表示的能力及圖形構(gòu)造上的限制，往往驗(yàn)證效果不佳。與之相比，基于代數(shù)方法的等價性驗(yàn)證在抽象層級較高時表現(xiàn)出較好的效率，主要是因?yàn)楦叱橄髮蛹墸娐繁硎竞写罅康淖旨壝枋?，而代?shù)方法的形式化表示更適合高層次驗(yàn)證。

1 組合邏輯電路多項(xiàng)式建模

1.1 基本算術(shù)運(yùn)算

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

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

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

“×”運(yùn)算表示為Y-X1·X2=0，

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

1.2boole運(yùn)算

用來進(jìn)行邏輯運(yùn)算的子模塊，可考慮先完成基本邏輯運(yùn)算的多項(xiàng)式表示，再按照子模塊完成基本邏輯運(yùn)算的順序，將該子模塊表示成一個多項(xiàng)式的形式。

數(shù)學(xué)上，一個布爾代數(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，通過變換,有多項(xiàng)式Y(jié)-X1-X2+X1·X2=0。

1.3 多路選擇運(yùn)算

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

1.4 比較運(yùn)算

定理1[8]?x∈R，R為實(shí)數(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將其表示為等價的等式形式

與

從而可表示為如下多項(xiàng)式集合形式

同理，其他的比較運(yùn)算可類似表示出。

2 組合邏輯電路等價性驗(yàn)證

2.1 基本思路

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

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

2.2 等價性驗(yàn)證算法

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

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

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

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

算法1 組合邏輯電路的等價驗(yàn)證。

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

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

Function EQU (DataP1，DataP2)

{

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

建立DataP2對應(yīng)的多項(xiàng)式集合PS2；

計(jì)算PS1的良序基WAS1；

計(jì)算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 實(shí)驗(yàn)結(jié)果

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

表1 基準(zhǔn)電路實(shí)驗(yàn)結(jié)果

4 實(shí)驗(yàn)結(jié)果分析

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

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

5 結(jié)束語

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

[1] 吳文俊. 數(shù)學(xué)機(jī)械化[M]. 北京: 科學(xué)出版社, 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] 李光輝，李曉維. 基于增量可滿足性的等價性檢驗(yàn)方法[J]. 計(jì)算機(jī)學(xué)報(bào), 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

[責(zé)任編輯：郝麗英]

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

黑龍江工程學(xué)院博士基金項(xiàng)目(2012BJ08)

范德會(1973-),男,副教授，研究方向：集成電路設(shè)計(jì)自動化.

TW79

A

1671-4679(2017)03-0030-03