可滿足模理論在軟硬件劃分領(lǐng)域的應(yīng)用*

毛樂樂,胡小勤,盧　晨

(廣西民族大學(xué),a.廣西混雜計(jì)算與集成電路設(shè)計(jì)分析重點(diǎn)實(shí)驗(yàn)室；

b.信息科學(xué)與工程學(xué)院，廣西 南寧 530006)

?

可滿足模理論在軟硬件劃分領(lǐng)域的應(yīng)用*

毛樂樂a,胡小勤a,盧晨b

(廣西民族大學(xué),a.廣西混雜計(jì)算與集成電路設(shè)計(jì)分析重點(diǎn)實(shí)驗(yàn)室；

b.信息科學(xué)與工程學(xué)院，廣西 南寧 530006)

摘要：軟硬件劃分是評(píng)價(jià)軟硬件協(xié)同設(shè)計(jì)優(yōu)劣，甚至影響設(shè)計(jì)成敗的關(guān)鍵技術(shù)之一.文章首次將可滿足模理論應(yīng)用于軟硬件劃分問題，借助Z3、CVC4與MathSAT5可滿足問題解決器求得最優(yōu)的軟硬件劃分方案，使得系統(tǒng)的軟硬件實(shí)現(xiàn)代價(jià)最小，經(jīng)實(shí)驗(yàn)驗(yàn)證，針對(duì)軟硬件劃分問題，Z3的綜合性能要優(yōu)于另外兩種解決器.采用可滿足性問題求解方案，不僅克服了傳統(tǒng)啟發(fā)式算法陷入局部最優(yōu)解的弊端，同時(shí)也彌補(bǔ)了規(guī)劃類算法不適應(yīng)于大規(guī)模劃分問題的不足.

關(guān)鍵詞：軟硬件協(xié)同設(shè)計(jì)；軟硬件劃分；可滿足模理論；可滿足模理論求解器

0引言

在傳統(tǒng)的芯片設(shè)計(jì)中，工程師一般是憑經(jīng)驗(yàn)進(jìn)行軟硬件劃分，但隨著電子技術(shù)的發(fā)展，嵌入式的系統(tǒng)設(shè)計(jì)變得越來越復(fù)雜，設(shè)計(jì)周期要求越來越短，性能控制也要求越來越高，僅憑經(jīng)驗(yàn)已經(jīng)無法滿足設(shè)計(jì)周期，性能控制的要求，而且系統(tǒng)的軟硬件劃分結(jié)果直接影響著后續(xù)的軟硬件協(xié)同設(shè)計(jì)，因此軟硬件劃分技術(shù)成為當(dāng)前信息領(lǐng)域的研究熱點(diǎn)之一.系統(tǒng)的硬件與軟件都有各自的優(yōu)缺點(diǎn)，硬件執(zhí)行速度快成本較高的特點(diǎn)與軟件執(zhí)行速度較慢成本卻相對(duì)較低的特點(diǎn)互補(bǔ)，因此嵌入式系統(tǒng)可以分別交由軟件和硬件實(shí)現(xiàn)，其中關(guān)鍵部分交由硬件實(shí)現(xiàn)，非關(guān)鍵部分交由軟件實(shí)現(xiàn).通過此方法可以將系統(tǒng)功能行為最優(yōu)地分配到軟硬件系統(tǒng)結(jié)構(gòu)上.因此目前大部分嵌入式系統(tǒng)都要經(jīng)過軟硬件劃分以獲得高性能、低成本的優(yōu)化效果.

