李明翠，周日貴

（華東交通大學(xué)信息學(xué)院，江西 南昌330013）

能耗和散熱是電子產(chǎn)品功能越來越復(fù)雜、體積越來越小發(fā)展過程中日益突出的問題。由于可逆線路的低能耗特性，可逆線路被認(rèn)為為未來量子計算、納米技術(shù)以及低功耗COMS等領(lǐng)域的一種解決方案。計算機(jī)每擦除一位信息就會釋放至少kT ln 2 J的熱量（k是波爾茲曼常數(shù)1.38×10-23，T是計算時的絕對溫度）［1］。不可逆電路中的能量消耗與在計算過程中擦除的信息位數(shù)乘正比。而可逆線路要求在計算過程中保持輸入和輸出的一一對應(yīng)關(guān)系，因此可逆計算沒有信息丟失。Bennett［2］指出如果所有的運算都是用可逆部件完成的話，零能耗將成為可能。Barenco等［3］指出任何的運算在邏輯上和熱力學(xué)上都可以以可逆的方式進(jìn)行。另一方面，由于量子物理學(xué)中的酉變換是可逆的，因此，可逆線路是量子力學(xué)中的最基本部分。從可逆門的設(shè)計到加法器及各種可逆電路的合成，國內(nèi)外學(xué)者進(jìn)行了很多相關(guān)的研究［4-7］。為了保證電路的正確性，在電路設(shè)計過程中和設(shè)計后的錯誤檢測非常重要。可逆電路的錯誤模型和檢測集生成方法與傳統(tǒng)電路存在很大的不同。目前提出的可逆線路錯誤模型主要有：固定點錯誤模型、單門失效模型、門重復(fù)錯誤模型、多門失效錯誤模型、門部分控制點失效等模型。Patel［8］提出的錯誤檢測集產(chǎn)生方法（ILP），Ramasamy［9］提出的基于錯誤表的適應(yīng)樹方法，以及文獻(xiàn)［10-13］設(shè)計的基于奇偶保持的可逆容錯線路，都是針對可逆電路的固定點錯誤模型。然而，在可逆線路中，更能體現(xiàn)整個電路是否實現(xiàn)了目標(biāo)功能的是門錯誤模型。Polian等人［14］用離子阱技術(shù)通過激光脈沖作用于離子的方式模擬了基于k-NOT 門的可逆電路的單門失效（SMGF）、門重復(fù)（RGF）、連續(xù)位置的多門失效（MMGF和門部分失效（PMGF）錯誤模型。Hayes等［15］提出了基于k-NOT 門的門失效錯誤模型（MGF）檢測方法DFT。DFT 方法是在原有線路中增加一條傳輸線和多個受控非門，這種方法的優(yōu)點是僅用一個檢測向量就能檢測整個線路中是否存在單個門錯誤，但其缺點也很明顯：為了輔助錯誤檢測而增加的多個受控非門本身也可能產(chǎn)生新的錯誤，這些門一旦產(chǎn)生錯誤，DFT方法的優(yōu)點將不復(fù)存在。肖芳英等人［16］提出了根據(jù)門間占據(jù)關(guān)系檢測單門失效的錯誤完備測試集算法CTS，這種方法不適于復(fù)雜的不規(guī)則電路。Zhang［17］提出了用向量反復(fù)迭代的方式獲得單門失效最小測試集的方法，其缺點是每生成一個測試向量都要用該向量對剩余錯誤進(jìn)行迭代檢測。Kole［18］提出了連續(xù)位置門失效問題測試集的生成算法。以下根據(jù)SAT可滿足性原理著重研究基于k-NOT 門的可逆電路的單門失效錯誤檢測集的自動產(chǎn)生方法。

1 可逆電路中的單門失效錯誤模型

