ASIP體系結(jié)構(gòu)形式化建模與驗證方法研究.pdf

1、專用指令集處理器(Application Specific Instructions Set Processor，ASIP)是專為某個或某類應用而設計的處理器。隨著ASIP體系結(jié)構(gòu)的不斷發(fā)展，設計的復雜性不斷增加，如何有效地驗證體系結(jié)構(gòu)設計的正確性問題在ASIP設計中日益突出。ASIP體系結(jié)構(gòu)本身具有指令行為定義的多樣性和邏輯結(jié)構(gòu)設計的靈活性等特點，使得構(gòu)造驗證模型與精確地刻畫系統(tǒng)特征非常困難，尚未形成一套能夠有效地解決ASIP體系結(jié)構(gòu)

2、層設計自動驗證問題的理論和方法。 本文針對上述問題，在分析ASIP體系結(jié)構(gòu)的層次化設計特征的基礎上，提出了基于Petri網(wǎng)理論和模型檢測方法的ASIP體系結(jié)構(gòu)驗證框架，對ASIP體系結(jié)構(gòu)進行描述和驗證。通過對已有的ASIP體系結(jié)構(gòu)設計的分析，將ASIP體系結(jié)構(gòu)需要滿足的屬性分為靜態(tài)屬性和動態(tài)屬性兩個方面，分別進行研究。靜態(tài)屬性是指系統(tǒng)中的結(jié)構(gòu)特征和單條指令的執(zhí)行情況的檢測，動態(tài)屬性關(guān)注的是指令并發(fā)執(zhí)行設計的正確性，主要包括與數(shù)據(jù)

3、相關(guān)、控制相關(guān)等方面相關(guān)的控制結(jié)構(gòu)設計的正確性的檢測。主要研究工作包括： (1)基于Petri網(wǎng)描述ASIP體系結(jié)構(gòu)。首先根據(jù)ASIP體系結(jié)構(gòu)設計的特點提出一個新的擴展的Petri網(wǎng)--HDPN(Hardware design based-on Petri Net)，用其描述ASIP體系結(jié)構(gòu)，刻畫處理器設計中的結(jié)構(gòu)和行為特征。然后給出ASIP設計需要滿足的靜態(tài)屬性，用以檢測ASIP設計中的靜態(tài)需求是否得到滿足。 (2)基

4、于模型檢測方法對動態(tài)屬性進行驗證。首先建立待驗證的ASIP體系結(jié)構(gòu)模型并提取該模型需要滿足的動態(tài)屬性，然后采用模型檢測工具對模型和動態(tài)屬性的一致性進行驗證。本文給出了基于模型檢測方法建立ASIP體系結(jié)構(gòu)模型的方法，針對流水線處理器和亂序處理器兩種抽象處理器描述了具體的建模方法，分析了它們的動態(tài)屬性，并對其進行了驗證，證明了此方法的有效性。 (3)結(jié)合ASIP設計的層次化特點，提出了層次化和局部化的建模方法。采用抽象模型描述設計的

5、整體特性，采用細化模型來刻畫局部設計的細節(jié)，從而控制模型的規(guī)模，規(guī)避模型檢測方法中的狀態(tài)空間爆炸問題。 (4)提出了從HDPN描述到模型檢測描述的轉(zhuǎn)換規(guī)則。在此基礎上，實現(xiàn)了一個支持結(jié)構(gòu)檢測和指令執(zhí)行正確性檢測的體系結(jié)構(gòu)驗證框架。 本文做出的貢獻主要體現(xiàn)在： (1)面向體系結(jié)構(gòu)建模的需求，基于Petri網(wǎng)理論，提出了一種ASIP體系結(jié)構(gòu)描述方法--HDPN。HDPN繼承了Petri網(wǎng)的直觀性特點，可以很好地刻畫體

6、系結(jié)構(gòu)中模塊間的互連關(guān)系；在此基礎上加強了對設計中的存儲單元、功能單元以及數(shù)據(jù)通路的刻畫，通過對Petri網(wǎng)中的基本元素--庫所、變遷和弧的擴展，分別對存儲單元中存儲的數(shù)據(jù)添加了類型定義，對功能部件添加了接口參數(shù)、執(zhí)行條件和具體的行為描述，對數(shù)據(jù)通路定義了所傳遞的參數(shù)，提高了模型的描述能力?；贖DPN描述提出ASIP設計需要滿足的靜態(tài)屬性，對設計的結(jié)構(gòu)描述正確性和單條指令執(zhí)行的正確性進行驗證。 (2)將模型檢測方法應用于ASI

7、P體系結(jié)構(gòu)驗證中。提出了基于模型檢測方法建立ASIP體系結(jié)構(gòu)模型的方法，針對流水線處理器和亂序執(zhí)行處理器描述了具體的建模方法，并給出了處理器正確執(zhí)行所需滿足的屬性。在建模時采用分層和局部建模的方法有效規(guī)避模型檢測方法中的狀態(tài)空間爆炸問題，提高了模型檢測方法的可用性。 (3)建立了HDPN描述和模型檢測描述之間的轉(zhuǎn)換規(guī)則，形成一個完整的ASIP體系結(jié)構(gòu)驗證框架。將ASIP體系結(jié)構(gòu)的驗證問題合理地劃分為靜態(tài)屬性(結(jié)構(gòu)正確性和單條指令