| 摘要 | 第1-6页 |
| ABSTRACT | 第6-10页 |
| 第一章 绪论 | 第10-15页 |
| ·课题背景 | 第10-11页 |
| ·课题研究意义 | 第11-12页 |
| ·国内外研究现状 | 第12-13页 |
| ·章节安排 | 第13-15页 |
| 第二章 符号轨迹赋值与广义符号轨迹赋值 | 第15-35页 |
| ·符号轨迹赋值算法（STE） | 第15-17页 |
| ·建模阶段 | 第15-16页 |
| ·性质描述 | 第16页 |
| ·算法运行过程及验证结果 | 第16-17页 |
| ·符号轨迹赋值算法验证中的数据结构 | 第17-22页 |
| ·Binary Decision Diagram（BDD） | 第18-21页 |
| ·二叉判定图表达能力的扩展（MDD） | 第21页 |
| ·符号轨迹赋值的优缺点 | 第21-22页 |
| ·广义符号轨迹赋值（GSTE） | 第22-33页 |
| ·产生 GSTE 的时代背景 | 第22-27页 |
| ·GSTE 的前向和后向 | 第27-30页 |
| ·符号化变量的优势 | 第30-33页 |
| ·GSTE 与其他算法之间的对比 | 第33-34页 |
| ·GSTE 与 STE 的对比 | 第33-34页 |
| ·GSTE 与传统模型检验方法的对比 | 第34页 |
| ·本章小结 | 第34-35页 |
| 第三章 VIS 验证平台的分析和研究 | 第35-49页 |
| ·平台的前端处理 | 第35-40页 |
| ·电路前端抽取 | 第35-38页 |
| ·对抽取的数据进行分析生成 BLIF-MV 迁移关系 | 第38-40页 |
| ·VIS 基本数据结构（GLU 包） | 第40-41页 |
| ·VIS 的主程序框架设计 | 第41-44页 |
| ·VIS 中的主流程 | 第41-42页 |
| ·VIS 中内部细节分析 | 第42-44页 |
| ·通过具体例子介绍 VIS 平台 | 第44-47页 |
| ·VIS 平台的验证 | 第44-46页 |
| ·VIS 平台的仿真 | 第46-47页 |
| ·本章小结 | 第47-49页 |
| 第四章 GSTE 算法的实现 | 第49-67页 |
| ·设计思路来源 | 第49-50页 |
| ·系统设计 | 第50-59页 |
| ·系统结构 | 第50-51页 |
| ·前台设计 | 第51-54页 |
| ·后台设计 | 第54-59页 |
| ·系统中脚本文件 | 第59-61页 |
| ·系统测试 | 第61-65页 |
| ·本章小结 | 第65-67页 |
| 第五章 GSTE 反例查找算法 | 第67-73页 |
| ·反例查找算法介绍 | 第67-69页 |
| ·主要理论依据 | 第67-68页 |
| ·算法代码实现 | 第68-69页 |
| ·反例查找算法的正确性分析与验证 | 第69-71页 |
| ·算法正确性分析 | 第69-70页 |
| ·算法正确性验证 | 第70-71页 |
| ·本章小结 | 第71-73页 |
| 第六章 总结和展望 | 第73-76页 |
| ·本文总结 | 第73-74页 |
| ·主要完成的工作 | 第73-74页 |
| ·存在的不足 | 第74页 |
| ·下一步工作的展望和设想 | 第74-76页 |
| 致谢 | 第76-77页 |
| 参考文献 | 第77-81页 |
| 硕士期间取得的成果 | 第81-82页 |