王先建 王倫耀 儲(chǔ)著飛 夏銀水

(寧波大學(xué)信息科學(xué)與工程學(xué)院 寧波 315211)

1 引言

CMOL電路是結(jié)合納米技術(shù)和傳統(tǒng) CMOS工藝的 CMOS/納米線/分子混合(CMOS/nanowire/MOLecular hybrid, CMOL)電路結(jié)構(gòu)[1]，而且文獻(xiàn)[2]從理論上證明了 CMOL電路進(jìn)行單元配置可實(shí)現(xiàn)電路邏輯功能的完備性。由于CMOL電路結(jié)構(gòu)既保留了目前成熟的CMOS工藝，同時(shí)又具有納電子器件所具有的高密度特點(diǎn)而受到研究者們的廣泛關(guān)注，其研究?jī)?nèi)容包括 CMOL存儲(chǔ)器[3]、CMOL FPGA[4]以及神經(jīng)元電路[5]等等。而在有關(guān) CMOL CAD的研究中，CMOL的單元配置方法一直是一個(gè)重要內(nèi)容[4,6-8]，因?yàn)樗?CMOL電路實(shí)現(xiàn)特定功能必經(jīng)的步驟。

目前對(duì) CMOL電路的單元配置方法已經(jīng)開展了一些研究。這些方法包括基于邏輯簇(Tile)的設(shè)計(jì)方法[4]，基于力矢量算法[6]，啟發(fā)式算法[7]以及電路等效變換法[8]等，并發(fā)展出了CMOL自動(dòng)綜合工具CMOL FPGA CAD 1.0[4]。

CMOL電路的單元配置問題實(shí)際上也可以被描述成一個(gè)可滿足性問題(Satisfiability Problem)，因此可以利用布爾可滿足性(Boolean Satisfiability,SAT)來解決 CMOL電路的單元配置問題。但在已發(fā)表的利用SAT實(shí)現(xiàn)CMOL電路單元配置的方法中[9]，由于采用二項(xiàng)式編碼[10]，使得子句的個(gè)數(shù)過多、中間處理文件過大，影響了算法的效率和處理電路大小的能力。相比于用合取范式(Conjunctive Normal Form, CNF)表示的約束，偽布爾(Pseudo-Boolean, PB)約束更加容易表示[11-15]。目前偽布爾可滿足性(Pseudo-Boolean Satisfiability, PBS)法[11]已被成功應(yīng)用于低功耗狀態(tài)分配[12]和最大電路開關(guān)性估計(jì)[13]等領(lǐng)域中。本文提出利用 PBS法來解決CMOL電路的單元配置問題，該方法在不增加額外的布爾變量集個(gè)數(shù)的條件下，通過降低編碼過程中的約束個(gè)數(shù)[10,11]達(dá)到減少中間處理文件大小的目的。實(shí)驗(yàn)結(jié)果表明，相比于文獻(xiàn)[9]的基于傳統(tǒng)SAT的CMOL單元配置方法，本文采用的方法能有效減少中間處理文件大小，達(dá)到加快算法速度和提高求解電路規(guī)模的目的。

2 CMOL FPGA結(jié)構(gòu)

在CMOL電路中，納米線以一定的長(zhǎng)度周期性斷開，納米線的這種特點(diǎn)使得每一個(gè)CMOL單元只能與周圍M=2r(r-1)-1個(gè)其它 CMOL單元相連，其中r為連通域半徑。以圖1為例，其中r為3，圖中深灰色單元C只能與周圍 11個(gè)淺灰色單元連通，這些淺灰色單元構(gòu)成了深灰色單元的連通域。此外，CMOL電路中的兩點(diǎn)相對(duì)位置常用曼哈頓距離來表示。如在圖1中，C,D兩個(gè)CMOL單元的坐標(biāo)分別為C(x1,y1),D(x2,y2)，則它們之間的曼哈頓距離為|x1-x2|+|y1-y2|。利用連通域半徑和曼哈頓距離就可以確定某一CMOL單元的連通域。以圖1為例，在圖1中坐標(biāo)原點(diǎn)在C上，坐標(biāo)軸將圖1分為4塊，分別為第1至第4象限，則當(dāng)圖1中某一點(diǎn)D與C的曼哈頓距離分別不大于r,r-1,r-2 及r-1時(shí)，那么滿足這些曼哈頓距離約束條件的CMOL單元D的個(gè)數(shù)就是CMOL單元C的連通域大小。

