| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-8页 |
| 第一章 综述 | 第8-16页 |
| ·引言 | 第8页 |
| ·验证的基本概念 | 第8-9页 |
| ·验证方法综述 | 第9-16页 |
| ·模拟验证 | 第9-11页 |
| ·模拟验证的基本原理 | 第9-10页 |
| ·事件驱动模拟和基于周期的模拟 | 第10页 |
| ·硬件加速和硬件仿真 | 第10-11页 |
| ·模拟验证的特点 | 第11页 |
| ·形式验证 | 第11-16页 |
| ·形式验证的基本过程 | 第11-12页 |
| ·模型检验 | 第12-13页 |
| ·定理证明 | 第13-14页 |
| ·形式验证方法与模拟验证方法的比较 | 第14-16页 |
| 第二章 二元判决图及其在电路验证中的应用 | 第16-30页 |
| ·引言 | 第16页 |
| ·二元判决图 | 第16-23页 |
| ·二元判决图的基本概念 | 第16-18页 |
| ·简化有序二元判决图(ROBDD)的性质 | 第18-21页 |
| ·目前对BDD研究的新进展 | 第21-23页 |
| ·符号模型检验的BDD表示和操作 | 第23-30页 |
| ·用BDD表示基本的布尔操作 | 第23-24页 |
| ·用BDD表示的量词操作 | 第24-26页 |
| ·用BDD表示集合和状态转移关系 | 第26-30页 |
| 第三章 符号模型检验技术 | 第30-44页 |
| ·引言 | 第30页 |
| ·计算树逻辑(CTL—Computation Tree Logic) | 第30-33页 |
| ·Kripke结构上幂集运算的不动点特性 | 第33-35页 |
| ·符号模型检验技术 | 第35-41页 |
| ·用BDD表示被验证系统 | 第36-37页 |
| ·符号模型检验的基本算法 | 第37-41页 |
| ·公平性约束检验(Fairness Constraints) | 第41-44页 |
| 第四章 用符号模型检验技术验证时序逻辑电路 | 第44-54页 |
| ·引言 | 第44页 |
| ·同步时序逻辑电路的BDD表示 | 第44-46页 |
| ·异步时序逻辑电路的BDD表示 | 第46-54页 |
| 第五章 符号模型检验系统的设计和实现 | 第54-64页 |
| ·引言 | 第54-55页 |
| ·SCSMV输入语言的语法规则和编译器的设计 | 第55-59页 |
| ·词法规则 | 第56页 |
| ·语法规则 | 第56-59页 |
| ·SCSMV的数据结构和算法实现 | 第59-61页 |
| ·实验结果 | 第61-64页 |
| 第六章 结束语 | 第64-66页 |
| ·结论 | 第64页 |
| ·将来的工作 | 第64-66页 |
| 附录 | 第66-70页 |
| 参考文献 | 第70-74页 |
| 致谢 | 第74-76页 |
| 作者简历 | 第76页 |