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

作     者：郑飞君 严晓浪 葛海通 杨军 Zheng Fei-jun;YAN Xiao-lang;GE Hai-tong;Yang Jun

作者机构：浙江大学超大规模集成电路设计研究所杭州310027 

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

出 版 物：《电子与信息学报》 (Journal of Electronics & Information Technology)

年 卷 期：2005年第27卷第4期

页      码：651-654页

摘      要：该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了 与／非 图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆 炸,推理简化减小了SAT搜索空间。ISCAS85电路实验结果表明了本算法的有效性。

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

学科分类：080903[080903] 0809[工学-计算机类] 08[工学] 

核心收录：

馆 藏 号：203839471...