圖1 CMOL FPGA

3 CMOL單元配置問題的PBS描述

3.1 偽布爾可滿足性

SAT是用來解決給定的布爾方程是否存在一組變量賦值使問題為可滿足。而布爾方程的描述常采用CNF來表示。在CNF中，由m個(gè)子句w1,…,wm的合取組成；而子句由k個(gè)文字的析取組成。其中一個(gè)文字即為一個(gè)變量或者其反變量。因此，為了滿足一個(gè)式子，每一個(gè)子句必須至少有一個(gè)文字的值為真。

隨著SAT法的快速發(fā)展，SAT求解器被擴(kuò)展用來處理PB約束，即為帶整數(shù)系數(shù)的線性不等式。偽布爾可滿足性問題可表示為 PB約束的合取，其中PB約束可表示為

式(1)中ai和b為整數(shù)常數(shù)；li為一個(gè)文字，可表示為變量xi和其反變量，即li=xi或者li=，其中xi∈{0,1},；“?”為關(guān)系操作符，可表示“=”，“＞”，“≥”，“＜”或者“≤”。若式(1)中的|ai|都為同一個(gè)數(shù)a0時(shí)，則式(1)對(duì)應(yīng)的 PB約束稱為基數(shù)約束(cardinality constraints)，即

假設(shè)一個(gè)PB式子F為PB約束的合取。對(duì)于PBS問題，如果存在一組配置解x1,…,xm滿足所有的PB約束使得F為真，則表示F可滿足，這一組解即為可配置解。

例如，給定一個(gè)F(x1,x2,x3)=(2x1-2x2≥1)∧(x1+x2+3≥1)，它由3個(gè)布爾變量，5個(gè)文字，2個(gè) PB約束組成。{x1=1,x2=0,x3=1}和{x1=1,x2=0,x3=0}等都為可滿足配置解。

3.2 CMOL單元配置問題的PBS描述

由于CMOL電路僅適于“或非/非”邏輯電路，因此在進(jìn)行 CMOL單元配置之前需要對(duì)原始電路進(jìn)行轉(zhuǎn)換，該轉(zhuǎn)換可以借助邏輯綜合工具SIS將由“與/或/非”邏輯電路轉(zhuǎn)換成“或非/非”邏輯電路。而 CMOL單元配置過程就是通過設(shè)置可配置納米二極管的狀態(tài)，將一個(gè)給定的邏輯電路功能用CMOL FPGA實(shí)現(xiàn)的過程。

在CMOL單元配置過程中，一般將電路輸入輸出端口放在CMOL電路的四周。因此對(duì)于一個(gè)由行(row)，列(column)構(gòu)成的CMOL單元陣列，令C表示該陣列的CMOL單元集合，||C||表示集合C中的元素個(gè)數(shù)；C1表示位于C邊界上的 CMOL單元集合，||C1||表示集合C1中的元素個(gè)數(shù)；C2表示位于非C邊界上的CMOL單元集合，||C2||表示集合C2中的元素個(gè)數(shù)。則有

由于CMOL電路結(jié)構(gòu)存在連通域約束，因此對(duì)于一個(gè)CMOL單元c,c∈C,D(c)為構(gòu)成c的連通域的CMOL單元的集合，則有

給定一個(gè)基于“或非/非”邏輯的電路K，電路K可被看作是一個(gè)無環(huán)有向圖(Directed Acyclic Graph, DAG)，即K=(G,E)。其中G為對(duì)應(yīng)于“或非/非”門的節(jié)點(diǎn)集合，E=G×G表示連接的門與門的邊的集合。對(duì)于電路中的任意門g,g'∈G，要想得到(g,g')∈E，當(dāng)且僅當(dāng)門g的輸出與門g'的輸入相連，亦即

