使用布尔可满足性的组合电路等价性验证算法  

Using Boolean Satisfiability for Combinational Equivalence Checking

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

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

出　　处：《电子与信息学报》2005年第4期651-654,共4页Journal of Electronics & Information Technology

基　　金：国家自然科学基金(90207002)资助课题

摘　　要：该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了'与／非'图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆 炸,推理简化减小了SAT搜索空间。ISCAS85电路实验结果表明了本算法的有效性。In this paper, a new combinational equivalence checking approach using Boolean Satisfiability is proposed. The algorithm uses several methods to reduce the space of the SAT reasoning first, those methods are AND/INVERTER graph transformation, BDD propagation and implication learning, CNF-based SAT solver zChaff is used to solve the verification task. The algorithm combines the advantages of both BDD and SAT, BDD's size is limited to avoid memory explosion problem and structural reduction is applied to reduce the search space of SAT. The efficiency of the proposed approach is shown through its application on the ISCAS85 benchmark circuits.

关 键 词：等价性验证 与/非图 可满足性解算器 隐含学习 

分 类 号：TN402[电子电信—微电子学与固体电子学]