浅谈asip体系结构描述、仿真和形式化验证方法研究

《浅谈asip体系结构描述、仿真和形式化验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中国科学技术大学硕士学位论文ASIP体系结构描述、仿真和形式化验证方法研究姓名：仲力申请学位级别：硕士专业：计算机系统结构指导教师：李曦20070501摘要A$IP(ApplicationSpecificInstruction-setProcessor)是针对特定应用领域而设计的专用指令集处理器，它兼具ASIC(ApplicationSpecificIntcgratexlCircuit)的高性能和GPP(GeneralPUrpDSCProcessor)的灵活性，在嵌入式领域有着广泛的应用前景。但是目前还没有十分成熟通用的ASIP设计开发工具，这使得ASIP的开发

2、只能由经验丰富的专家完成。ASIP设计方法学因此成为了目前的研究热点，主要的研究方向有：体系结构描述、编译器和仿真器自动生成、体系结构设计空间搜索、体系结构正确往验证等。本文针对ASIP设计方法学进行研究，主要工作和贡献如下：(1)ADL(／f本系结构描述语言，ArchitectureDescriptionlanguage)的设计本文在分析多种现有的ADL优缺点的基础上。结合本实验室在ADL领域已有的研究经验，提出并规范化定义了～种基于微体系结构模板的体系结构描述语言mtADL(micro-architccturetemplateADL)，mtADL为嵌入式领域

3、最常见的2种体系微体系结构(简单流水线和动态调度流水线)提供了模板。用户选定并配置好微结构模板后，可以完全定制指令集。并且在定制指令集时，用户可以把精力集中在指令的功能上，丽不需要处理各种复杂的微体系结构特性。这样既保留了ASIP的大部分灵活性，又极大地提高了开发速度。(2)AS]P仿真器自动生成仿真器是ASIP开发中的重要工具。本文介绍了根据mtADL的描述自动生成ASIP功能仿真器和周期精确仿真器的算法。(3)形式化验证本文使。固基于模型；睑验(modclchecking)的方法形式化地验证处理器流水线控制逻辑的正确性，特别是流水线是否支持精确中断。我们使用

4、有限状态机(FSM，FiniteStateMachine)对流水线控制逻辑进行建模，使用时序逻辑O'emporalLogic)公式来描述包括中断精确性在内的流水线正确性属性，然后使用模型检验工具NuSMV检验时序逻辑公式在流水线模型上是否为真。和传统的基于仿真的验证方法相比，我们的验证方法可以达到100％的覆盖率。本文还通过一个基于mtADL简单流水线模板的MIPS处理器范例详细地说明了我们的验证过程。本文验证的流水线范例含有3个不同的执行单元，2级Cache和乱序完成等复杂的流水线特性．关键字：ASIP设计方法学ADL仿真器自动生成形式化验证精确中断Abstr

5、actASIP(ApplicationSpecificInstruction-setProcessor)isanemergingtechnologytodevelopapplications础embeddedsystems．ItcancompeteASIC丽thperformance．andi乜flexibilityiscomparablewithGPP(C-eneralPurposeProcessor)．Asanresult,ASIPhasbeenprovedtobeapromisingapproachinembeddedsystemdesigns．Butdu

6、etolackofintegratedandeasytou∞developingtools．thedevelopmentofASIPiscurrentlytheexclusivedomainofsemiconductorhousesandOOrevendors．Therefore．ASIPdesignmethodologyisbecoming孤activefieldofresearchworks．Themainresearchsub-fieldsarearchitecturedescription，automaticgenerationofsimulatoran

7、dcompiler,designspaceexploration∞SE)，verificationofASIP,etC．ThisthesisfocusesontheresearchofASIPdesignmethodology．Themainworkandcontributionare．"(1)DesignofADL(ArchitectureDescriptionLanguage)BasedonthestudyofexistingADLs，andtheADLresearchegpeTienceofourLaboratory,thisthesispresentsa

8、novelADL：mtA