根據(jù)邏輯門在邏輯電路中所處的位置的不同，可以將邏輯門集合G分為3個(gè)子集，即G1,G2和G3，分別表示輸入端口的邏輯門集合，輸出端口的邏輯門集合和非輸入輸出端口的邏輯門集合，并用||G1||,||G2||和||G3||表示各子集中包含的元素個(gè)數(shù)。并且有

CMOL單元配置問題則可描述為將給定的電路邏輯門的集合G配置到 CMOL單元集合C中是否存在可配置解的問題。CMOL單元配置問題可用數(shù)學(xué)式描述成一個(gè)內(nèi)射函數(shù)P，即P:G→C。在進(jìn)行CMOL單元配置過程中，至少要滿足以下4個(gè)約束：

(1)與輸入、輸出端口相連的門必須被配置到陣列邊界的CMOL單元上，作為I/O口，即

(2)每個(gè)“或非/非”門必須被配置到有且僅有一個(gè)CMOL單元上，即

(3)兩個(gè)或者兩個(gè)以上不同的門不能被配置到同一個(gè)CMOL單元上，即

(4)電路中有連接關(guān)系的門單元位于各自的連通域中，即

考慮到 CNF中子句的數(shù)量與布爾變量成指數(shù)級(jí)增加，為此本文在不增加額外的布爾變量集個(gè)數(shù)的條件下，采用PB約束代替CNF，達(dá)到減少約束個(gè)數(shù)的目的。在描述CMOL單元配置問題時(shí)，ai為0或1,b為 1，相關(guān)的PB約束可以表示為以下 3種約束，分別為：

(1)關(guān)系操作符“?”為“≤”時(shí)，即為“至多一個(gè)”基數(shù)約束，簡(jiǎn)稱AMO(At-Most-One)約束，即

(2)關(guān)系操作符“?”為“≥”時(shí)，即為“至少一個(gè)”基數(shù)約束，簡(jiǎn)稱ALO(At-Least-One)約束。這種PB約束等價(jià)于標(biāo)準(zhǔn)的SAT子句，即

(3)關(guān)系操作符“?”為“=”時(shí)，即為“有且僅有一個(gè)”基數(shù)約束，簡(jiǎn)稱EO(Exactly-One)約束，即

CMOL單元配置問題主要由這3種基數(shù)約束來表示，從3種基數(shù)約束可以看出，只須對(duì)AMO約束進(jìn)行改進(jìn)即可。傳統(tǒng)的SAT法針對(duì)AMO約束采用二項(xiàng)式編碼法，即

在本文中，布爾變量表示將門g配置到CMOL單元c中，其中g(shù)∈G和c∈C。因此給定一個(gè)電路G和CMOL單元陣列，符合式(7)-式(10)的CMOL單元配置可以被編碼成以下幾種類型的PB約束：

(1)當(dāng)門g必須被配置到有且僅有一個(gè) CMOL單元c上，即可編碼成

(2)當(dāng)CMOL單元c至多被一個(gè)門g配置，即可編碼成

(3)當(dāng)門g'配置在CMOL單元c上，那么與門g'的輸入線有連接關(guān)系的門g應(yīng)該配置在CMOL單元c的連通域范圍內(nèi)，即可編碼成

將式(15)-式(17)中的PB約束集導(dǎo)入PBS求解器中。針對(duì)CMOL單元配置時(shí)碰到的實(shí)際問題，可導(dǎo)入更多其它的PB約束。例如，任意的“或非/非”門可以配置到滿足以上 PB約束的任意的CMOL單元上?？紤]到屬于G1和G2的門被要求配置在陣列邊界當(dāng)作I/O口，因此可設(shè)置 Σc∈C1=1。這樣能夠通過PB約束傳播達(dá)到簡(jiǎn)化CMOL單元配置問題。

PBS法的具體步驟為：

步驟 1 通過 SIS邏輯綜合工具將原始 BLIF電路網(wǎng)表文件轉(zhuǎn)換成全由“或非/非”門組成的BLIF格式電路文件；

步驟 2 讀入基于“或非/非”門的BLIF電路，對(duì)輸入信號(hào)、“或非/非”門等進(jìn)行標(biāo)號(hào)；

