基于SAT的可逆线路检测集生成算法

李明翠，周日贵

（华东交通大学信息学院，江西 南昌330013）

能耗和散热是电子产品功能越来越复杂、体积越来越小发展过程中日益突出的问题。由于可逆线路的低能耗特性，可逆线路被认为为未来量子计算、纳米技术以及低功耗COMS等领域的一种解决方案。计算机每擦除一位信息就会释放至少kT ln 2 J的热量（k是波尔兹曼常数1.38×10-23，T是计算时的绝对温度）［1］。不可逆电路中的能量消耗与在计算过程中擦除的信息位数乘正比。而可逆线路要求在计算过程中保持输入和输出的一一对应关系，因此可逆计算没有信息丢失。Bennett［2］指出如果所有的运算都是用可逆部件完成的话，零能耗将成为可能。Barenco等［3］指出任何的运算在逻辑上和热力学上都可以以可逆的方式进行。另一方面，由于量子物理学中的酉变换是可逆的，因此，可逆线路是量子力学中的最基本部分。从可逆门的设计到加法器及各种可逆电路的合成，国内外学者进行了很多相关的研究［4-7］。为了保证电路的正确性，在电路设计过程中和设计后的错误检测非常重要。可逆电路的错误模型和检测集生成方法与传统电路存在很大的不同。目前提出的可逆线路错误模型主要有：固定点错误模型、单门失效模型、门重复错误模型、多门失效错误模型、门部分控制点失效等模型。Patel［8］提出的错误检测集产生方法（ILP），Ramasamy［9］提出的基于错误表的适应树方法，以及文献［10-13］设计的基于奇偶保持的可逆容错线路，都是针对可逆电路的固定点错误模型。然而，在可逆线路中，更能体现整个电路是否实现了目标功能的是门错误模型。Polian等人［14］用离子阱技术通过激光脉冲作用于离子的方式模拟了基于k-NOT 门的可逆电路的单门失效（SMGF）、门重复（RGF）、连续位置的多门失效（MMGF和门部分失效（PMGF）错误模型。Hayes等［15］提出了基于k-NOT 门的门失效错误模型（MGF）检测方法DFT。DFT 方法是在原有线路中增加一条传输线和多个受控非门，这种方法的优点是仅用一个检测向量就能检测整个线路中是否存在单个门错误，但其缺点也很明显：为了辅助错误检测而增加的多个受控非门本身也可能产生新的错误，这些门一旦产生错误，DFT方法的优点将不复存在。肖芳英等人［16］提出了根据门间占据关系检测单门失效的错误完备测试集算法CTS，这种方法不适于复杂的不规则电路。Zhang［17］提出了用向量反复迭代的方式获得单门失效最小测试集的方法，其缺点是每生成一个测试向量都要用该向量对剩余错误进行迭代检测。Kole［18］提出了连续位置门失效问题测试集的生成算法。以下根据SAT可满足性原理着重研究基于k-NOT 门的可逆电路的单门失效错误检测集的自动产生方法。

1 可逆电路中的单门失效错误模型

可逆电路的输入和输出具有一一对应的双射关系，n位输入的可逆电路必有n位输出，常用n×n表示具有n位输入和n位输出的可逆电路。一个n×n的可逆电路的真值表具共有2n行输入和2n行输出。对于基本的二进制位输入，可逆电路的输出是输入的某个排列置换。可逆电路从左到有对信息进行线性转换，每向右边增加一次转换称为深度增加1。k-NOT 门是组成可逆电路的最常用基本门。一个k-NOT门有k个控制位c1,c2,...ck和一个目标位t，实现的是一个(k+1)×(k+1)的酉变换。k-NOT 门的逻辑功能为即控制位的输入与输出相同，当所有的控制位的输入都为1时，目标位的输出与输入相反。其中0-NOT 相当于一个反向器（NOT），输出与输入相反，1-NOT 也叫控制非门（CNOT），2-NOT 门也叫Toffoli门。图1描述了这三种门的逻辑表示方式，其中门的控制位用·表示，目标位用⊕表示。

图1 三种基本可逆门Fig.1 Three elementary reversible gates

单门失效错误（SMGF）指的是电路中的一个k-NOT门的功能完全消失，其所在位置相当于传输线直接连通的效果。实现该门的激光脉冲太短或者消失或没有调整到位都可能是造成SMGF的物理原因。可逆线路具有非可逆线路所没有的两个重要特征可控制性和可观测性。可控制性是指，存在一个检测向量能产生电路中任意指定位置所需要的状态，即在电路的某个深度指定的任意状态都有一个对应的输入向量。可观察性指任何一个改变某个中间状态的错误也同时改变输出。根据可控性和可观测性，一个SMGF可以通过设置失效门的所有控制点输入为1，其他输入是0或1来检测。图2（电路来源于可逆电路测试网站http：//www.cs.uvic.ca/～dmaslov）描述了虚线框中的2-NOT门失效的SMGF错误。在图2的例子中，如果输入{in1,in2,in3}={0,1,1}，正确的输出应该是{out1,out2,out3}={1,0,0}，然而，当虚线框中的SMGF发生后输出变成了{out1,out2,out3}={0,1,1}。线路中可能的SMGF数量与线路中门的数量相等。

图2 单门失效错误（SMGF）Fig.2 Single missing-gate fault（SMGF）