可逆電路的輸入和輸出具有一一對應(yīng)的雙射關(guān)系，n位輸入的可逆電路必有n位輸出，常用n×n表示具有n位輸入和n位輸出的可逆電路。一個n×n的可逆電路的真值表具共有2n行輸入和2n行輸出。對于基本的二進(jìn)制位輸入，可逆電路的輸出是輸入的某個排列置換?？赡骐娐窂淖蟮接袑π畔⑦M(jìn)行線性轉(zhuǎn)換，每向右邊增加一次轉(zhuǎn)換稱為深度增加1。k-NOT 門是組成可逆電路的最常用基本門。一個k-NOT門有k個控制位c1,c2,...ck和一個目標(biāo)位t，實現(xiàn)的是一個(k+1)×(k+1)的酉變換。k-NOT 門的邏輯功能為即控制位的輸入與輸出相同，當(dāng)所有的控制位的輸入都為1時，目標(biāo)位的輸出與輸入相反。其中0-NOT 相當(dāng)于一個反向器（NOT），輸出與輸入相反，1-NOT 也叫控制非門（CNOT），2-NOT 門也叫Toffoli門。圖1描述了這三種門的邏輯表示方式，其中門的控制位用·表示，目標(biāo)位用⊕表示。

圖1 三種基本可逆門Fig.1 Three elementary reversible gates

單門失效錯誤（SMGF）指的是電路中的一個k-NOT門的功能完全消失，其所在位置相當(dāng)于傳輸線直接連通的效果。實現(xiàn)該門的激光脈沖太短或者消失或沒有調(diào)整到位都可能是造成SMGF的物理原因。可逆線路具有非可逆線路所沒有的兩個重要特征可控制性和可觀測性。可控制性是指，存在一個檢測向量能產(chǎn)生電路中任意指定位置所需要的狀態(tài)，即在電路的某個深度指定的任意狀態(tài)都有一個對應(yīng)的輸入向量?？捎^察性指任何一個改變某個中間狀態(tài)的錯誤也同時改變輸出。根據(jù)可控性和可觀測性，一個SMGF可以通過設(shè)置失效門的所有控制點輸入為1，其他輸入是0或1來檢測。圖2（電路來源于可逆電路測試網(wǎng)站http：//www.cs.uvic.ca/～dmaslov）描述了虛線框中的2-NOT門失效的SMGF錯誤。在圖2的例子中，如果輸入{in1,in2,in3}={0,1,1}，正確的輸出應(yīng)該是{out1,out2,out3}={1,0,0}，然而，當(dāng)虛線框中的SMGF發(fā)生后輸出變成了{(lán)out1,out2,out3}={0,1,1}。線路中可能的SMGF數(shù)量與線路中門的數(shù)量相等。

圖2 單門失效錯誤（SMGF）Fig.2 Single missing-gate fault（SMGF）

2 基于SAT的單門失效錯誤完備檢測集生成算法

布爾可滿足性問題（SAT）是指對給定的一個包含k個布爾變量的邏輯函數(shù)h，確定是否存在這n個變量的一組取值組合，使得h的值為1或者證明不存在使得h為1的取值組合。如果賦值組合存在則稱為可滿足（SAT），否則，稱為不可滿足（UNSAT）。SAT問題是計算機(jī)理論界和邏輯學(xué)界共同關(guān)注的重大問題，被廣泛的應(yīng)用于自動規(guī)劃、模型診斷和電路等價性等方面的研究。SMGF問題可以轉(zhuǎn)化為這樣一個SAT問題“是否存在這樣一個輸入向量，使得k-NOT 門gj的所有控制位輸入為1，1 ≤j≤m，m是線路中的k-NOT 總數(shù)”。用NuSMV模型檢測器檢測指定的可逆線路是否滿足某個線性屬性。

2.1 可逆線路中的數(shù)據(jù)傳輸建模

給定一個具有n條傳輸線和m個k-NOT 門的可逆線路。假定所有的初始輸入為基本的二進(jìn)制輸入0和1，則n位的0和1的組合沿著傳輸線從左到右依次經(jīng)過m個可逆門進(jìn)行傳輸和轉(zhuǎn)化。將電路中的n位數(shù)據(jù)用向量A=a1a2…an表示，A每經(jīng)過一個k-NOT 門，狀態(tài)會發(fā)生改變，我們用aj i表示第i位數(shù)據(jù)經(jīng)過第j個門后的狀態(tài)，用gj表示第j個門，1 ≤i≤n，1 ≤j≤m。則aj i的轉(zhuǎn)化可以用數(shù)學(xué)公式（1）描述。公式（1）表示n位信息經(jīng)過gj后，只有g(shù)j的目標(biāo)位所在的傳輸線中的信息會發(fā)生變化，其余信息位不變。

