【摘要】： 專用指令集處理器(Application Specific Instructions Set Processor,ASIP)是專為某個或某類應(yīng)用而設(shè)計的處理器。隨著ASIP體系結(jié)構(gòu)的不斷發(fā)展,設(shè)計的復(fù)雜性不斷增加,如何有效地驗證體系結(jié)構(gòu)設(shè)計的正確性問題在ASIP設(shè)計中日益突出。ASIP體系結(jié)構(gòu)本身具有指令行為定義的多樣性和邏輯結(jié)構(gòu)設(shè)計的靈活性等特點,使得構(gòu)造驗證模型與精確地刻畫系統(tǒng)特征非常困難,尚未形成一套能夠有效地解決ASIP體系結(jié)構(gòu)層設(shè)計自動驗證問題的理論和方法。 本文針對上述問題,在分析ASIP體系結(jié)構(gòu)的層次化設(shè)計特征的基礎(chǔ)上,提出了基于Petri網(wǎng)理論和模型檢測方法的ASIP體系結(jié)構(gòu)驗證框架,對ASIP體系結(jié)構(gòu)進(jìn)行描述和驗證。通過對已有的ASIP體系結(jié)構(gòu)設(shè)計的分析,將ASIP體系結(jié)構(gòu)需要滿足的屬性分為靜態(tài)屬性和動態(tài)屬性兩個方面,分別進(jìn)行研究。靜態(tài)屬性是指系統(tǒng)中的結(jié)構(gòu)特征和單條指令的執(zhí)行情況的檢測,動態(tài)屬性關(guān)注的是指令并發(fā)執(zhí)行設(shè)計的正確性,主要包括與數(shù)據(jù)相關(guān)、控制相關(guān)等方面相關(guān)的控制結(jié)構(gòu)設(shè)計的正確性的檢測。主要研究工作包括: (1)基于Petri網(wǎng)描述ASIP體系結(jié)構(gòu)。首先根據(jù)ASIP體系結(jié)構(gòu)設(shè)計的特點提出一個新的擴(kuò)展的Petri網(wǎng)——HDPN(Hardware design based-on Petri Net),用其描述ASIP體系結(jié)構(gòu),刻畫處理器設(shè)計中的結(jié)構(gòu)和行為特征。然后給出ASIP設(shè)計需要滿足的靜態(tài)屬性,用以檢測ASIP設(shè)計中的靜態(tài)需求是否得到滿足。 (2)基于模型檢測方法對動態(tài)屬性進(jìn)行驗證。首先建立待驗證的ASIP體系結(jié)構(gòu)模型并提取該模型需要滿足的動態(tài)屬性,然后采用模型檢測工具對模型和動態(tài)屬性的一致性進(jìn)行驗證。本文給出了基于模型檢測方法建立ASIP體系結(jié)構(gòu)模型的方法,針對流水線處理器和亂序處理器兩種抽象處理器描述了具體的建模方法,分析了它們的動態(tài)屬性,并對其進(jìn)行了驗證,證明了此方法的有效性。 (3)結(jié)合ASIP設(shè)計的層次化特點,提出了層次化和局部化的建模方法。采用抽象模型描述設(shè)計的整體特性,采用細(xì)化模型來刻畫局部設(shè)計的細(xì)節(jié),從而控制模型的規(guī)模,規(guī)避模型檢測方法中的狀態(tài)空間爆炸問題。 (4)提出了從HDPN描述到模型檢測描述的轉(zhuǎn)換規(guī)則。在此基礎(chǔ)上,實現(xiàn)了一個支持結(jié)構(gòu)檢測和指令執(zhí)行正確性檢測的體系結(jié)構(gòu)驗證框架。 本文做出的貢獻(xiàn)主要體現(xiàn)在: (1)面向體系結(jié)構(gòu)建模的需求,基于Petri網(wǎng)理論,提出了一種ASIP體系結(jié)構(gòu)描述方法——HDPN。HDPN繼承了Petri網(wǎng)的直觀性特點,可以很好地刻畫體系結(jié)構(gòu)中模塊間的互連關(guān)系;在此基礎(chǔ)上加強(qiáng)了對設(shè)計中的存儲單元、功能單元以及數(shù)據(jù)通路的刻畫,通過對Petri網(wǎng)中的基本元素——庫所、變遷和弧的擴(kuò)展,分別對存儲單元中存儲的數(shù)據(jù)添加了類型定義,對功能部件添加了接口參數(shù)、執(zhí)行條件和具體的行為描述,對數(shù)據(jù)通路定義了所傳遞的參數(shù),提高了模型的描述能力�；贖DPN描述提出ASIP設(shè)計需要滿足的靜態(tài)屬性,對設(shè)計的結(jié)構(gòu)描述正確性和單條指令執(zhí)行的正確性進(jìn)行驗證。 (2)將模型檢測方法應(yīng)用于ASIP體系結(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)正確性和單條指令執(zhí)行的正確性問題)和動態(tài)屬性(指令并行執(zhí)行的正確性問題)兩個子問題,分別通過基于Petri網(wǎng)的靜態(tài)屬性檢測方法和基于模型檢測的動態(tài)屬性的檢測方法對其描述和驗證。
【學(xué)位授予單位】：中國科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2009
【分類號】：TP332
【圖文】：

