基于增量可满足性的等价性检验方法

• 作者: 李光辉 李晓维
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 组合电路 形式验证 等价性检验 增量可满足性
• 年，卷（期）: 2004,（10）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1388-1394
• 页数: 7页
• 分类号: TP391
• 字数: 5827字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2004.10.011

摘要

组合验证是数字集成电路形式化设计验证的重要方面.该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等价结点和增量可满足性算法来提高算法性能,并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式,避免了误判的发生,又能缩小验证程序的搜索空间.针对ISCAS'85电路的实验结果表明,该文提出的方法比以往同类方法更快、更强健.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李晓维	中国科学院计算技术研究所	127	1467	20.0	32.0
5	李光辉	浙江林学院信息工程学院	17	172	9.0	13.0