國外從20世紀(jì)90年代開始探索軟硬件劃分方法, 在初期研究者將整數(shù)線性規(guī)劃等規(guī)劃類方法應(yīng)用于軟硬件劃分并進(jìn)行求解.文獻(xiàn)[1-2]提出應(yīng)用貪婪算法實(shí)現(xiàn).文獻(xiàn)[3]提出將所有的系統(tǒng)任務(wù)節(jié)點(diǎn)首先映射到將系統(tǒng)功能實(shí)現(xiàn)從全硬件功能逐步劃分到軟件功能軟件，然后將部分任務(wù)節(jié)點(diǎn)逐步映射到硬件的方法實(shí)現(xiàn)軟硬件劃分.但是應(yīng)用于軟硬件劃分問題的規(guī)劃類算法執(zhí)行時(shí)間較長，一般適用于較小規(guī)模的軟硬件劃分問題，當(dāng)問題規(guī)模較大時(shí)，并不適用并且全局搜索能力較差.2000年，國內(nèi)開始著手解決軟硬件劃分問題的相關(guān)研究，為了更好地解決軟硬件劃分問題，國內(nèi)學(xué)者也在不斷嘗試，不斷探索，2002年劉功杰等人提出遺傳算法(GA)[4]的軟硬件劃分算法，2004年鄒誼等人將量子遺傳算法(QGA)[5]應(yīng)用到軟硬件劃分;2007年郭榮華等人提出混合量子遺傳算法(HQGA)[6]用于求解大模的系統(tǒng)軟硬件劃分問題;2010年，劉安等人將遺傳算子引入到粒子群優(yōu)化算法(PSO)[7]中應(yīng)用于軟硬件劃分.上述提出的軟硬件劃分算法較復(fù)雜，運(yùn)行時(shí)間較長, 而且傳統(tǒng)啟發(fā)式算法建模相對(duì)復(fù)雜，同時(shí)還有一個(gè)共同的弊端：容易陷入局部最優(yōu).

文章首次將軟硬件劃分問題轉(zhuǎn)化為SMT問題，即將可滿足模理論應(yīng)用到軟硬件劃分問題并借助可滿足問題解決器Z3、CVC4與MathSAT5解決器求得最優(yōu)的軟硬件劃分方案，使得系統(tǒng)的軟硬件實(shí)現(xiàn)代價(jià)最小.利用可滿足模理論不僅克服了傳統(tǒng)啟發(fā)式算法陷入局部最優(yōu)解的弊端，同時(shí)也彌補(bǔ)了規(guī)劃類算法不適應(yīng)于大規(guī)模劃分問題的不足.而且應(yīng)用表現(xiàn)優(yōu)秀的SMT解決器,建立的軟硬件劃分模型也相對(duì)簡單.通過對(duì)比三種SMT解決器執(zhí)行相同變量求得全局最優(yōu)解的時(shí)間以及軟硬件的實(shí)現(xiàn)代價(jià),得出Z3的綜合性能要優(yōu)于另外兩種解決器，劃分問題規(guī)模越大，效果越明顯.這篇文章從新角度嘗試探索解決軟硬件劃分問題的新途徑.

1軟硬件劃分問題的描述與數(shù)學(xué)模型

軟硬件劃分是軟硬件協(xié)同設(shè)計(jì)的重要環(huán)節(jié)和組成部分，其主要任務(wù)是在滿足各項(xiàng)設(shè)計(jì)約束的條件下，把系統(tǒng)功能劃分到目標(biāo)結(jié)構(gòu)中的軟件和硬件部分上，并為系統(tǒng)提供最佳的軟硬件劃分方案.

這篇文章利用可滿足模理論在短時(shí)間內(nèi)生成一套執(zhí)行時(shí)間少，系統(tǒng)總代價(jià)小的高質(zhì)量劃分方案.

求解軟硬件劃分問題時(shí)，通常使用無向圖來描述任務(wù)流圖.

定義1R={R0,R1,…,Rn}代表劃分系統(tǒng)的所有任務(wù)節(jié)點(diǎn)集合,其中Ri表示第i個(gè)任務(wù)節(jié)點(diǎn)，其中i=0,1,2,…,n.圖中的一個(gè)節(jié)點(diǎn)就是對(duì)應(yīng)劃分系統(tǒng)的一個(gè)任務(wù)，每個(gè)節(jié)點(diǎn)包含其軟件、硬件代價(jià)信息,例如采用硬件時(shí)的運(yùn)行時(shí)間和采用軟件時(shí)在處理器上執(zhí)行時(shí)間.

定義2系統(tǒng)總代價(jià)由軟件代價(jià)和硬件代價(jià)組成，即系統(tǒng)總代價(jià)為軟件代價(jià)與硬件代價(jià)之和，第m次劃分后系統(tǒng)總代價(jià)用Vm+1表示，其中m=0,1,…,n.即沒有進(jìn)行劃分時(shí)系統(tǒng)總代價(jià)為V1，第一次劃分后的系統(tǒng)總代價(jià)為V2，系統(tǒng)每進(jìn)行一次劃分便得到一次優(yōu)化，系統(tǒng)總代價(jià)將減小，因此V2≤V1.