圖1.5AS工P設(shè)計的驗證框架1.8論文組織本論文的主要目的是針對AS護(hù)設(shè)計流程中的驗證需求，提出一套對系統(tǒng)設(shè)計，尤其是體系結(jié)構(gòu)層次進(jìn)行驗證的方法。該方法提出一個完整的驗證框架，以擴(kuò)展的Petri網(wǎng)—HDPN為基礎(chǔ)，通過模型提取、靜態(tài)屬性檢測和動態(tài)屬性檢測方法，對設(shè)計的正確性進(jìn)行檢測。本文提出的驗證方法具有通用性，可以用于ASIP設(shè)計過程的不同抽象層次的檢測。如采用自上而下的設(shè)計方法，則可以將該方法與設(shè)計過程相結(jié)合，對設(shè)計中的每個層次的正確性進(jìn)行檢測，從而避免將設(shè)計錯誤帶入后續(xù)的設(shè)計過程，減少大規(guī)模修改設(shè)計的可能，有效地縮短設(shè)計周期和面世時間。第一章概括介紹了ASIP設(shè)計的背景和研究動機(jī)。介紹了當(dāng)前該領(lǐng)域形式化驗證和體系結(jié)構(gòu)描述的主要背景，以及我們研究的意義。引出文中使用的驗

寫回狀態(tài)的指令對應(yīng)的保留站編號記錄的，則將操作數(shù)更新為寫回指令的計算結(jié)果。Tomasul。算法的基本思想是只要操作數(shù)有效，就將其取到保留站，避免指令直接從寄存器中取數(shù)據(jù)(張晨曦，王志英 etal.2000)。圖7.1給出了基于Tomasulo算法的MIPS處理器的基本結(jié)構(gòu) (Hennessyandpatterson2007)�！� 「 「「~一一一 一 }...「一 }}} }}}}}}}}}}}}}!{{{{{{{一 一一一一一一一 一operat，。·” US}}}}}}} }}}}}}}}}}}…… … … … … lllllllllllllll}}}}}}}}}}母 母 母母 lllllllllllllllllll .......}}}圖7.1基于Tomasulo算法的M工PS浮點部件的基本結(jié)構(gòu)由于保留站的數(shù)目多于實際的寄存器，使用保留站對寄存器重命名可以消除寫后寫和先讀后寫相關(guān)。因此，基于Tomasulo算法的處理器可以實現(xiàn)指令的

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 邵志芳;錢省三;劉仲英;;基于Petrinet的半導(dǎo)體代工系統(tǒng)建模及案例研究[J];半導(dǎo)體技術(shù);2006年11期

2 王海峰,陳建明,張仲義;安全苛求系統(tǒng)的形式化開發(fā)方法[J];北方交通大學(xué)學(xué)報;2002年06期

3 汪亞男,王明哲;賦時著色Petri網(wǎng)在建模仿真中的應(yīng)用[J];兵工自動化;2005年01期

4 陳玉波;李世英;張彥忠;陳樂;;作戰(zhàn)單元裝備系統(tǒng)的需求量仿真模型[J];兵工自動化;2006年06期

5 王芳,侯朝楨;用蒙特卡羅和Petri網(wǎng)方法估計隨機(jī)流網(wǎng)絡(luò)的可靠性[J];北京理工大學(xué)學(xué)報;2004年07期

