| 摘要 | 第1-4页 |
| 英文摘要 | 第4-5页 |
| 目录 | 第5-8页 |
| 图目录 | 第8-9页 |
| 表目录 | 第9-10页 |
| 第一章 引言 | 第10-18页 |
| ·课题背景 | 第10-13页 |
| ·日益复杂的集成电路设计 | 第10-11页 |
| ·仿真验证方法的不足 | 第11-12页 |
| ·形式化方法处理能力的局限性 | 第12页 |
| ·半形式化验证方法的引入 | 第12-13页 |
| ·半形式化验证方法简介 | 第13-15页 |
| ·半形式化验证方法的原理 | 第13页 |
| ·状态迁移策略 | 第13页 |
| ·形式化分析引擎 | 第13-15页 |
| ·显式模型检验方法 | 第14-15页 |
| ·基于BDD(决策图)的模型检验方法 | 第15页 |
| ·基于SAT(可满足性判定)的模型检验方法 | 第15页 |
| ·基于符号仿真的模型检验方法 | 第15页 |
| ·本文工作 | 第15-16页 |
| ·本文组织 | 第16-18页 |
| 第二章 基于SAT—BMC的半形式化验证 | 第18-34页 |
| ·SAT—BMC的半形式化验证系统的总体设计 | 第18-19页 |
| ·被验证系统的模型化 | 第19-21页 |
| ·Kripke结构 | 第19-20页 |
| ·SMV符号模型检验语言简介 | 第20-21页 |
| ·RTL直接模型化 | 第21页 |
| ·系统规范的描述 | 第21-23页 |
| ·CTL公式语法 | 第21-22页 |
| ·CTL公式语义 | 第22-23页 |
| ·LTL公式语法 | 第23页 |
| ·一个CTL描述系统规范的例子 | 第23页 |
| ·SAT—BMC形式化引擎 | 第23-34页 |
| ·布尔公式的SAT判定方法 | 第24-27页 |
| ·布尔公式判定问题到SAT问题的转化 | 第24页 |
| ·布尔公式的CNF表示 | 第24-25页 |
| ·布尔SAT算法 | 第25-27页 |
| ·数学公式的SAT判定算法 | 第27-29页 |
| ·数学公式判定问题到SAT问题的转化 | 第27页 |
| ·数学公式的E-CNF表示 | 第27-28页 |
| ·支持E-CNF表示的SAT算法 | 第28页 |
| ·支持运算逻辑的布尔约束传输过程 | 第28-29页 |
| ·NuSMV形式化分析工具简介 | 第29-31页 |
| ·SAT—BMC形式化分析实例 | 第31-34页 |
| 第三章 浮点乘加部件的半形式化验证 | 第34-44页 |
| ·FMAF结构介绍 | 第34-35页 |
| ·FMAF的整体结构 | 第34-35页 |
| ·FMAF的模型化 | 第35-36页 |
| ·FMAF的规范描述 | 第36-39页 |
| ·FMAF的例外处理 | 第36-37页 |
| ·FMAF的舍入 | 第37-39页 |
| ·基准浮点乘加部件(Reference FMAF) | 第39-44页 |
| 第四章 浮点乘加部件的初步验证结果 | 第44-56页 |
| ·浮点乘加部件整体验证 | 第44-47页 |
| ·基于BDD的浮点乘加部件的整体验证 | 第44-45页 |
| ·基于SAT—BMC浮点乘加部件整体验证 | 第45-46页 |
| ·基于BDD与SAT—BMC的比较分析 | 第46-47页 |
| ·浮点乘加部件的状态分割 | 第47-50页 |
| ·分割后的部分验证结果 | 第50-52页 |
| ·浮点乘加部件半形式化验证结果总结 | 第52页 |
| ·半形式化方法和仿真方法结果比较 | 第52-56页 |
| 第五章 总结与展望 | 第56-58页 |
| ·总结 | 第56-57页 |
| ·进一步的工作 | 第57-58页 |
| 参考文献 | 第58-61页 |
| 致谢 | 第61-62页 |
| 作者简历 | 第62页 |