步驟 3 根據(jù)標(biāo)號(hào)的個(gè)數(shù)以及I/O個(gè)數(shù)來設(shè)置CMOL單元陣列大?。?/p>

步驟 4 應(yīng)用PBS法根據(jù)式(7)-式(10)的條件約束將基于“或非/非”門的 BLIF電路配置到CMOL單元陣列中；

步驟 5 將步驟 4中的所有 PB約束導(dǎo)入到PBS求解器中，如果有一個(gè)解滿足所有的PB約束，那這個(gè)解就是CMOL單元配置解，反之則無可配置解。

4 實(shí)例說明

下面以全加器為例子來說明一個(gè)原始的電路是如何利用PBS法配置到CMOL電路中的。

步驟 1 通過 SIS邏輯綜合工具對(duì)原始全加器的BLIF電路網(wǎng)表文件轉(zhuǎn)換成由“或非/非”門組成的BLIF格式電路文件，如圖2(a)所示。

步驟 2 由圖 2(a)中可以看出，電路有 3個(gè)輸入信號(hào)A,B,C, 2個(gè)輸出信號(hào)Sum,D，有 15個(gè)標(biāo)號(hào)，其中標(biāo)號(hào)1, 2, 3為輸入信號(hào)，標(biāo)號(hào)11, 15為輸出信號(hào)門，標(biāo)號(hào)4, 5, 6為“非”門，標(biāo)號(hào)7, 8,9, 10, 11, 12, 13, 14, 15為“或非”門。并將它們之間的連接關(guān)系進(jìn)行記錄，例如標(biāo)號(hào) 11的門與標(biāo)號(hào)7, 8, 9, 10的門相連。

步驟 3 此例可設(shè)置5×4大小的 CMOL單元陣列，如圖2(b)所示。為與傳統(tǒng)的SAT法進(jìn)行公平對(duì)比，默認(rèn)設(shè)置連通域半徑r也為9。

圖2 全加器實(shí)例

步驟5 將步驟4中的所有PB約束導(dǎo)入到PBS求解器中，如果有一個(gè)解滿足所有的PB約束，那這個(gè)解就是CMOL單元配置解。即基于“或非/非”門的全加器電路成功配置到CMOL電路中。

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

本文中提到的基于PBS的CMOL單元配置法用C語言編程實(shí)現(xiàn)，通過GCC編譯，在linux操作系統(tǒng)及Intel Pentium Dual-core 3 GHz CPU, 2 GBRAM的PC環(huán)境下運(yùn)行。表1中的數(shù)據(jù)是采用perl腳本語言對(duì)每個(gè)測(cè)試電路進(jìn)行20次的實(shí)驗(yàn)測(cè)試，然后取出相對(duì)公平的中間值得到的。

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

從表1可以看出，相對(duì)于傳統(tǒng)的SAT法，PBS法在沒有增加額外的布爾變量集個(gè)數(shù)的基礎(chǔ)上，SAT法中的子句個(gè)數(shù)平均為PBS法中的PB約束個(gè)數(shù)的126.29倍，說明PBS法比傳統(tǒng)的SAT法更易表示、更簡(jiǎn)單。CNF大小平均為OPB大小的4.01倍?？紤]到OPB文件為PB約束的合取，亦即單元配置過程中產(chǎn)生的中間處理文件，它的減小有利于CAD工具在運(yùn)行過程中占用更少的內(nèi)存，或可求解更大的電路。從時(shí)間來看，對(duì)于 s27, s386及 s444 3個(gè)電路，PBS法所用時(shí)間稍微比傳統(tǒng)的SAT法略長(zhǎng)一點(diǎn)，但從平均值角度看，PBS法求解速度要比傳統(tǒng)的SAT法求解速度快9.03倍。并且傳統(tǒng)的SAT法對(duì)于s420及s526兩個(gè)電路無法求解，而PBS法可以。

6 結(jié)論