6 黃照強(qiáng),馮學(xué)智;基于PETRI網(wǎng)的土地變更時空過程建模[J];測繪學(xué)報;2005年03期

7 譚丹;樂曉波;;基于Petri網(wǎng)的樂音體系建模[J];長沙電力學(xué)院學(xué)報(自然科學(xué)版);2006年01期

8 湯志偉,殷靜;行政組織的流程重組建模技術(shù)分析[J];電子科技大學(xué)學(xué)報(社科版);2004年02期

9 徐敏,蘇建元;OOPN和PNOO建模技術(shù)研究[J];電腦與信息技術(shù);2005年05期

10 高秋紅;駱麗;;面向SOC設(shè)計的混合驗證方法及其應(yīng)用[J];電腦知識與技術(shù);2006年17期

相關(guān)會議論文 前2條

1 張繼軍;董衛(wèi);;基于Petri網(wǎng)的構(gòu)件組裝運算及其性質(zhì)[A];2006年全國開放式分布與并行計算機(jī)學(xué)術(shù)會議論文集（三）[C];2006年

2 童朝南;李寶峰;;電梯群控系統(tǒng)的Petri網(wǎng)建模與分析[A];冶金企業(yè)自動化、信息化與創(chuàng)新——全國冶金自動化信息網(wǎng)建網(wǎng)30周年論文集[C];2007年

相關(guān)博士學(xué)位論文 前10條

1 羅鵬程;基于Petri網(wǎng)的系統(tǒng)安全性建模與分析技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2001年

2 董威;面向UML的模型檢驗研究[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2002年

3 宋輝;量子計算機(jī)體系結(jié)構(gòu)及模擬技術(shù)的研究與實現(xiàn)[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2003年

4 劉海峰;安全操作系統(tǒng)若干關(guān)鍵技術(shù)的研究[D];中國科學(xué)院研究生院（軟件研究所）;2002年

5 楊宏志;人車路與環(huán)境系統(tǒng)仿真構(gòu)架及實施策略研究[D];長安大學(xué);2003年

6 張云勇;開放系統(tǒng)中移動性研究——基于agent的計算基本架構(gòu)（ABCBA）[D];電子科技大學(xué);2003年

7 董利達(dá);基于序狀Petri網(wǎng)的離散事件系統(tǒng)監(jiān)控理論[D];浙江大學(xué);2004年

8 竇連旺;網(wǎng)絡(luò)控制系統(tǒng)的建模、穩(wěn)定性分析及其調(diào)度的研究[D];天津大學(xué);2004年

9 梁彬;可信進(jìn)程機(jī)制及相關(guān)問題研究[D];中國科學(xué)院研究生院（軟件研究所）;2004年

10 張紹華;網(wǎng)格工作流關(guān)鍵技術(shù)研究[D];復(fù)旦大學(xué);2004年

相關(guān)碩士學(xué)位論文 前10條

1 張東紅;離散事件系統(tǒng)的Petri網(wǎng)控制方法研究[D];西安電子科技大學(xué);2000年

2 王卡停;柔性制造系統(tǒng)的Petri網(wǎng)物流仿真[D];浙江大學(xué);2001年

3 習(xí)勇;基于MPC850的嵌入式系統(tǒng)設(shè)計與應(yīng)用[D];國防科學(xué)技術(shù)大學(xué);2002年

4 王蓉暉;指令級并行性開發(fā)關(guān)鍵技術(shù)的研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2002年

5 蔣勇;工業(yè)以太網(wǎng)遠(yuǎn)程橋接系統(tǒng)的研究[D];重慶大學(xué);2002年

6 劉恒江;集裝箱空箱調(diào)運PETRI網(wǎng)模型仿真分析[D];上海海運學(xué)院;2002年

7 鄒顯春;基于活動圖模型的工作流形式化語義研究[D];西南師范大學(xué);2003年

8 池靜;Bloom Filter和Weighted Bloom Filte的比較和研究[D];太原理工大學(xué);2003年

9 高軍;EPIC體系結(jié)構(gòu)研究與流水線設(shè)計及實現(xiàn)[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2002年

10 李垣陵;基于68K處理器的嵌入式系統(tǒng)設(shè)計與應(yīng)用[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2002年

本文編號：2719488