| 第一章 绪论 | 第1-22页 |
| §1.1 引言 | 第11-12页 |
| §1.2 验证的基本概念 | 第12-13页 |
| §1.3 验证方法综述 | 第13-20页 |
| ·模拟验证方法 | 第13-14页 |
| ·软件模拟 | 第13-14页 |
| ·硬件仿真 | 第14页 |
| ·测试 | 第14页 |
| ·形式验证方法 | 第14-20页 |
| ·模型检验 | 第15-16页 |
| ·定理证明 | 第16-17页 |
| ·等价性检查 | 第17-20页 |
| §1.4 论文的研究重点以及章节安排 | 第20-22页 |
| 第二章 二叉决策图及其在电路验证中的应用 | 第22-34页 |
| §2.1 引言 | 第22页 |
| §2.2 二叉决策图 | 第22-23页 |
| §2.3 有序二叉决策图 | 第23-29页 |
| ·最简的的序二叉决策图 | 第24-25页 |
| ·ROBDD运算小结 | 第25-27页 |
| ·建立电路中节点逻辑函数的ROBDD表示 | 第27-28页 |
| ·ROBDD的变量问题 | 第28-29页 |
| §2.4 基于HARMONY多输出变量排序 | 第29-34页 |
| ·单输出变量排序 | 第31-32页 |
| ·Harmony启发式算法 | 第32-33页 |
| ·其它变量合并 | 第33页 |
| ·实验结果 | 第33-34页 |
| 第三章 可满足性方法与形式验证 | 第34-50页 |
| §3.1 引言 | 第34页 |
| §3.2 可满足性问题的有关定义和性质 | 第34-35页 |
| §3.3 SAT求解程序 | 第35-40页 |
| ·DPLL算法 | 第36-37页 |
| ·分支策略 | 第37-38页 |
| ·冲突分析 | 第38-40页 |
| §3.3 可满足性的电路验证原理 | 第40-42页 |
| §3.4 静态隐含加速等价性验证 | 第42-50页 |
| ·静态隐含术语介绍 | 第42-44页 |
| ·关联节点静态隐含 | 第44-47页 |
| ·识别关联节点 | 第45页 |
| ·关联节点静态隐含算法 | 第45-47页 |
| ·提高隐含速度的策略 | 第47-48页 |
| ·算法 | 第48页 |
| ·实验结果 | 第48-50页 |
| 第四章 组合电路等价性验证方法研究 | 第50-72页 |
| §4.1 引言 | 第50-51页 |
| §4.2 组合电路中一些基本定义 | 第51-54页 |
| §4.3 结合二叉判决图和布尔可满足性的等价性验证算法 | 第54-61页 |
| ·基本定义和定理 | 第55页 |
| ·验证算法 | 第55-60页 |
| ·AIG结构简化 | 第56-57页 |
| ·二叉判决图扩展 | 第57-58页 |
| ·基于电路的解算器和基于CNF的解算器 | 第58-60页 |
| ·实验结果 | 第60-61页 |
| §4.4 一种有效的基于割集的等价性验证算法 | 第61-72页 |
| ·基本定义和定理 | 第61-62页 |
| ·算法描述 | 第62-64页 |
| ·割集生成算法 | 第64-68页 |
| ·动态割集生成 | 第64-66页 |
| ·静态割集 | 第66-68页 |
| ·依赖性处理 | 第68页 |
| ·误判处理 | 第68-69页 |
| ·实验结果及其分析 | 第69-72页 |
| 第五章 时序电路等价性验证方法研究 | 第72-95页 |
| §5.1 引言 | 第72-73页 |
| §5.2 一种有效的用于时序电路等价性验证的锁存器匹配算法 | 第73-81页 |
| ·预备知识 | 第74-75页 |
| ·算法描述 | 第75-79页 |
| ·任意模拟技术 | 第76页 |
| ·局部BDD | 第76-78页 |
| ·目标模拟 | 第78-79页 |
| ·实验结果 | 第79-81页 |
| §5.3 基于局部BDD的时序电路等价性验证 | 第81-95页 |
| ·预备知识 | 第81-85页 |
| ·相关研究 | 第85-88页 |
| ·基于局部BDD的时序验证算法 | 第88-93页 |
| ·算法流程 | 第88-90页 |
| ·算法原理 | 第90页 |
| ·其它加速策略 | 第90-91页 |
| ·时序方法描述 | 第91-93页 |
| ·实验结果 | 第93-95页 |
| 第六章 结论与展望 | 第95-97页 |
| §6.1 论文的主要工作 | 第95-96页 |
| §6.2 进一步的研究工作和设想 | 第96-97页 |
| 参考文献 | 第97-103页 |
| 攻读博士期间撰写的学术论文 | 第103-104页 |
| 致谢 | 第104页 |