【作者】 高妍妍；

【导师】 熊焰； 李曦；

【作者基本信息】 中国科学技术大学 ， 计算机系统结构， 2009， 博士

【摘要】 专用指令集处理器(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】 Application Specific Instructions Set Processors(ASIP) is a kind of special processor designed for a particular type of applications.With the continuous development of ASIP design,the complexity of the design is also increasing,and the verification efforts on the correctness of design are increasingly prominently accordingly.Due to the diversity of instructions’ behaviors and the flexibility of logical structures,it is very difficult to build a general method to verify the correctness of the ASIP design automaticly.So far,there is not any effective theory and methodology on the automatic verification of ASIP design at architecture level.On the problems mentioned above,the hierarchy characteristics of ASIP architecture design were analyzed deeply.A framework on the verification of ASIP architecture design,which is based on Petri Net and Model Checking theory and methodology,is presented in this thesis.The properties which an ASIP design needs to satisfy are divided into static properties and dynamic properties.Static properties are used to specify the requirements of structure and individual instructions’ execution,while dynamic properties are used to specify the requirements of concurrent instructions.The main research works include:(1) Description of the ASIP architecture based on Petri net.Hardware Design based-on Petri Net(HDPN),an extended Petri net,is used to describe the structural and behavioral characteristics of ASIP architecture.The static properties which an ASIP design should obey are also proposed.(2) Verification of the dynamic properties based on Model Checking.Firstly, the model of ASIP architecture to be validated is constructed,and the dynamic properties which a processor should obey are extracted from customer-built requirements.Then model checker is used to check the consistency of the model and of the properties.The method is applied to a pipeline processor and an out-of-order processor to prove the availability.(3) Modeling method based on the hierarchical and local characteristic of ASIP design.In order to efficiently verify the design,the models’ scale should be restricted.Two kinds of models,global design and local models are constructed in this method.The global design,in which many details are hidden to reduce the scale of the model,is used to check the validity of the interaction between the components. While local models,in which concrete designs of each individual component are described,are used to verify detailed specifications.In this situation,the other parts of the design are treated as outer environment,and the interface parameters of the model are set as stochastic values in the possible range.(4) The translation rules from HDPN based description to model checker based description.Based on the translation procedure,a verification framework which supports the validation on the correctness of structures and instructions’ execution of an ASIP architecture design is constructedThe main contributions of this thesis are as follows:(1) Aiming to the design of ASIP architecture,a novel extended Petri Net model named HDPN is introduced.It can describe target architecture in a succinct and precise way.In HDPN,tokens are endowed with concrete information according to the specific design,but not only a black dot in traditional Petri Net.Therefore the elements in the Places are added with types.And transitions,which are used to describe the function units,are appended with interface parameters,execution conditions and concrete action description.Arcs,which are used to describe data path,are also appended with parameters.To sum up,as a modeling tool,HDPN can sufficiently describe the structural information and individual instructions’ execution of the ASIP architecture.The method based on HDPN,taking advantage of it,can efficiently verify the static properties accordingly.(2) Model checking is applied to the verification of ASIP architecture. Modeling method based on hierarchical and local description is presented and used to abstract models from a pipeline processor and an out-of-order execution processor. These modeling methods are effective to avoid state space explosion.The dynamic properties used to check the correctness of a processor execution are also proposed.(3) The translation rules from HDPN description to the input language of model checker-NuSMV are presented.Therefore,an integrated framework for ASIP architecture verification is built.The properties for the verification are divided into static properties and dynamic properties.They are checked through the static property checking method based on HDPN and dynamic property checking method based on model checking,separately.更多还原