| 摘要 | 第1-6页 |
| 目录 | 第6-10页 |
| 图目录 | 第10-12页 |
| 表目录 | 第12-14页 |
| 第一章 绪论 | 第14-26页 |
| ·引入形式化验证方法的必要性 | 第14-16页 |
| ·日益复杂的硬件系统设计 | 第14-15页 |
| ·设计缺陷带来的惨重代价 | 第15页 |
| ·仿真验证方法的局限性 | 第15-16页 |
| ·形式化方法综述 | 第16-24页 |
| ·定理证明方法 | 第17-18页 |
| ·模型检验方法 | 第18-24页 |
| ·运算电路验证方法研究的必要性 | 第24页 |
| ·本文研究内容与组织 | 第24-26页 |
| 第二章 运算电路的模型检验方法 | 第26-44页 |
| ·CTL公式的模型检验方法 | 第26-35页 |
| ·Kripke结构 | 第26-27页 |
| ·CTL公式语法 | 第27页 |
| ·CTL公式语义 | 第27-28页 |
| ·不动点理论(Fixpoint Theory) | 第28-30页 |
| ·CTL公式模型检验 | 第30页 |
| ·基于BDD的符号模型检验方法 | 第30-35页 |
| ·运算电路CTL公式的模型检验方法 | 第35-43页 |
| ·运算电路CTL公式语法 | 第35-36页 |
| ·运算电路CTL公式语义 | 第36页 |
| ·运算电路CTL的模型检验 | 第36-37页 |
| ·基于~*PHDD的运算电路模型检验方法 | 第37-43页 |
| ·本章小结 | 第43-44页 |
| 第三章 ~*PHDD的运算操作算法 | 第44-62页 |
| ·基于~*PHDD的运算操作算法一般优化原则 | 第44-45页 |
| ·基于~*PHDD的加法、乘法和幂函数等运算操作优化算法 | 第45-47页 |
| ·加法操作算法 | 第45-46页 |
| ·乘法操作算法 | 第46-47页 |
| ·幂函数操作算法 | 第47页 |
| ·整除和取模算法 | 第47-57页 |
| ·~*PHDD的整除和取模运算中余数符号定义 | 第48-49页 |
| ·基本算法 | 第49-50页 |
| ·简化规则、算法及性能分析 | 第50-55页 |
| ·性能测试结果 | 第55-57页 |
| ·上下界函数计算算法 | 第57-60页 |
| ·本章小结 | 第60-62页 |
| 第四章 条件模型检验方法 | 第62-74页 |
| ·条件模型检验方法的基本思想 | 第62-63页 |
| ·条件约束算法 | 第63-66页 |
| ·条件约束算法基本定理 | 第63-65页 |
| ·条件约束算法基本原理 | 第65-66页 |
| ·基于条件预处理的条件约束算法 | 第66-69页 |
| ·替换判定条件对条件约束算法的性能影响分析 | 第66-67页 |
| ·条件预处理对条件约束算法的性能影响分析 | 第67-68页 |
| ·基于条件预处理的条件约束算法描述 | 第68-69页 |
| ·条件过滤机制 | 第69-70页 |
| ·多级条件约束机制 | 第70-71页 |
| ·本章小结 | 第71-74页 |
| 第五章 基于SAT的运算电路验证方法 | 第74-84页 |
| ·布尔公式的SAT判定方法 | 第74-77页 |
| ·布尔公式判定问题到SAT问题的转化 | 第74-75页 |
| ·布尔公式的CNF表示 | 第75-76页 |
| ·布尔SAT算法 | 第76-77页 |
| ·数学公式的SAT判定算法 | 第77-80页 |
| ·数学公式判定问题到SAT问题的转化 | 第78页 |
| ·数学公式的E-CNF表示 | 第78-79页 |
| ·支持E-CNF表示的SAT算法 | 第79-80页 |
| ·SAT方法与决策图方法性能比较分析 | 第80-81页 |
| ·影响SAT方法性能的主要因素 | 第80页 |
| ·影响决策图方法性能的主要因素 | 第80-81页 |
| ·比较结果 | 第81页 |
| ·性能数据结果与分析 | 第81-82页 |
| ·本章小结 | 第82-84页 |
| 第六章 字级模型检验系统ArithSMV | 第84-90页 |
| ·SMV系统 | 第84-85页 |
| ·字级模型检验系统设计中的关键问题 | 第85-87页 |
| ·字变量与位变量的相互转化方法 | 第85-86页 |
| ·数据表示范围与精度 | 第86页 |
| ·多模块系统验证 | 第86-87页 |
| ·ArithSMV系统 | 第87-89页 |
| ·功能描述 | 第87页 |
| ·系统结构 | 第87-88页 |
| ·条件模型检验模块 | 第88-89页 |
| ·可满足性判定模块 | 第89页 |
| ·本章小结 | 第89-90页 |
| 第七章 浮点加法部件验证 | 第90-110页 |
| ·浮点加法部件介绍 | 第90-91页 |
| ·输入空间分割 | 第91-98页 |
| ·加法 | 第94-95页 |
| ·指数差大于1的减法 | 第95页 |
| ·指数差等于0的减法 | 第95-98页 |
| ·指数差等于1的减法 | 第98页 |
| ·舍入问题 | 第98-99页 |
| ·实验结果 | 第99-109页 |
| ·正确电路验证结果 | 第100-107页 |
| ·错误电路 | 第107-108页 |
| ·子规范覆盖率 | 第108-109页 |
| ·本章小节 | 第109-110页 |
| 第八章 结束语 | 第110-112页 |
| ·全文总结 | 第110-111页 |
| ·今后研究方向 | 第111-112页 |
| 参考文献 | 第112-124页 |
| 致谢 | 第124-125页 |
| 作者简历 | 第125页 |