定義3軟硬件劃分問題中我們可以得出x=(x0,x1,x2,…,xn)是劃分系統(tǒng)任務(wù)流圖的一個(gè)可行解，代表對(duì)系統(tǒng)的一種劃分，xi{0,1}，xi=1代表Ri由軟件實(shí)現(xiàn)，xi=0代表Ri由硬件實(shí)現(xiàn)，其中i代表第i個(gè)節(jié)點(diǎn), i=0,1,2,…,n.

定義4 軟件代價(jià)si是在[0,10]中隨機(jī)產(chǎn)生并服從均勻分布，硬件代價(jià)hi是在[0 ,10]中隨機(jī)產(chǎn)生服從均勻分布，其中i=0,1,2,…,n.

1.1軟硬件劃分問題定義

軟硬件劃分實(shí)質(zhì)是對(duì)節(jié)點(diǎn)集合做劃分，即將原節(jié)點(diǎn)集合R={R0,R1,…,Rn}劃分為兩個(gè)子集，即Q=(Rh,RS)，其中Rh∪RS=R且Rh∩RS=Φ.

軟硬件劃分問題：在滿足性能約束的條件下，將一個(gè)節(jié)點(diǎn)集合R劃分，分別映射到軟件和硬件實(shí)現(xiàn)，映射到軟件實(shí)現(xiàn)需要消耗軟件代價(jià)，同理映射到硬件實(shí)現(xiàn)需要消耗硬件代價(jià)，劃分后的系統(tǒng)硬件代價(jià)和軟件代價(jià)的形式化定義分別為式(1),式(2).

HR=∑Ri∈Rhhi

(1)

式中，hi，si分別表示第i個(gè)節(jié)點(diǎn)交由硬件實(shí)現(xiàn)或軟件實(shí)現(xiàn)所消耗的代價(jià).

SR=∑Ri∈RSsi

(2)

給定軟件代價(jià)函數(shù),硬件代價(jià)函數(shù),以及約束Vm+1，由于軟硬件代價(jià)大于零，所以Vm+1>0，求解一種軟硬件劃分，使得系統(tǒng)的開銷最小.

用x=(x0,x1,x2,…,xn)表示一個(gè)劃分即劃分系統(tǒng)任務(wù)流圖的一個(gè)可行解，xi=1代表Ri由軟件實(shí)現(xiàn)，xi=0代表Ri由硬件實(shí)現(xiàn)，則系統(tǒng)的軟件代價(jià)和硬件代價(jià)可分別表示為式(3)，式(4).

(3)

(4)

在第m次軟硬件劃分后，滿足

S(x)+ H(x)

(5)

即

(6)

軟硬件劃分問題：在滿足性能約束的條件下，將一個(gè)節(jié)點(diǎn)集合R={R0,R1,…,Rn}進(jìn)行劃分，分別映射到軟件和硬件實(shí)現(xiàn)，系統(tǒng)的軟硬件劃分完成后可以使得系統(tǒng)的軟硬件代價(jià)最小，整個(gè)問題轉(zhuǎn)化成規(guī)劃問題：

目標(biāo)函數(shù)MinCost(x)

約束函數(shù)Cost(x)

系統(tǒng)經(jīng)過每一次軟硬件劃分后，都會(huì)產(chǎn)生一個(gè)新的系統(tǒng)代價(jià)，并且新的系統(tǒng)代價(jià)要比上一次的系統(tǒng)代價(jià)小.若進(jìn)行m次劃分后的系統(tǒng)總代價(jià)用Vm+1表示，則Vm+2≤Vm+1，如此不斷劃分尋找滿足條件的最小值Vm+1.

1.2基于SMT的軟硬件劃分模型

可滿足性理論(SatisfiabilityModuloTheories,SMT)是布爾可滿足問題的擴(kuò)展，它是對(duì)多類型一階邏輯公式進(jìn)行可滿足性判定的理論.

假設(shè)要進(jìn)行判定的SMT公式如下：

