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

SAT-based Algorithm for Generating Test Set of Reversible Circuits

作　　者：李明翠[1] 周日贵[1] 

机构地区：[1]华东交通大学信息学院,江西南昌330013

出　　处：《华东交通大学学报》2014年第6期87-92,共6页Journal of East China Jiaotong University

基　　金：国家自然科学基金项目(61340029;61462026);江西省教育厅青年科学基金项目(GJJ14395);江西省科技厅对外科技合作项目(20141BDH80007);江西省教育厅科技项目(KJLD14037)

摘　　要：可逆逻辑是量子计算的基本特征,也是日益突出的低能耗需求的一种解决方案。根据可逆电路的可控制性和可观测性,论文提出了一种基于逻辑可满足性的算法来自动产生单门失效错误的完备检测集。基于k-NOT门的可逆逻辑线路中的数据传输进行线性建模,用线性时态逻辑描述单门失效错误约束,运用SAT求解器寻求反例的方法自动生成可逆电路的错误检测集。实验结果显示,本方法能够有效的应用于不规则和复杂的基于k-NOT门的可逆逻辑线路,自动化程度高。Reversible logic is the basic feature of quantum computing, and is also a solution to the increasingly prominent low energy demand. According to the controllability and observability of reversible circuits, this paper presents a novel algorithm which is based on the logic satisfiability to generate the complete test set automatically for single missing-gate fault in reversible circuits. The data transmissions of reversible logic circuits based on k-NOT gates are linear modeled, and the constraint of single missing-gate faults are described by linear temporal logic. The test sets are generated automatically by applying the circuit models and the fault constraints to the SAT solver to obtain the counterexample. Experimental results show that this method can generate test set effectively with high degree of automation for irregular and complex reversible logic circuit based on k-NOT gates.

关 键 词：可逆 量子 SAT 门失效 错误检测 

分 类 号：TP387[自动化与计算机技术—计算机系统结构] TP306.2[自动化与计算机技术—计算机科学与技术]