结合二叉判决图和布尔可满足性的等价性验证算法

• 作者: 严晓浪 杨军 葛海通 郑飞君
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 等价性验证 与/非图 孤立节点 二叉判决图 可满足性解算器
• 年，卷（期）: 2004,（8）
• 所属期刊栏目: 学术论文
• 页码范围: 1233-1235
• 页数: 3页
• 分类号: TN4
• 字数: 3035字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2004.08.001

摘要

本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术.算法是在与/非图AIG中进行推理,并交替使用BDD扩展和基于电路SAT解算器简化电路.如尚未解决,将用基于合取范式SAT解算器进行推理.与已有算法相比主要有如下改进:在AIG中结合多种引擎进行简化,不存在误判可能;充分利用了基于电路解算器和基于合取范式解算器各自优点,减小了SAT推理的搜索空间.实验结果表明了本算法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨军	浙江大学超大规模集成电路设计研究所	59	513	11.0	19.0
2	严晓浪	浙江大学超大规模集成电路设计研究所	246	1634	19.0	29.0
3	葛海通	浙江大学超大规模集成电路设计研究所	52	293	8.0	14.0
4	郑飞君	浙江大学超大规模集成电路设计研究所	8	114	5.0	8.0