ASIP体系结构形式化建模与验证方法研究

论文摘要

专用指令集处理器（Application Specific Instructions Set Processor,ASIP）是专为某个或某类应用而设计的处理器。随着ASIP体系结构的不断发展,设计的复杂性不断增加,如何有效地验证体系结构设计的正确性问题在ASIP设计中日益突出。ASIP体系结构本身具有指令行为定义的多样性和逻辑结构设计的灵活性等特点,使得构造验证模型与精确地刻画系统特征非常困难,尚未形成一套能够有效地解决ASIP体系结构层设计自动验证问题的理论和方法。本文针对上述问题,在分析ASIP体系结构的层次化设计特征的基础上,提出了基于Petri网理论和模型检测方法的ASIP体系结构验证框架,对ASIP体系结构进行描述和验证。通过对已有的ASIP体系结构设计的分析,将ASIP体系结构需要满足的属性分为静态属性和动态属性两个方面,分别进行研究。静态属性是指系统中的结构特征和单条指令的执行情况的检测,动态属性关注的是指令并发执行设计的正确性,主要包括与数据相关、控制相关等方面相关的控制结构设计的正确性的检测。主要研究工作包括:（1）基于Petri网描述ASIP体系结构。首先根据ASIP体系结构设计的特点提出一个新的扩展的Petri网——HDPN（Hardware design based-on Petri Net）,用其描述ASIP体系结构,刻画处理器设计中的结构和行为特征。然后给出ASIP设计需要满足的静态属性,用以检测ASIP设计中的静态需求是否得到满足。（2）基于模型检测方法对动态属性进行验证。首先建立待验证的ASIP体系结构模型并提取该模型需要满足的动态属性,然后采用模型检测工具对模型和动态属性的一致性进行验证。本文给出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序处理器两种抽象处理器描述了具体的建模方法,分析了它们的动态属性,并对其进行了验证,证明了此方法的有效性。（3）结合ASIP设计的层次化特点,提出了层次化和局部化的建模方法。采用抽象模型描述设计的整体特性,采用细化模型来刻画局部设计的细节,从而控制模型的规模,规避模型检测方法中的状态空间爆炸问题。（4）提出了从HDPN描述到模型检测描述的转换规则。在此基础上,实现了一个支持结构检测和指令执行正确性检测的体系结构验证框架。本文做出的贡献主要体现在:（1）面向体系结构建模的需求,基于Petri网理论,提出了一种ASIP体系结构描述方法——HDPN。HDPN继承了Petri网的直观性特点,可以很好地刻画体系结构中模块间的互连关系;在此基础上加强了对设计中的存储单元、功能单元以及数据通路的刻画,通过对Petri网中的基本元素——库所、变迁和弧的扩展,分别对存储单元中存储的数据添加了类型定义,对功能部件添加了接口参数、执行条件和具体的行为描述,对数据通路定义了所传递的参数,提高了模型的描述能力。基于HDPN描述提出ASIP设计需要满足的静态属性,对设计的结构描述正确性和单条指令执行的正确性进行验证。（2）将模型检测方法应用于ASIP体系结构验证中。提出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序执行处理器描述了具体的建模方法,并给出了处理器正确执行所需满足的属性。在建模时采用分层和局部建模的方法有效规避模型检测方法中的状态空间爆炸问题,提高了模型检测方法的可用性。（3）建立了HDPN描述和模型检测描述之间的转换规则,形成一个完整的ASIP体系结构验证框架。将ASIP体系结构的验证问题合理地划分为静态属性（结构正确性和单条指令执行的正确性问题）和动态属性（指令并行执行的正确性问题）两个子问题,分别通过基于Petri网的静态属性检测方法和基于模型检测的动态属性的检测方法对其描述和验证。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 引言
• 1.2 ASIP应用背景
• 1.3 ASIP设计
• 1.4 ASIP验证的研究动机与目标
• 1.5 验证方法概述
• 1.5.1 基于仿真的验证方法
• 1.5.2 基于形式化方法的验证
• 1.5.3 验证方法小结
• 1.6 体系结构描述方法
• 1.6.1 体系结构描述语言
• 1.6.2 Petri网
• 1.6.3 小结
• 1.7 本文的主要工作
• 1.8 论文组织
• 第2章 ASIP体系结构描述
• 2.1 引言
• 2.2 已有工作
• 2.3 ASIP体系结构
• 2.4 HDPN
• 2.4.1 Petri网原理
• 2.4.2 HDPN
• 2.5 基于HDPN的ASIP设计
• 2.6 描述实例
• 2.7 小结
• 第3章 静态属性验证
• 3.1 引言
• 3.2 静态属性
• 3.2.1 结构有效性
• 3.2.2 接口一致性
• 3.2.3 行为确定性
• 3.2.4 活性
• 3.2.5 公平性
• 3.2.6 语义映射
• 3.2.7 时间约束
• 3.3 小结
• 第4章 动态属性验证
• 4.1 引言
• 4.2 已有工作
• 4.3 模型描述和属性描述方法
• 4.3.1 NuSMV
• 4.3.2 属性描述方法
• 4.4 模型提取方法
• 4.4.1 分层检测方法
• 4.4.2 局部模型检测方法
• 4.5 实例
• 4.6 小结
• 第5章 从HDPN到NuSMV描述的转换
• 5.1 引言
• 5.2 HDPN和NuSMV的比较
• 5.3 HDPN到NuSMV描述的转换
• 5.3.1 全局模型的转换
• 5.3.2 局部模型的转换
• 5.4 实例分析
• 5.5 小结
• 第6章 流水线处理器验证
• 6.1 引言
• 6.2 DLX流水线的验证
• 6.2.1 已有工作
• 6.2.2 流水线结构
• 6.2.3 流水线模型
• 6.2.4 流水线的基本属性
• 6.2.5 流水线验证
• 6.2.6 小结
• 6.3 带旁路的流水线验证
• 6.3.1 已有工作
• 6.3.2 旁路流水线
• 6.3.3 流水线模型
• 6.3.4 属性定义
• 6.3.5 实例分析
• 6.4 小结
• 第7章 乱序执行处理器验证
• 7.1 引言
• 7.2 已有工作
• 7.3 基于Tomasulo算法的处理器设计验证
• 7.3.1 Tomasulo算法
• 7.3.2 基于Tomulo算法处理器的模型提取
• 7.3.3 属性提取
• 7.4 支持猜测执行和Tomasulo算法的处理器设计验证
• 7.4.1 支持猜测执行和Tomasulo算法的处理器体系结构
• 7.4.2 模型提取
• 7.4.3 属性提取
• 7.4.4 处理器验证
• 7.5 存储器访问操作的建模和验证
• 7.6 小结
• 第8章 结束语
• 8.1 研究工作总结
• 8.2 进一步研究工作的展望
• 参考文献
• 在读期间发表的学术论文与取得的研究成果
• 致谢