例如圖3中可逆線路Ham3中的信息轉(zhuǎn)化關(guān)系為

圖3 Ham3中的信息傳輸Fig.3 Data transformation in reversible circuit Ham3

2.2 SMGF錯誤約束

m個k-NOT 門組成的可逆線路有m個可能的SMGF錯誤。根據(jù)線路中門的輸入輸出關(guān)系，將m個可逆門生成m個數(shù)據(jù)轉(zhuǎn)化實例gc1,gc2,…,gcm。這m個實例的數(shù)據(jù)輸入輸出關(guān)系用公式（3）描述，其中g(shù)cj+1.in[i] ，是第j+1（1 ≤j≤m-1，1 ≤i≤n）個層次（深度）的輸入向量，gcj.out[i]是經(jīng)過第前j個層次的k-NOT 門后得到的輸出。

一個SMGF的錯誤檢測可以約束為將該失效門的所有控制點輸入為設(shè)置為1。例如圖3中的編號為2的CNOT門的錯誤檢測約束為a13=1，即gc1.out[3]=1。同理編號為4的CNOT門的錯誤檢測約束為a13=1，即gc3.out[1]=1。公式（4）用線性時態(tài)邏輯（LTL）描述了第j+1個k-NOT門的錯誤約束的反，用來表示指定線路不存在滿足指定公式的屬性，其中p,q,…,r∈Cj+1，Cj+1是第j+1個k-NOT門的控制點集合。

根據(jù)公式（4），圖3的Ham3線路中5個單門失效錯誤約束取反可以描述如下

將數(shù)據(jù)傳輸模型和錯誤約束LTL公式輸入SAT檢測器NuSMV，得到的反例就是每個錯誤的輸入檢測向量。Ham3 根據(jù)公式（1）～（5）得到的一組檢測集向量為（011，111，101，011，101），合并后得到（011，111，101），因此（011，111，101）是圖3所示Ham3的SMGF完備檢測集。

3 實驗結(jié)果分析

可逆線路單門失效錯誤檢測集生成算法實驗結(jié)果如表1所示。

表1 文章所提出方法的實驗結(jié)果Tab.1 Experiment results of the proposed method

實驗所用線路全部來自可逆線路測試網(wǎng)站（http：//www.cs.uvic.ca/～dmaslov）。表中第1 列是所選用的可逆線路名稱，第2列是線路的傳輸線數(shù)目，第3列是線路中包含的可逆門數(shù)目，第4列是用本文提出的方法得到的完備檢測集大小，第五列是具體的檢測集，其中所有的檢測向量都已轉(zhuǎn)換為十進(jìn)制數(shù)，其對應(yīng)的二進(jìn)制數(shù)從高位到低位對應(yīng)于線路的傳輸線1,2,…,n的輸入。實驗結(jié)果顯示本方法對于無規(guī)則線路和復(fù)雜線路均有效。

在檢測過程中，由于NOT門可以被任意輸入向量檢測到，因此在檢測集生成時可以忽略NOT門的檢測向量生成。對輸入有特殊限制的電路（例如Mod5d1的最后一根輸入線要求是1，Gf2^4mult 的最后四根線的輸入要求為常量0），可以將錯誤約束LTL 公式進(jìn)行特征約束擴(kuò)展，將公式（4）擴(kuò)展成公式（6），其中a0是電路最左端的初始輸入，u,...,v∈{1,2,3,...,n}是對輸入有特殊限制的傳輸線編號，w根據(jù)具體線路的輸入限制取0或1。

4 總結(jié)