2 基于SAT的单门失效错误完备检测集生成算法

布尔可满足性问题（SAT）是指对给定的一个包含k个布尔变量的逻辑函数h，确定是否存在这n个变量的一组取值组合，使得h的值为1或者证明不存在使得h为1的取值组合。如果赋值组合存在则称为可满足（SAT），否则，称为不可满足（UNSAT）。SAT问题是计算机理论界和逻辑学界共同关注的重大问题，被广泛的应用于自动规划、模型诊断和电路等价性等方面的研究。SMGF问题可以转化为这样一个SAT问题“是否存在这样一个输入向量，使得k-NOT 门gj的所有控制位输入为1，1 ≤j≤m，m是线路中的k-NOT 总数”。用NuSMV模型检测器检测指定的可逆线路是否满足某个线性属性。

2.1 可逆线路中的数据传输建模

给定一个具有n条传输线和m个k-NOT 门的可逆线路。假定所有的初始输入为基本的二进制输入0和1，则n位的0和1的组合沿着传输线从左到右依次经过m个可逆门进行传输和转化。将电路中的n位数据用向量A=a1a2…an表示，A每经过一个k-NOT 门，状态会发生改变，我们用aj i表示第i位数据经过第j个门后的状态，用gj表示第j个门，1 ≤i≤n，1 ≤j≤m。则aj i的转化可以用数学公式（1）描述。公式（1）表示n位信息经过gj后，只有gj的目标位所在的传输线中的信息会发生变化，其余信息位不变。

例如图3中可逆线路Ham3中的信息转化关系为

图3 Ham3中的信息传输Fig.3 Data transformation in reversible circuit Ham3

2.2 SMGF错误约束

m个k-NOT 门组成的可逆线路有m个可能的SMGF错误。根据线路中门的输入输出关系，将m个可逆门生成m个数据转化实例gc1,gc2,…,gcm。这m个实例的数据输入输出关系用公式（3）描述，其中gcj+1.in[i] ，是第j+1（1 ≤j≤m-1，1 ≤i≤n）个层次（深度）的输入向量，gcj.out[i]是经过第前j个层次的k-NOT 门后得到的输出。

一个SMGF的错误检测可以约束为将该失效门的所有控制点输入为设置为1。例如图3中的编号为2的CNOT门的错误检测约束为a13=1，即gc1.out[3]=1。同理编号为4的CNOT门的错误检测约束为a13=1，即gc3.out[1]=1。公式（4）用线性时态逻辑（LTL）描述了第j+1个k-NOT门的错误约束的反，用来表示指定线路不存在满足指定公式的属性，其中p,q,…,r∈Cj+1，Cj+1是第j+1个k-NOT门的控制点集合。

根据公式（4），图3的Ham3线路中5个单门失效错误约束取反可以描述如下

将数据传输模型和错误约束LTL公式输入SAT检测器NuSMV，得到的反例就是每个错误的输入检测向量。Ham3 根据公式（1）～（5）得到的一组检测集向量为（011，111，101，011，101），合并后得到（011，111，101），因此（011，111，101）是图3所示Ham3的SMGF完备检测集。

3 实验结果分析

可逆线路单门失效错误检测集生成算法实验结果如表1所示。

表1 文章所提出方法的实验结果Tab.1 Experiment results of the proposed method

实验所用线路全部来自可逆线路测试网站（http：//www.cs.uvic.ca/～dmaslov）。表中第1 列是所选用的可逆线路名称，第2列是线路的传输线数目，第3列是线路中包含的可逆门数目，第4列是用本文提出的方法得到的完备检测集大小，第五列是具体的检测集，其中所有的检测向量都已转换为十进制数，其对应的二进制数从高位到低位对应于线路的传输线1,2,…,n的输入。实验结果显示本方法对于无规则线路和复杂线路均有效。

在检测过程中，由于NOT门可以被任意输入向量检测到，因此在检测集生成时可以忽略NOT门的检测向量生成。对输入有特殊限制的电路（例如Mod5d1的最后一根输入线要求是1，Gf2^4mult 的最后四根线的输入要求为常量0），可以将错误约束LTL 公式进行特征约束扩展，将公式（4）扩展成公式（6），其中a0是电路最左端的初始输入，u,...,v∈{1,2,3,...,n}是对输入有特殊限制的传输线编号，w根据具体线路的输入限制取0或1。

4 总结

可逆线路的可控制性保证了可以求得任意指定层次数据对应的原始输入向量，可观测性保证了任意层次数据的改变将直接反应到输出结果。根据可控性和可观测性，将检测向量生成问题转化为求解逻辑可满足问题，通过在k-NOT 门的对应层次上指定其所有控制位输入为1的约束条件来获得对应的检测向量。将逻辑线路的数据转化抽象成线性逻辑公式，用线性时态逻辑LTL描述所求问题的反，通过求反例的方式来自动生成整个可逆电路的完备单门失效错误检测集。用可逆线路网站上的部分线路检测提出的方法，实验结果显示此方法能够很好的产生完备检测集，自动化程度高，能应对不规则的复杂线路，易于针对线路的特殊属性进行扩展。

[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] 黎海生,周日贵.在纠缠量子系统中的图像几何形状存储和检索[J].华东交通大学学报,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] 肖芳英,陈汉武,李志强.量子电路中门失效错误的检测方法[J].仪器仪表学报,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.