结合模拟蕴含技术的电路验证方法

• 作者: 唐璞山 柯宪明
• 来源期刊: 微电子学与计算机
• 关键词: 等价验证 模拟蕴含学习 可满足性问题
• 年，卷（期）: 2007,（2）
• 页码范围: 58-61
• 页数: 4页
• 分类号: TP302
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2007.02.017

摘要

提出了一种改进现有基于SAT的组合电路验证方法的新技术.主要创新在于提出了对CUVs的模拟蕴含学习方法,能快速地将许多间接的蕴含关系转化成子句.将这些子句加入原有的CNF表达数据中,可以减少SAT解决器的搜索空间并且加速BCP过程.对于ISCAS测试电路的实验可以看出该方法比常规算法有着近一个数量级的速度提升.