基于可满足性问题解算器的有界模型检验——子句规则和冲突分析研究

文摘

英文文摘

声明

第一章 绪论

1.1 集成电路发展与设计验证

1.2 NP完全问题与可满足性问题

1.3 模型检验

1.4 基于SAT的有界模型检验

1.5 本文的组织结构

第二章 可满足性问题和现代SAT解算器

2.1 SAT问题简介

2.2 基本定义

2.2.1布尔代数

2.2.2 基于合取范式的可满足性问题

2.3 DPLL算法

2.4 现代SAT解算器

2.5 小结

第三章有界模型检验

3.1 Kripke结构和时态逻辑

3.1.1 系统建模：Kripke结构

3.1.2 属性表示：时态逻辑

3.2有界模型检验

3.2.1 时态逻辑的界限语义

3.2.2 有界模型检验问题到SAT问题的转化

3.3 小结

第四章BMC问题的子句规则研究和改进

4.1 基本定义

4.2 重命名子句规则

4.3 改进的子句规则

4.3.1 节点分类

4.3.2逻辑化简

4.3.3 处理多元运算

4.3.4合并相邻节点

4.3.5 时间复杂度和可满足性等价证明

4.4 实验结果与分析

4.5 小结

第五章BMC问题的冲突分析研究和改进

5.1引言

5.2 基于第一个唯一蕴涵点的冲突分析

5.3 增强的冲突分析

5.4 改进的冲突分析算法

5.4.1 BMC的冲突特征

5.4.2 改进的冲突分析算法

5.4.3 时间复杂度和空间复杂度分析

5.4.4 辅助学习子句对SAT解算器的影响

5.5实验结果与分析

5.6 小结

第六章总结与展望

6.1总结

6.2展望

参考文献

致谢