可逆線路的可控制性保證了可以求得任意指定層次數(shù)據(jù)對應(yīng)的原始輸入向量，可觀測性保證了任意層次數(shù)據(jù)的改變將直接反應(yīng)到輸出結(jié)果。根據(jù)可控性和可觀測性，將檢測向量生成問題轉(zhuǎn)化為求解邏輯可滿足問題，通過在k-NOT 門的對應(yīng)層次上指定其所有控制位輸入為1的約束條件來獲得對應(yīng)的檢測向量。將邏輯線路的數(shù)據(jù)轉(zhuǎn)化抽象成線性邏輯公式，用線性時態(tài)邏輯LTL描述所求問題的反，通過求反例的方式來自動生成整個可逆電路的完備單門失效錯誤檢測集。用可逆線路網(wǎng)站上的部分線路檢測提出的方法，實驗結(jié)果顯示此方法能夠很好的產(chǎn)生完備檢測集，自動化程度高，能應(yīng)對不規(guī)則的復(fù)雜線路，易于針對線路的特殊屬性進(jìn)行擴(kuò)展。

[1] LANDAUER R.Irreversibility and heat generation in the computing process[J].IBM Journal of Research and Development, 1961,5(3):183-191.

[2] BENNETT C H.Logical reversibility of computation[J].IBM journal of Research and Development, 1973,17(6):525-532.

[3] BARENCO A,BENNETT CH,CLEVE R.Elementary gates for quantum computation[J].Canadian Metallurgical Quarterly, 1995,52(5):3457-3467.

[4] TOFFOLI T.Reversible computing[M].Berlin Heidelberg:Springer,1980:1-34.

[5] THAPLIYAL H, SRINIVAS M B.A novel reversible TSG gate and its application for designing reversible carry look-ahead and other adder architectures[M].Berlin Heidelberg:Springer,2005:805-817.

[6] 黎海生,周日貴.在糾纏量子系統(tǒng)中的圖像幾何形狀存儲和檢索[J].華東交通大學(xué)學(xué)報,2013,30(4):14-18.

[7] ZHOU RIGUI,ZHANG MAN QUN,WU QIAN,et al.Optimization approaches for designing a novel 4-bit reversible comparator[J].International Journal of Theoretical Physics,2013,52(2):559-575.

[8] PATEL K N, HAYES J P, MARKOV I L.Fault testing for reversible circuits[J].Computer-Aided Design of Integrated Circuits and Systems,IEEE Transactions on,2004,23(8):1220-1230.

[9] RAMASAMY K, TAGARE R, PERKINS E, et al.Fault localization in reversible circuits is easier than for classical circuits[C]//Proceedings of the International Workshop on Logic and Synthesis,June 2004.

[10] SAFARI P, HAGHPARAST M, AZARI A, et al.A design of fault tolerant reversible arithmetic logic unit[J].Life Science Journal,2012,9(3):643-646.

[11] BOROUMAND S,HAGHPARAST M.A novel nanometric fault tolerant reversible associative memory cell[J].Australian Journal of Basic and Applied Sciences,2011,5(10):945-950.

[12] MITRA S K,CHOWDHURY A R.Minimum cost fault tolerant adder circuits in reversible logic synthesis[C]//VLSI Design(VLSID),2012 25th International Conference.IEEE,2012:334-339.

[13] ZHOU R G,LI Y C,ZHANG M Q.Novel designs for fault tolerant reversible binary coded decimal adders[J].International Journal of Electronics,2014,101(10):1336-1356.

[14] POLIAN I, FIEHN T, BECKER B, et al.A family of logical fault models for reversible circuits[C]//Test Symposium, 2005 Proceedings 14th Asian.IEEE,2005:422-427.

[15] HAYES J P,POLIAN I,BECKER B.Testing for missing-gate faults in reversible circuits[C]//Test Symposium, 2004 13th Asian.IEEE,2004:100-105.

[16] 肖芳英,陳漢武,李志強(qiáng).量子電路中門失效錯誤的檢測方法[J].儀器儀表學(xué)報,2008,29(10):2084-2089.

[17] ZHANG H,FREHSE S,WILLE R,et al.Determining minimal testsets for reversible circuits using boolean satisfiability[C]//Africon.IEEE,2011:1-6.

[18] KOLE D K,RAHAMAN H,DAS D K,et al.Derivation of test set for detecting multiple missing-gate faults in reversible circuits[J].Computers and Electrical Engineering,2013,39(2):225-236.