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

发布时间：2020-06-18 15:52

【摘要】： 专用指令集处理器(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网的静态属性检测方法和基于模型检测的动态属性的检测方法对其描述和验证。
【学位授予单位】：中国科学技术大学
【学位级别】：博士
【学位授予年份】：2009
【分类号】：TP332
【图文】：

框架图,框架,设计过程,形式化验证

图1.5AS工P设计的验证框架1.8论文组织本论文的主要目的是针对AS护设计流程中的验证需求，提出一套对系统设计，尤其是体系结构层次进行验证的方法。该方法提出一个完整的验证框架，以扩展的Petri网—HDPN为基础，通过模型提取、静态属性检测和动态属性检测方法，对设计的正确性进行检测。本文提出的验证方法具有通用性，可以用于ASIP设计过程的不同抽象层次的检测。如采用自上而下的设计方法，则可以将该方法与设计过程相结合，对设计中的每个层次的正确性进行检测，从而避免将设计错误带入后续的设计过程，减少大规模修改设计的可能，有效地缩短设计周期和面世时间。第一章概括介绍了ASIP设计的背景和研究动机。介绍了当前该领域形式化验证和体系结构描述的主要背景，以及我们研究的意义。引出文中使用的验

基本结构,保留站,写回,操作数

写回状态的指令对应的保留站编号记录的，则将操作数更新为写回指令的计算结果。Tomasul。算法的基本思想是只要操作数有效，就将其取到保留站，避免指令直接从寄存器中取数据(张晨曦，王志英 etal.2000)。图7.1给出了基于Tomasulo算法的MIPS处理器的基本结构 (Hennessyandpatterson2007)。「「「「~一一一一 }...「一 }}} }}}}}}}}}}}}}!{{{{{{{一一一一一一一一一operat，。·” US}}}}}}} }}}}}}}}}}}…… … … … … lllllllllllllll}}}}}}}}}}母母母母 lllllllllllllllllll .......}}}图7.1基于Tomasulo算法的M工PS浮点部件的基本结构由于保留站的数目多于实际的寄存器，使用保留站对寄存器重命名可以消除写后写和先读后写相关。因此，基于Tomasulo算法的处理器可以实现指令的

【共引文献】