微处理器的分级模型检验验证研究

论文摘要

验证(Verification)是当今集成电路计算机辅助设计(ICCAD)领域的一个重要且困难的问题。传统的基于二叉决策图(BDD)的模型检验(Model Checking)技术和工具在有限状态并发系统的形式化验证中已运用多年。然而,由于该方法要求在进行验证前首先将目标系统的BDD模型在空间展开,从而不能利用设计本身在功能或结构方面的模块性和连接性,因此在处理较大规模的系统(如微处理器)设计时,具有很大的局限性。本文的工作目标是对微处理器的分级模型检验技术的研究和实现。旨在利用硬件设计语言(HDL)在寄存器传输级(RTL)上的设计特性,采用自底向上的方法分级建模,从而自动构造出可供模型检验工具处理的微处理器模型。通过利用模块间信号不变量,添加层次间附加辅助约束的方法,减小验证空间,消除冗余的不可达状态,提高模型检验的效率。本文将研究成果和开源模型检验工具NuSMV进行了集成,并利用集成后的系统对多个DLX结构的CPU设计模型进行了验证。通过NuSMV语言构造待验证系统,利用分支时态逻辑(CTL)描述待验证的时态性质。实验结果证明了研究算法的有效性,相对于传统的模型检验,在验证时间和空间消耗方面都取得明显改善。

论文目录

• 第1章 引言
• 1.1 问题的提出
• 1.2 选题背景及意义
• 1.2.1 设计验证技术简介
• 1.2.2 模拟验证
• 1.2.3 形式验证
• 1.2.4 微处理器的设计验证
• 1.2.5 小结
• 1.3 文献综述
• 1.3.1 形式验证的研究现状
• 1.3.2 微处理器形式验证的发展
• 1.4 研究方法
• 1.5 论文结构安排
• 第2章 层次式模型检验建模
• 2.1 模型检验概述
• 2.1.1 时态逻辑
• 2.1.2 二叉判定图BDD
• 2.1.3 符号模型检验SMC
• 2.1.4 定界模型检验BMC
• 2.2 NuSMV 中的模型检验
• 2.3 模块化设计的验证建模
• 2.3.1 定义一
• 2.3.2 定义二
• 2.3.3 定义三
• 2.4 层次化验证算法框架
• 2.5 验证框架和NuSMV 集成
• 第3章 DLX 微处理器验证模型的提取
• 3.1 DLX 处理器体系结构
• 3.1.1 ISA 关键部件
• 3.1.2 DLX 指令集结构
• 3.1.3 指令流水阶段
• 3.2 DLX 层次验证模型提取
• 3.2.1 设计域和验证域的模块化
• 3.2.2 层次模型的提取方法
• 3.2.3 提取结果
• 3.3 DLX 的NuSMV 验证模型生成
• 第4章 验证性质的提取
• 4.1 功能性质的CTL 表述
• 4.2 验证性质分类
• 4.2.1 机器特殊指令性质
• 4.2.2 算术逻辑运算性质
• 4.2.3 流水线指令流性质
• 4.2.4 分支预测性质
• 4.2.5 流水线执行类型性质
• 4.2.6 内部总线性质
• 第5章 验证实验
• 5.1 实验环境
• 5.2 实验目的和方法
• 5.3 实验结果
• 第6章 结论
• 6.1 研究结论
• 6.2 未来方向
• 参考文献
• 致谢
• 声明
• 附录A RT 级流水线DLX CPU 设计B 的NuSMV 模型
• 个人简历、在学期间发表的学术论文与研究成果