針對(duì) CMOL單元配置問題，本文提出了基于PBS的單元配置方法。傳統(tǒng)的SAT法在處理CMOL單元配置過程中，因采用二項(xiàng)式編碼使得子句的個(gè)數(shù)過多、中間處理文件過大，影響了算法的效率和處理電路大小的能力。為此，本文在不增加額外的布爾變量集個(gè)數(shù)的條件下，通過降低約束個(gè)數(shù)、減小中間處理文件，將問題編碼成PBS問題。實(shí)驗(yàn)結(jié)果表明，PBS法的PB約束個(gè)數(shù)比傳統(tǒng)的SAT法的子句個(gè)數(shù)平均減少了126.29倍，中間處理文件大小平均減少了4.01倍，CPU運(yùn)行時(shí)間平均快了9.03倍，并且增大了求解規(guī)模。

[1]Likharev K K and Strukov D B. CMOL: Devices, Circuits,and Architectures. Introducing Molecular Electronics[M].Berlin: Springer, 2005: 447-477.

[2]Chen Gang, Song Xiao-yu, and Hu Ping. A theoretical investigation on CMOL FPGA cell assignment problem[J].IEEE Transactions on Nanotechnology, 2009, 8(3): 322-329.

[3]Strukov D B and Likharev K K. Defect-tolerant architectures for nanoelectronic crossbar memories[J].Journal of Nanoscience and Nanotechnology, 2007, 7(1): 151-167.

[4]Strukov D B and Likharev K K. CMOL FPGA circuits[C].Proceedings of International Conference on Computer Design,Las Vegas, Nevada, USA, June 26-29, 2006: 213-219.

[5]Afifi A, Ayatollahi A, and Raissi F. CMOL implementation of spiking neurons and spike-timing dependent plasticity[J].International Journal of Circuit Theory and Applications,2011, 39(4): 357-372.

[6]Kim K, Karri R, and Orailoglu A. Design automation for hybrid CMOS-nanoelectronics crossbars[C]. Proceedings of IEEE International Symposium on Nanoscale Architectures,Los Alamitos, CA, USA, October 21-22, 2007: 27-32.

[7]Xia Yin-shui, Chu Zhu-fei, and Hung N N,et al.. An intergrate optimizaiton approach for nano-hybrid circuit cell mapping[J].IEEE Transactions on Nanotechnology, 2011,10(6): 1275-1284.

[8]夏銀水, 儲(chǔ)著飛, 王倫耀, 等. 納米CMOS電路邏輯等效轉(zhuǎn)換[J]. 電子與信息學(xué)報(bào), 2011, 33(7): 1733-1737.

Xia Yin-shui, Chu Zhu-fei, and Wang Lun-yao,et al.. Logic equivalent transformation for nano-meter CMOS hybrid circuits[J].Jounal of Electronics&Information Technology,2011, 33(7): 1733-1737.

[9]Hung N N, Gao Chang-jian, and Song Xiao-yu,et al.. Defect tolerant CMOL cell assignment via satisfiability[J].IEEE Sensors Journal, 2008, 8(6): 823-830.

[10]Chen Jing-chao. A new SAT encoding of the at-most-one constraint[C]. Proceedings of the Tenth International Workshop on Constraint Modelling and Reformulating, St.Andrews, Scotland, UK, September 6, 2010.

[11]Roussel O and Manquinho V. Pseudo-Boolean and Cardinality Constraints. Handbook of Satisfibility[M].Amsterdam: IOS Press, 2009: 695-733.

[12]Sagahyroon A, Aloul F, and Sudnitson A. Using SAT-based techniques in low power state assignment[J].Journal of Circuits,Systems,and Computers, 2011, 20(8): 1-14.

[13]Mangassarian H, Veneris A, and Najm F N. Maximum circuit activity estimation using Pseudo-Boolean Satisfiability[J].IEEE Transactions on Computer-Aided Design of Intergrated Circuits and Systems, 2012, 31(2): 271-284.

[14]Eén N and S?rensson N. Translating Pseudo-Boolean constraints into SAT[J].Journal of Satisfiability,Boolean Modeling and Computation, 2006, 2: 1-26.

[15]Berre D Le and Parrain A. The Sat4j library, release 2.2 system description[J].Journal on Satisfiability,Boolean Modeling and Computation, 2010, 7: 59-64.