应用不可满足子式地解码电路综合优化方法（.docVIP

应用不可满足子式解码电路综合( 张建民黎铁军马柯帆肖立权 （国防科学技术大学 ，湖南 长沙 410073） 摘要：解释布尔公式的不可满足的原因在很多领域都具有实际的应用需求而最小不可满足子式能够为诸如电路的自动综合等应用领域中的不可满足原因提供最的解释。因此，将两种高效求解最小不可满足子式的算法：分支-限界算法与贪心遗传算法，集成到电路自动综合工具中。采用通信领域的标准编码电路作为测试集，将两种算法进行了对比。实验结果表明，在运行时间与每秒剔除的短句数方面，贪心遗传算法优于分支-限界算法并实验说明了不可满足子式在解码电路的自动综合过程中的重要作用。 关键词：电路综合；形式化方法；可满足性求解；不可满足子式 中图分类号：TP391 文献标志码：　　　文章编号： Optimization method of decoding circuits’ synthesis using unsatisfiable subformulas ZHANG Jianmin, LI Tiejun, MA Kefan, XIAO Liquan (College of Computer, National University of Defense Technology, Changsha 410073, China) Abstract: Explaining the causes of unsatisfiability of the Boolean formulas has many real applications in various fields. The minimum unsatisfiable subformulas can provide most accurate explanation for the causes of infeasibility in many application fields such as the automatic circuits’ synthesis. Two best algorithms of extracting the minimum unsatisfiable subformulas, respectively called the branch-and-bound algorithm and greedy genetic algorithm, are integrated in the decoding circuits’ synthesis tool. Adopted the standard encoding circuits in communication fields as the benchmarks, the two algorithms are compared and analyzed. The experimental results show that the greedy genetic algorithm outperforms the branch-and-bound algorithm on runtime and removed clauses per second. The results also show that the unsatisfiable subformulas plays an important role in process of synthesizing automatically the decoding circuits. Keywords: circuit synthesis; formal method; satisfiability solving; unsatisfiable subformula 在超大规模集成电路 Large Scale Integrated）中，都会各样的编码和解码电路，尤其是与通信相关的芯片设计过程中，往往会遇到很多非常复杂的编码与解码电路。某种规则将原始数据编码或产生校验码常见的校验 Redundancy Code，CRC）或码Error Correction Code，ECC），而解码电路根据原始数据判定的数据是否正确。这些电路需要消耗设计者大量的时间进行验证，那么，能否只设计与验证编码电路，而后通过一种自动化的方法来产生正确的解码电路，从而降低设计者的工作量？因此，产生了自动对偶综合工具[1]。自动对偶综合的基本思路是：给出一个已验证的编码电路，通过形式化的方法自动综合出一个功能正确的解码电路。对偶综合工具是通过分析特定编码电路的状态空间，自动产生相应的解码电路，避免设计人员将时间花费在设计解码器上，从而降低芯片设计的风险，并加速设计进程。而在对偶综合工具中，使用不可满足