| 摘要 | 第1-3页 |
| ABSTRACT | 第3-6页 |
| 第一章 绪论 | 第6-12页 |
| §1．1 集成电路发展及设计验证 | 第6-8页 |
| §1．2 NP完全问题 | 第8页 |
| §1．3 本文研究背景及出发点 | 第8-10页 |
| §1．4 本文研究重点 | 第10页 |
| §1．5 论文的组织结构 | 第10-12页 |
| 第二章 基础知识 | 第12-19页 |
| §2．1 布尔代数 | 第12-13页 |
| §2．2 集合与布尔函数 | 第13-14页 |
| §2．3 二分决策图(BDD) | 第14-15页 |
| §2．4 逻辑范式、电路与可满足性问题(SAT) | 第15-19页 |
| 第三章 可满足性问题算法的发展 | 第19-33页 |
| §3．1 历史综述 | 第19-21页 |
| §3．2 DPLL算法 | 第21-22页 |
| §3．3 加速搜索过程的启发式策略 | 第22-29页 |
| §3．3．1 布尔约束传递过程(BCP，Boolean Constraint Propagation) | 第22-23页 |
| §3．3．2 基于冲突的学习过程和非同步回溯 | 第23-26页 |
| §3．3．3 决策变量选择策略 | 第26-28页 |
| §3．3．4 学习子句的删除 | 第28-29页 |
| §3．3．5 随机重新启动 | 第29页 |
| §3．4 数据结构 | 第29-32页 |
| §3．5 小结 | 第32-33页 |
| 第四章 高级推理过程—FLD算法研究 | 第33-43页 |
| §4．1 高级推理过程简述 | 第33-34页 |
| §4．2 FLD算法 | 第34-35页 |
| §4．3 动态筛选策略 | 第35-37页 |
| §4．4 结合FLD的DPLL算法流程 | 第37-38页 |
| §4．5 实验结果与分析 | 第38-42页 |
| §4．6 小结 | 第42-43页 |
| 第五章 不可满足子集提取 | 第43-47页 |
| §5．1 不可满足子集 | 第43页 |
| §5．2 基于DPLL算法的不可满足子集提取算法简述 | 第43-47页 |
| 第六章 时序电路等价验证综述 | 第47-56页 |
| §6．1 时序电路模型及等价验证层次 | 第47-48页 |
| §6．2 时序电路等价定义 | 第48-50页 |
| §6．3 基于状态遍历的等价验证算法 | 第50-53页 |
| §6．4 BDD引擎vs SAT引擎 | 第53-55页 |
| §6．5 小结 | 第55-56页 |
| 第七章 基于时间帧展开的时序电路等价验证算法 | 第56-72页 |
| §7．1 引言 | 第56-57页 |
| §7．2 数学归纳法思想 | 第57-59页 |
| §7．3 基于时间帧展开的等价验证算法 | 第59-66页 |
| §7．4 实验结果与分析 | 第66-70页 |
| §7．5 小结 | 第70-72页 |
| 第八章 总结和展望 | 第72-74页 |
| §8．1 论文工作总结 | 第72-73页 |
| §8．2 今后工作展望 | 第73-74页 |
| 参考文献 | 第74-81页 |
| 附录 | 第81-88页 |
| §附录一：FDSAT程序部分伪代码 | 第81-84页 |
| §附录二：FESD程序部分伪代码 | 第84-88页 |
| 致谢 | 第88-89页 |