ASIP(Application Specific Instruction-set Processor)是针对特定应用领域而设计的专用指令集处理器，它兼具ASIC(Application Specific Integrated Circuit)的高性能和GPP(General Purpose Processor)的灵活性，在嵌入式领域有着广泛的应用前景。 但是目前还没有十分成熟通用的ASIP设计开发工具，这使得ASIP的开发只能由经验丰富的专家完成。ASIP设计方法学因此成为了目前的研究热点，主要的研究方向有：体系结构描述、编译器和仿真器自动生成、体系结构设计空间搜索、体系结构正确性验证等。 本文针对ASIP设计方法学进行研究，主要工作和贡献如下： (1)ADL(体系结构描述语言，Architecture Description Language)的设计本文在分析多种现有的ADL优缺点的基础上，结合本实验室在ADL领域已有的研究经验，提出并规范化定义了一种基于微体系结构模板的体系结构描述语言mtADL(micro-architecture template ADL)。mtADL为嵌入式领域最常见的2种体系微体系结构(简单流水线和动态调度流水线)提供了模板。用户选定并配置好微结构模板后，可以完全定制指令集。并且在定制指令集时，用户可以把精力集中在指令的功能上，而不需要处理各种复杂的微体系结构特性。这样既保留了ASIP的大部分灵活性，又极大地提高了开发速度。 (2)ASIP仿真器自动生成仿真器是ASIP开发中的重要工具。本文介绍了根据mtADL的描述自动生成ASIP功能仿真器和周期精确仿真器的算法。 (3)形式化验证本文使用基于模型检验(model checking)的方法形式化地验证处理器流水线控制逻辑的正确性，特别是流水线是否支持精确中断。我们使用有限状态机(FSM，Finite State Machine)对流水线控制逻辑进行建模，使用时序逻辑(Temporal Logic)公式来描述包括中断精确性在内的流水线正确性属性，然后使用模型检验工具NuSMV检验时序逻辑公式在流水线模型上是否为真。和传统的基于仿真的验证方法相比，我们的验证方法可以达到100％的覆盖率。 本文还通过一个基于mtADL简单流水线模板的MIPS处理器范例详细地说明了我们的验证过程。本文验证的流水线范例含有3个不同的执行单元、2级Cache和乱序完成等复杂的流水线特性。