摘要:為了提高FPGA技術(shù)映射算法的質(zhì)量,提出了一種基于布爾可滿足性(SAT)的算法,在實(shí)現(xiàn)系統(tǒng)功能的前提下,可以將一個(gè)子電路映射到數(shù)量最少的查看表中。通過(guò)將該算法迭代應(yīng)用于已經(jīng)完成映射的電路局部,在許多情況下,可以使用更少的查看表來(lái)完成。
關(guān)鍵詞:布爾可滿足性;FPGA;再綜合;映射優(yōu)化;查看表
中圖分類號(hào):TP331文獻(xiàn)標(biāo)識(shí)碼:A 文章編號(hào):1009-3044(2008)35-2502-02
An Optimality of FPGA Mapping Algorithms Based on SAT
LU Hua-qi
(Department of Computer Engineering, Huaiyin Institute of Technology, Huai’an 223003, China)
Abstract: This paper attempts to quantify the optimality of FPGA technology mapping algorithms. We develop an algorithm, based on Boolean satisability (SAT), that is able to map a small subcircuit into the smallest possible number of lookup tables (LUTs) needed to realize its functionality. We iteratively apply this technique to small portions of circuits that have already been technology mapped by the best available mapping algorithms for FPGAs. In many cases, the optimal mapping of the subcircuit uses fewer LUTs than is obtained by the technology mapping algorithm.
Keywords: Boolean Satisability; Resynthesis; Mapping Optimization; FPGA, Lookup Table
1 引言
FPGA是可重構(gòu)的集成電路,其特點(diǎn)是由大量可編程的布線結(jié)構(gòu)包圍的可編程邏輯模塊。目前大部分FPGA器件都包含基于K個(gè)輸入查看表(K-LUT)的可編程邏輯模塊,一個(gè)K-LUT含有2K個(gè)真值表配置位,因此K-LUT可以實(shí)現(xiàn)任意的K個(gè)輸入功能。對(duì)于一個(gè)給定電路而言,實(shí)現(xiàn)給定電路的LUT數(shù)量決定了基于FPGA實(shí)現(xiàn)的尺寸和代價(jià)。因此,在FPGA CAD流程中最重要的的階段之一就是技術(shù)映射,技術(shù)映射將一個(gè)優(yōu)化過(guò)的電路描述映射到目標(biāo)FPGA體系結(jié)構(gòu)中的一個(gè)LUT網(wǎng)絡(luò)中。
在技術(shù)映射過(guò)程中,常常將技術(shù)映射看為覆蓋問(wèn)題。例如,在圖1中給出了將一個(gè)電路映射到LUT的過(guò)程。圖1a是初始的門級(jí)網(wǎng)絡(luò),圖1b是使用4-LUT對(duì)初始網(wǎng)絡(luò)的可能覆蓋,圖1c給出了由覆蓋產(chǎn)生的LUT網(wǎng)絡(luò)[1]。在所給出的映射中,標(biāo)號(hào)為x的門同時(shí)屬于兩個(gè)LUT,即復(fù)制了x。有時(shí),為了最小化LUT網(wǎng)絡(luò)面積,必須復(fù)制門電路。
對(duì)于小的子電路來(lái)說(shuō),實(shí)現(xiàn)面積優(yōu)化沒(méi)有問(wèn)題。設(shè)f(i0,i1,…,in)是任意函數(shù),如果以3-LUT或2-LUT實(shí)現(xiàn),可以使用圖2所示的可配置虛擬網(wǎng)絡(luò)(Configurable Virtual Network, CVN)來(lái)實(shí)現(xiàn)面積的優(yōu)化。CVN是由連接到變量i0,i1,…,in的輸入線與三個(gè)2-LUT組成。交叉位置允許LUT輸入選擇來(lái)自其它LUT的任意輸入線或輸出線。交叉點(diǎn)上的每一個(gè)“開(kāi)關(guān)”由一個(gè)虛擬配置位進(jìn)行配置,其中0代表交叉點(diǎn)是不連接的,而1表示交叉點(diǎn)是連接的。如同為每個(gè)2-LUT設(shè)置真值表配置位一樣,通過(guò)控制虛擬配置位,可以枚舉包含三個(gè)2-LUT的每一種可能的電路配置[2]。
在式(1)及(2)中,可以看到網(wǎng)絡(luò)fnet的輸出作為布爾表達(dá)式,其中表達(dá)式中包括變量i0, i1…, in、虛擬配置位V1…Vm及真值表配置位L1…Lo。在這兩個(gè)式中,需要提出的是,對(duì)于i0,…, in所有的值來(lái)說(shuō),V1…Vm及L1…Lo的賦值對(duì)fnet(i0, i1…, in,V1…Vm,L1…Lo)引起的變化是否等同于f(i0, i1…, in),這個(gè)問(wèn)題可以從布爾可滿足性(Boolean Satisfiability, SAT)中獲得確切的答案[2]。給定在交集范式(Conjunctive Normal Form, CNF)中的一個(gè)布爾表達(dá)式,其中表達(dá)式是由句子的一個(gè)乘積組成的,而每個(gè)句子是由文字的和組成的,試圖對(duì)變量進(jìn)行賦值,使每個(gè)句子至少有一個(gè)文字的值為真。
2 對(duì)面積的再綜合
所謂針對(duì)面積的再綜合,必須以原有的LUT電路為基礎(chǔ),其目的是在維持原有功能的基礎(chǔ)上,試圖降低電路圖中的LUT數(shù)量。
2.1 將綜合問(wèn)題轉(zhuǎn)化為布爾可滿足性
確定一個(gè)n可達(dá)的錐面是否能用X個(gè)n-LUT實(shí)現(xiàn)的方法將其進(jìn)行再綜合到用X-1個(gè)或更少的n-LUT的n可達(dá)錐面中,驗(yàn)證的方法是使用SAT。完成的過(guò)程時(shí)首先生成一個(gè)比初始的錐面所包含的LUT數(shù)量更少的n可達(dá)的沒(méi)有扇出的錐面(Fanout Free Cone, FFC),然后,將代表初始錐面功能的真值表賦給CNF表達(dá)式。如果該CNF表達(dá)式是可滿足的,再綜合成一個(gè)新的FFC是可行的。
為了更清晰地表達(dá)這個(gè)過(guò)程,圖3中的3a是由三個(gè)2-LUT組成的初始錐面,其功能實(shí)現(xiàn)了一個(gè)三輸入。由于該錐面只有三個(gè)輸入,將圖3a再綜合成圖3b并節(jié)省一個(gè)LUT是可行的。為了確定是否可以從圖3a再綜合到圖3b,圖3b必須轉(zhuǎn)換成一個(gè)CNF表達(dá)式,如果表達(dá)式是滿足的,則再綜合是可行的[3]。
CNF等式能夠表達(dá)電路的所有合法向量,例如,在圖4中,當(dāng)且僅當(dāng)圖4a中的信號(hào)A、B及Z與一個(gè)AND門的功能相對(duì)應(yīng)時(shí)(如(A=0, B=X, Z=0)、(A=X, B=0, Z=0)或(A=1, B=1, Z=1)),式(1)才滿足。與此相同,只有類似(A=1, B=1, C=0, Z=1, Y=0)的合法向量時(shí),式(2)才滿足。
F1(A,B,Z)=(A+Z)·(B+Z)·(A+B+Z) (1)
F2(A,B,C,Z,Y)=(A+Z)·(B+Z)·(A+B+Z)·(Z+Y)·(C+Y)·(Z+C+Y) (2)
為了實(shí)現(xiàn)這種再綜合的檢查,首先應(yīng)該形成CNF的等式,其次,應(yīng)該根據(jù)錐面的真值表限制在CNF等式中的輸入與輸出變量。最后,利用一個(gè)SAT解決器來(lái)檢查可滿足的賦值[4]。例如,將一個(gè)兩輸入的錐面映射到圖4b的電路上,將C設(shè)置為配置位。為了檢查兩輸入的函數(shù)f(1,1)=1是可達(dá)的,可以通過(guò)判斷是否滿足F2(A=1,B=1,C,Z,Y=1)=1來(lái)實(shí)現(xiàn)。很明顯,當(dāng)C=1時(shí)其返回值為真值。但是,這只能說(shuō)明f(1,1)=1是可行的,即只是一個(gè)真值表的值。為了在整個(gè)錐面上驗(yàn)證一個(gè)再綜合的電路,即驗(yàn)證整個(gè)真值表,其CNF等式將反復(fù)計(jì)算2n次,以形成一個(gè)新的CNF等式,其中n為所映射錐面的扇入數(shù)量。基本電路CNF等式的每一次重復(fù)計(jì)算都對(duì)應(yīng)著錐面真值表中的一個(gè)值。因此,需要強(qiáng)調(diào)的是,為了檢查初始的錐面是否能夠與再綜合的電路相匹配,可以通過(guò)在一個(gè)新的CNF式上完成SAT的檢驗(yàn)來(lái)實(shí)現(xiàn)。
再返回到圖3中初始的LUT例子,下面的步驟將給出如何實(shí)現(xiàn)這些轉(zhuǎn)換。圖5是圖3b的細(xì)節(jié)圖,該圖清楚地給出了CNF構(gòu)造的內(nèi)部連線及配置位。在這些步驟中,f代表需要進(jìn)行再綜合的錐面的函數(shù),Xi代表輸入向量x1x2x3=i和fi=f(Xi)。
步驟1:針對(duì)再綜合電路中的每一個(gè)元素各生成一個(gè)CNF等式,見(jiàn)式(3)及(4)。
步驟2:從式(3)及式(4)中形成電路CNF等式。式(5)是一個(gè)與電路的輸入與輸出(x1-3, f)、內(nèi)部連線(M)及配置位(L1-8)變量相關(guān)的表達(dá)式。
Gresynth(Xi,fi)=GLUT1·GLUT2 (5)
步驟3:重復(fù)式(5)并根據(jù)f函數(shù)對(duì)輸入與輸出變量進(jìn)行約束。
在式(6)中,使用在每一個(gè)Gresynth(Xi,fi)實(shí)例中的同一變量(L1-8)來(lái)代表配置位,在每一個(gè)實(shí)例中的所有其他信號(hào)都有不同的變量[5]。這就保證了在每一個(gè)真值表的值都有唯一的配置位。最后,如果錐面與再綜合的結(jié)構(gòu)是對(duì)應(yīng)的,式(6)通過(guò)SAT檢驗(yàn)后將返回真值。
2.2 生成錐面
許多算法可以生成并存儲(chǔ)圖中所有的再綜合錐面,其中有一種算法是從PI到PO按照拓?fù)渑判虮闅v圖來(lái)生成再綜合錐面。在每一個(gè)內(nèi)部LUT中,通過(guò)與輸入LUT的錐面結(jié)合來(lái)產(chǎn)生新的錐面。本文中,如果錐面所有的輸入不超過(guò)(n+e),其中n為最大的再綜
合錐面扇入數(shù),e為擴(kuò)充值,則錐面產(chǎn)生算法與其他錐面結(jié)合。只有將e設(shè)為足夠高的數(shù)值,該啟發(fā)式算法才可以加速錐面生成的過(guò)程,而不會(huì)嚴(yán)重影響再綜合解決方案的質(zhì)量。
對(duì)于有1個(gè)以上扇出的錐面必須特別處理。例如圖6,如果將a到e的LUT再綜合到f到g的LUT,則必須將c到e的LUT復(fù)制,以保持LUT c的扇出。這樣,該再綜合算法總的節(jié)約只有1個(gè),而如果LUT c沒(méi)有扇出,則會(huì)節(jié)約3個(gè)。
3 結(jié)束語(yǔ)
本文提出一種可以幫助理解最新FPGA映射算法最優(yōu)性的方法,主要思想是將電路的每個(gè)部分再綜合,直到其達(dá)到最優(yōu)狀態(tài)。下一步的工作是尋找改進(jìn)該局部?jī)?yōu)化再綜合的方法。通過(guò)測(cè)試自定義硬件加速方法以改善錐面再綜合的運(yùn)行時(shí)間,研究使用don’t care來(lái)降低CNF的復(fù)雜度并增加再綜合研究領(lǐng)域的敏捷性。
參考文獻(xiàn):
[1] Altera.Component selector guide[S].ver 18.0,2007.
[2] Chai D,Jiang J,Jiang Y,et al.MVSIS 2.0 Programmer's Manual[R].UC Berkeley,Technical report,2003.
[3] Farrahi,Sarrafzadeh M.Complexity of the Lookup-Table Minimization Problem for FPGA Technology Mapping[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2003,13(11):1319-1332.
[4] Cong J,Wu C,Ding Y.Cut ranking and pruning: Enabling a general and efficient FPGA mapping solution[C].FPGA,2007:29-35.
[5] Xilinx.Virtex-ii complete data sheet[S].ver 5.3,2007.