ASIP體系結構描述、仿真和形式化驗證方法研究.pdf

1、ASIP(Application Specific Instruction-set Processor)是針對特定應用領域而設計的專用指令集處理器，它兼具ASIC(Application Specific Integrated Circuit)的高性能和GPP(General Purpose Processor)的靈活性，在嵌入式領域有著廣泛的應用前景。 但是目前還沒有十分成熟通用的ASIP設計開發(fā)工具，這使得ASIP的開發(fā)只能

2、由經(jīng)驗豐富的專家完成。ASIP設計方法學因此成為了目前的研究熱點，主要的研究方向有：體系結構描述、編譯器和仿真器自動生成、體系結構設計空間搜索、體系結構正確性驗證等。 本文針對ASIP設計方法學進行研究，主要工作和貢獻如下： (1)ADL(體系結構描述語言，Architecture Description Language)的設計本文在分析多種現(xiàn)有的ADL優(yōu)缺點的基礎上，結合本實驗室在ADL領域已有的研究經(jīng)驗，提出并規(guī)范

3、化定義了一種基于微體系結構模板的體系結構描述語言mtADL(micro-architecture template ADL)。mtADL為嵌入式領域最常見的2種體系微體系結構(簡單流水線和動態(tài)調度流水線)提供了模板。用戶選定并配置好微結構模板后，可以完全定制指令集。并且在定制指令集時，用戶可以把精力集中在指令的功能上，而不需要處理各種復雜的微體系結構特性。這樣既保留了ASIP的大部分靈活性，又極大地提高了開發(fā)速度。 (2)ASI

4、P仿真器自動生成仿真器是ASIP開發(fā)中的重要工具。本文介紹了根據(jù)mtADL的描述自動生成ASIP功能仿真器和周期精確仿真器的算法。 (3)形式化驗證本文使用基于模型檢驗(model checking)的方法形式化地驗證處理器流水線控制邏輯的正確性，特別是流水線是否支持精確中斷。我們使用有限狀態(tài)機(FSM，F(xiàn)inite State Machine)對流水線控制邏輯進行建模，使用時序邏輯(Temporal Logic)公式來描述包括