可滿足模理論在軟硬件劃分領域的應用*

毛樂樂,胡小勤,盧　晨

(廣西民族大學,a.廣西混雜計算與集成電路設計分析重點實驗室；

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

?

可滿足模理論在軟硬件劃分領域的應用*

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

(廣西民族大學,a.廣西混雜計算與集成電路設計分析重點實驗室；

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

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

關鍵詞：軟硬件協同設計；軟硬件劃分；可滿足模理論；可滿足模理論求解器

0引言

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

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

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

1軟硬件劃分問題的描述與數學模型

軟硬件劃分是軟硬件協同設計的重要環節和組成部分，其主要任務是在滿足各項設計約束的條件下，把系統功能劃分到目標結構中的軟件和硬件部分上，并為系統提供最佳的軟硬件劃分方案.

這篇文章利用可滿足模理論在短時間內生成一套執行時間少，系統總代價小的高質量劃分方案.

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

定義1R={R0,R1,…,Rn}代表劃分系統的所有任務節點集合,其中Ri表示第i個任務節點，其中i=0,1,2,…,n.圖中的一個節點就是對應劃分系統的一個任務，每個節點包含其軟件、硬件代價信息,例如采用硬件時的運行時間和采用軟件時在處理器上執行時間.

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

定義3軟硬件劃分問題中我們可以得出x=(x0,x1,x2,…,xn)是劃分系統任務流圖的一個可行解，代表對系統的一種劃分，xi{0,1}，xi=1代表Ri由軟件實現，xi=0代表Ri由硬件實現，其中i代表第i個節點, i=0,1,2,…,n.

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

1.1軟硬件劃分問題定義

軟硬件劃分實質是對節點集合做劃分，即將原節點集合R={R0,R1,…,Rn}劃分為兩個子集，即Q=(Rh,RS)，其中Rh∪RS=R且Rh∩RS=Φ.

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

HR=∑Ri∈Rhhi

(1)

式中，hi，si分別表示第i個節點交由硬件實現或軟件實現所消耗的代價.

SR=∑Ri∈RSsi

(2)

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

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

(3)

(4)

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

S(x)+ H(x)

(5)

即

(6)

軟硬件劃分問題：在滿足性能約束的條件下，將一個節點集合R={R0,R1,…,Rn}進行劃分，分別映射到軟件和硬件實現，系統的軟硬件劃分完成后可以使得系統的軟硬件代價最小，整個問題轉化成規劃問題：

目標函數MinCost(x)

約束函數Cost(x)

系統經過每一次軟硬件劃分后，都會產生一個新的系統代價，并且新的系統代價要比上一次的系統代價小.若進行m次劃分后的系統總代價用Vm+1表示，則Vm+2≤Vm+1，如此不斷劃分尋找滿足條件的最小值Vm+1.

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

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

假設要進行判定的SMT公式如下：

φ∶=(x1∧x2)∨x3

(7)

若x1,x2,x3為布爾量用SMT-LIB[8]標準語言描述公式φ，有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解決器的輸入參數，經過SMT解決器處理后可以判斷出SMT公式是可滿足的還是不可滿足的，以及輸出當公式可滿足時x1,x2,x3的值.

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

將軟硬件劃分問題轉化為SMT問題分為以下幾個步驟：

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

將原節點集合劃分問題轉化成SMT問題即用SMT-LIB標準語言描述得下式：

(declare-constxiInt)

(8)

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

(9)

即將第i個節點交由軟件或硬件實現.將軟硬件劃分中約束函數

轉化成SMT問題描述如下：

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

(10)

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

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

X1+3X2≤6X3

(11)

在smt2文件中LA理論應用于

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

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

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

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

(12)

可以得到一個新的軟硬件代價Vm+2.

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

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;

首先初始化軟硬件代價系數h，s和總代價v1，v2.然后生成z3的輸入文件，調用z3，求得新的劃分，將劃分的結果保存到result1和result2中.其中v1表示前一個劃分下的軟硬件代價的總和，v2表示當前劃分下的軟硬件代價的總和.result1表示前一個劃分的結果，result2表示當前劃分的結果.接著循環調用z3直到result2不可滿足時，result1即為所求得的劃分結果.

2仿真實例與分析

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

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

運用的SMT解決器:Z3、CVC4、Mathsat5.

Z3[9]是微軟公司研發的一個高效、可擴展與表達性強的SMT求解器.曾在SMT-COMP競賽中表現不俗，是到目前為止綜合求解能力最強的SMT求解器.

CVC是由紐約大學和愛荷華大學共同領導開發，具有給出證明和模型的推導能力等優點.最新的CVC系列的解決器是CVC4.

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

以節點為4為例,即i=4得約束函數公式：

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

(13)

用SMT-LIB標準語言描述公式(13),即將軟硬件劃分問題轉化為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解決器的求解效率而編寫的用例，隨后調用Z3求解得x0=0,x1=1,x2=0和x3=0.執行時間為0.356523 s，系統軟硬件代價為14.6.此外我們還作了大量的實例分析，部分結果如表1所示.

對比表1中的統計數據可以得出，調用MathSAT解決器在變量為0～15范圍內比Z3和CVC4解決器較快.調用Z3解決器在變量為15～178范圍內比MathSAT5、CVC4較快，系統的軟硬件實現總代價較小.CVC4解決器在各變量范圍內執行時間最長，系統的軟硬件實現代價最大.Z3在這篇文章的測試中具有時間開銷小，系統軟硬件開銷小的性能特點，具有較強的求解實力，CVC4在求解可滿足解時求解能力欠佳，MathSAT5在求解不可滿足解時求解能力欠佳.

表1　實驗結果

3結語

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

[參考文獻]

[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] 鄒誼，莊鎮泉，李斌.基于量子遺傳算法的嵌入式系統軟硬件劃分算法[J].電路與系統學報,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/.

[責任編輯蘇琴]

[責任校對黃招揚]

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

中圖分類號：TP301.6

文獻標識碼：A

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

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

基金項目：廣西民族大學研究生教育創新計劃(gxun-chxs2015097).

收稿日期：2015-10-16.