| 第1章 引言 | 第1-24页 |
| ·问题的提出 | 第7-8页 |
| ·选题背景及意义 | 第8-16页 |
| ·设计验证技术简介 | 第9-10页 |
| ·模拟验证 | 第10-11页 |
| ·形式验证 | 第11-13页 |
| ·微处理器的设计验证 | 第13-15页 |
| ·小结 | 第15-16页 |
| ·文献综述 | 第16-21页 |
| ·形式验证的研究现状 | 第16-19页 |
| ·微处理器形式验证的发展 | 第19-21页 |
| ·研究方法 | 第21-22页 |
| ·论文结构安排 | 第22-24页 |
| 第2章 层次式模型检验建模 | 第24-35页 |
| ·模型检验概述 | 第24-30页 |
| ·时态逻辑 | 第25-28页 |
| ·二叉判定图BDD | 第28-29页 |
| ·符号模型检验SMC | 第29-30页 |
| ·定界模型检验BMC | 第30页 |
| ·NuSMV 中的模型检验 | 第30-31页 |
| ·模块化设计的验证建模 | 第31-33页 |
| ·定义一 | 第31-32页 |
| ·定义二 | 第32页 |
| ·定义三 | 第32-33页 |
| ·层次化验证算法框架 | 第33页 |
| ·验证框架和NuSMV 集成 | 第33-35页 |
| 第3章 DLX 微处理器验证模型的提取 | 第35-49页 |
| ·DLX 处理器体系结构 | 第35-38页 |
| ·ISA 关键部件 | 第36-37页 |
| ·DLX 指令集结构 | 第37-38页 |
| ·指令流水阶段 | 第38页 |
| ·DLX 层次验证模型提取 | 第38-43页 |
| ·设计域和验证域的模块化 | 第38页 |
| ·层次模型的提取方法 | 第38-39页 |
| ·提取结果 | 第39-43页 |
| ·DLX 的NuSMV 验证模型生成 | 第43-49页 |
| 第4章 验证性质的提取 | 第49-56页 |
| ·功能性质的CTL 表述 | 第49-53页 |
| ·验证性质分类 | 第53-56页 |
| ·机器特殊指令性质 | 第53页 |
| ·算术逻辑运算性质 | 第53-54页 |
| ·流水线指令流性质 | 第54页 |
| ·分支预测性质 | 第54页 |
| ·流水线执行类型性质 | 第54-55页 |
| ·内部总线性质 | 第55-56页 |
| 第5章 验证实验 | 第56-58页 |
| ·实验环境 | 第56页 |
| ·实验目的和方法 | 第56-57页 |
| ·实验结果 | 第57-58页 |
| 第6章 结论 | 第58-59页 |
| ·研究结论 | 第58页 |
| ·未来方向 | 第58-59页 |
| 参考文献 | 第59-63页 |
| 致谢 | 第63页 |
| 声明 | 第63-64页 |
| 附录A RT 级流水线DLX CPU 设计B 的NuSMV 模型 | 第64-78页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第78页 |