基于深度优先搜索与增量式求解的极小一阶不可满足子式提取算法

• 作者: 张峻 张建民 徐炜遐 李思昆 黎铁军
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 形式化验证 硬件错误定位 可满足性模理论 极小不可满足子式
• 年，卷（期）: 2012,（5）
• 所属期刊栏目: 计算机科学与技术·数学与系统科学
• 页码范围: 121-126
• 分类号: TP391
• 字数: 5962字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2486.2012.05.023

摘要

随着寄存器传输级甚至行为级的硬件描述语言应用越来越广泛,基于一阶逻辑的可满足性模理论(Satisfiability Modulo Theories,SMT)逐渐替代布尔可满足性(Boolean Satisfiability,SAT),在VLSI形式化验证领域具有更加重要的应用价值.而极小不可满足子式能够帮助EDA工具迅速定位硬件中的逻辑错误.针对极小SMT不可满足子式的求解问题,采用深度优先搜索与增量式求解策略,提出了深度优先搜索的极小SMT不可满足子式求解算法.与目前最优的宽度优先搜索算法对比实验表明:该算法能够有效地求解极小不可满足子式,随着公式的规模逐渐增大时,深度优先搜索算法优于宽度优先搜索算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科技大学计算机学院	100	974	16.0	27.0
2	张建民	国防科技大学计算机学院	11	15	2.0	3.0
3	黎铁军	国防科技大学计算机学院	13	39	4.0	6.0
4	张峻	国防科技大学计算机学院	6	13	2.0	3.0
5	徐炜遐	国防科技大学计算机学院	20	52	4.0	6.0