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

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

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

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

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

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

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

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