φ∶=(x1∧x2)∨x3

(7)

若x1,x2,x3為布爾量用SMT-LIB[8]標(biāo)準(zhǔn)語言描述公式φ，有smt2文件：

(declare-constx1Int)

(declare-constx2Int)

(declare-constx3Int)

(assert(or(= x10) (= x11)))

(assert(or(= x20) (= x21)))

(assert(or(= x30) (= x31)))

(assert(or(andx1x2) x3))

(check-sat)

(get-value(x1x2x3))

將此smt2文件作為SMT解決器的輸入?yún)?shù)，經(jīng)過SMT解決器處理后可以判斷出SMT公式是可滿足的還是不可滿足的，以及輸出當(dāng)公式可滿足時(shí)x1,x2,x3的值.

因此我們要將軟硬件劃分問題轉(zhuǎn)化為SMT問題，必須將軟硬件劃分模型形式化為smt2文件形式.

將軟硬件劃分問題轉(zhuǎn)化為SMT問題分為以下幾個(gè)步驟：

第一步：在軟硬件劃分中將原節(jié)點(diǎn)集合R={R0,R1,…,Rn}劃分為兩個(gè)子集，即Q=(Rh,RS)，其中Rh∪RS=R且Rh∩RS=Φ，x=(x0,x1,x2,x3,…,xn)是劃分系統(tǒng)任務(wù)流圖的一個(gè)可行解，整數(shù)xi為1或?yàn)?，當(dāng)xi=1時(shí)代表Ri交由軟件實(shí)現(xiàn)，xi=0時(shí)代表Ri交由硬件實(shí)現(xiàn)，即將系統(tǒng)劃分為軟硬件兩部分.

將原節(jié)點(diǎn)集合劃分問題轉(zhuǎn)化成SMT問題即用SMT-LIB標(biāo)準(zhǔn)語言描述得下式：

(declare-constxiInt)

(8)

(assert(or(= xi0) (= xi1)))

(9)

即將第i個(gè)節(jié)點(diǎn)交由軟件或硬件實(shí)現(xiàn).將軟硬件劃分中約束函數(shù)

轉(zhuǎn)化成SMT問題描述如下：

(assert(<(+ (* xisi) (* (- 1 xi) hi)) Vm+1))

(10)

SMT-LIB描述幾個(gè)最基本的理論有抽象函數(shù)等式，線性算數(shù)，差分邏輯，位向量以及數(shù)組等，這篇文章應(yīng)用到線性算數(shù)理論.

線性算數(shù)(LinearArithmetic,LA)是算數(shù)函數(shù)只有“+”“-”的理論，謂詞符號(hào)一般只有(=、≤、<)，只允許數(shù)與變量的乘法，如整數(shù)的3·x，在實(shí)數(shù)上也允許分子形式的數(shù)乘，根據(jù)處理的類型不同可以分為整數(shù)上和實(shí)數(shù)上的LA理論.LA公式的一般形式為：

X1+3X2≤6X3

(11)

在smt2文件中LA理論應(yīng)用于

(assert(<(+ (* xisi) (* (- 1 xi) hi)) Vm+1) )

第二步：分別調(diào)用Z3、CVC4、MathSAT5解決器處理并判斷公式(10)是可滿足的還是不可滿足的，并在可滿足時(shí)輸出一組x=(x0,x1,x2,…,xn).

將此組x=(x0,x1,x2,…,xn)帶入公式(12):

