使用输出分组和电路可满足性的等价性验证算法  

Efficient Equivalence Checking Using Output Grouping and Circuit SAT Solver

作　　者：郑飞君[1] 严晓浪[1] 葛海通[1] 杨军[1] 卢永江[1] 

机构地区：[1]浙江大学超大规模集成电路设计研究所,杭州310027

出　　处：《计算机辅助设计与图形学学报》2005年第11期2484-2488,共5页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(90207002)

摘　　要：介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的.A new combinational equivalence checking technique using Circuit SAT is proposed in the paper. By the algorithm, a heuristic is used to do output grouping for complex problem first, then the equivalence checking problem is converted into some Circuit SAT problems. To reduce the search space, useful learned information of some sub-problem is shared. Experimental results show the efficiency of the proposed algorithm.

关 键 词：等价性验证 输出分组 电路可满足性 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]