(assert(=(+ (* xisi) (* (- 1 xi) hi)) Vm+2)

(12)

可以得到一個(gè)新的軟硬件代價(jià)Vm+2.

第三步：重復(fù)執(zhí)行第二步驟，直至不可滿足時(shí)，停止迭代，則在不可滿足的情況下之前的一組x=(x0,x1,x2,…,xn)即為全局最優(yōu)解.

1.3求解過程

基于SMT軟硬件劃分的偽代碼如下：

Init( h, s,v1, v2);

result1=result2=z3(h, s, v2);

while(1)

{

result1=result2;

result2=output(z3);

v1=v2;

v2=new_v(r2, h, s);

if(result2.sat= =1)

{

z3(h, s, v2);

}

if(result2.sat==0)

{

break;

}

}

Record result1;

首先初始化軟硬件代價(jià)系數(shù)h，s和總代價(jià)v1，v2.然后生成z3的輸入文件，調(diào)用z3，求得新的劃分，將劃分的結(jié)果保存到result1和result2中.其中v1表示前一個(gè)劃分下的軟硬件代價(jià)的總和，v2表示當(dāng)前劃分下的軟硬件代價(jià)的總和.result1表示前一個(gè)劃分的結(jié)果，result2表示當(dāng)前劃分的結(jié)果.接著循環(huán)調(diào)用z3直到result2不可滿足時(shí)，result1即為所求得的劃分結(jié)果.

2仿真實(shí)例與分析

操作系統(tǒng)：64位centos 6.3，CPU：Intel(R)Core(TM)i5-3470，RAM：12.00 GB.

所使用的編程語言：C++,gccg++.

運(yùn)用的SMT解決器:Z3、CVC4、Mathsat5.

Z3[9]是微軟公司研發(fā)的一個(gè)高效、可擴(kuò)展與表達(dá)性強(qiáng)的SMT求解器.曾在SMT-COMP競賽中表現(xiàn)不俗，是到目前為止綜合求解能力最強(qiáng)的SMT求解器.

CVC是由紐約大學(xué)和愛荷華大學(xué)共同領(lǐng)導(dǎo)開發(fā)，具有給出證明和模型的推導(dǎo)能力等優(yōu)點(diǎn).最新的CVC系列的解決器是CVC4.

MathSAT是由FBK(Fondazione Bruno Kessler)和特倫托大學(xué)聯(lián)合研發(fā)，MathSAT的DPLL的引擎是基于一個(gè)高效的SAT解決器.最新MathSAT系列的解決器是MathSAT5.

以節(jié)點(diǎn)為4為例,即i=4得約束函數(shù)公式：

s0*x0+h0*(1-x0)+s1*x1+h1*(1-x1)+s2*x2+h2*(1-x2)+s3*x3+h3*(1-x3)

(13)

用SMT-LIB標(biāo)準(zhǔn)語言描述公式(13),即將軟硬件劃分問題轉(zhuǎn)化為SMT問題建立模型如下:

(declare-constx0Int)

(declare-constx1Int)

(declare-constx2Int)

(declare-constx3Int)

(assert(or(= x00) (= x01)))

(assert(or(= x10) (= x11)))

(assert(or(= x20) (= x21)))

(assert(or(= x30) (= x31)))

(assert(<(+ (+ (+ (+ (+ (+ (+(* x0

3.85) (* (- 1 x0) 4.32)) (* x13.63)) (*

(- 1 x1) 1.13)) (* x21.74)) (* (- 1 x2)1.9))

(* x31.75)) (* (- 1 x3) 1.09)) 17.6) )

(check-sat)

(get-value (x0x1x2x3))

此Benchmarks是SMT-LIB用于比較各SMT解決器的求解效率而編寫的用例，隨后調(diào)用Z3求解得x0=0,x1=1,x2=0和x3=0.執(zhí)行時(shí)間為0.356523 s，系統(tǒng)軟硬件代價(jià)為14.6.此外我們還作了大量的實(shí)例分析，部分結(jié)果如表1所示.

對(duì)比表1中的統(tǒng)計(jì)數(shù)據(jù)可以得出，調(diào)用MathSAT解決器在變量為0～15范圍內(nèi)比Z3和CVC4解決器較快.調(diào)用Z3解決器在變量為15～178范圍內(nèi)比MathSAT5、CVC4較快，系統(tǒng)的軟硬件實(shí)現(xiàn)總代價(jià)較小.CVC4解決器在各變量范圍內(nèi)執(zhí)行時(shí)間最長，系統(tǒng)的軟硬件實(shí)現(xiàn)代價(jià)最大.Z3在這篇文章的測(cè)試中具有時(shí)間開銷小，系統(tǒng)軟硬件開銷小的性能特點(diǎn)，具有較強(qiáng)的求解實(shí)力，CVC4在求解可滿足解時(shí)求解能力欠佳，MathSAT5在求解不可滿足解時(shí)求解能力欠佳.

表1　實(shí)驗(yàn)結(jié)果

3結(jié)語

文章首次將可滿足模理論應(yīng)用于軟硬件劃分問題，并借助SMT解決器Z3、CVC4與MathSAT5求得最優(yōu)的軟硬件劃分方案，使得軟硬件實(shí)現(xiàn)代價(jià)最小.實(shí)驗(yàn)證明文中提出的方法是有效可行的，為研究軟硬件劃分問題提供了新的思路，同時(shí)證明Z3的綜合性能是最好的.但是隨著嵌入式系統(tǒng)的軟硬件設(shè)計(jì)越來越復(fù)雜，在軟硬件劃分研究中將迎來更多挑戰(zhàn)，需進(jìn)一步完善可滿足理論在軟硬件劃分問題上的應(yīng)用，增加更多的參數(shù)到軟硬件劃分，例如通信代價(jià)等.

[參考文獻(xiàn)]

[1]R. K. Gupta.Co-synthesis of hardware and software for digital embedded systems[D].PhDthesis,Stanford University, December 1993.

[2]P.Arato,S.Juhasz,Z.A.Mann.Hardware-software partitioningin embedded system design[A].WISP2003, Budapest,Hungary,September，2003:197-222.

[3]R.Ernst,J.Henkel,T.Benner.Hardware-softwarecosynt-hesis for microcontrollers[J].IEEE Design Test Comput，1993,10(4):64-75.

[4]G.Liu,L.Zhang,S.Li.Genetic algorithm inhardware/software partitioningapplications[J].Journal of National University of Defense Technology，2002, 24(2):64-68.

[5] 鄒誼，莊鎮(zhèn)泉，李斌.基于量子遺傳算法的嵌入式系統(tǒng)軟硬件劃分算法[J].電路與系統(tǒng)學(xué)報(bào),2004,9(5):1-7.

[6]R.Guo,B.Li,Y.Zou,Z.Zhuang.Hybrid quanturnprobabilistic coding genetic algorithm forlargescale hardware-software co-synthesis of embedded system [J].IEEE Congress on Evolutionary Computation,2007:3454-3458.

[7]A.Liu,J.Feng,X.Liang,X.Yang.Based on Geneticparticleswarm optimization of embedded system hardware-software partitioningalgorith[J].Journal of computer aided design and graphis,2010,22(6):927 -933.

[8]The Satisfiability ModuloTheories Library[EB/OL]. http://www.smt-lib.org/.

[9]Project Hosting For Open Source Software[EB/OL]. http://z3.codeplex.com/.

[責(zé)任編輯蘇琴]

[責(zé)任校對(duì)黃招揚(yáng)]

A Satisfiability Modulo Theories Method For Software And Hardware Division

MAO Le-lea,HU Xiao-qina,LU Chenb

(a.GuangxiKeyLaboratoryofHybridComputationandICDesignAnalysis；b.CollegeofInformationScienceandEngineering,

GuangxiUniversityforNationalities,Nanning530006,China)

Abstract:The hardware/software partition is one of the standard of evaluating the software/hardware co-design,a bad partition might make a worse co-design, or even a fail design. Inthispaper,The hardware/softwarepartitionproblemwas modeled with formulas of Satisfiability Modulo Theory (SMT).In our knowledge,itwouldbe thefirsttime to apply the SMT,as well as the SMT solvers including Z3,CVC4 and MathSAT5,tohardware/softwarepartitionproblem.According to the experiments,the optimizedpartition with the SMT and solvers,more-over,the Z3 solver is proved as the more efficient for hardware/software partition.In short,in terms of the SMT and its solvers,the method avoid the local optimized solution of the partition problem,as well as the method could be applied in the large scale of the co-design.

Key Words:Software/hardware；Co-design；The hardware/softwarepartition；SMT；SMT solvers

中圖分類號(hào)：TP301.6

文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：1673-8462(2016)01-0078-05

作者簡介：毛樂樂(1989-)，河北衡水人，廣西民族大學(xué)信息科學(xué)與工程學(xué)院碩士研究生，研究方向：大規(guī)模集成電路驗(yàn)證.

基金項(xiàng)目：廣西民族大學(xué)研究生教育創(chuàng)新計(jì)劃(gxun-chxs2015097).

收稿日期：2015-10-16.