【摘要】：當(dāng)今片上系統(tǒng)(System-on-chip,SoC)設(shè)計(jì)復(fù)雜度越來(lái)越高,很多復(fù)雜設(shè)計(jì)已經(jīng)無(wú)法從寄存器傳輸級(jí)(Register Transfer Level,RTL)開(kāi)始建模,對(duì)高層次行為和體系結(jié)構(gòu)模型的需求越來(lái)越迫切,系統(tǒng)級(jí)功能驗(yàn)證已經(jīng)成為影響SoC設(shè)計(jì)效率和質(zhì)量的最重要環(huán)節(jié)。針對(duì)SoC系統(tǒng)級(jí)功能驗(yàn)證各層巨大差異帶來(lái)的重復(fù)工作多、驗(yàn)證效率低下等突出問(wèn)題,本文研究SoC高層等價(jià)性檢驗(yàn)技術(shù),在理論和實(shí)踐上解決目前高層等價(jià)性檢驗(yàn)存在的問(wèn)題。SoC高層等價(jià)性檢驗(yàn)技術(shù)主要采用模擬方法,斷言方法和形式化方法。模擬方法主要是通過(guò)比較在相同的測(cè)試激勵(lì)下,不同層次設(shè)計(jì)輸出結(jié)果是否相同。斷言的方法主要是通過(guò)驗(yàn)證不同層次設(shè)計(jì)是否滿(mǎn)足相同的功能斷言。形式化方法主要利用形式化技術(shù)(模型檢驗(yàn),謂詞抽象和符號(hào)模擬)驗(yàn)證不同層次設(shè)計(jì)是否完全等價(jià)。三類(lèi)方法目前都面臨一些困難。模擬方法通過(guò)模擬大量的測(cè)試矢量進(jìn)行驗(yàn)證,開(kāi)銷(xiāo)較大并且無(wú)法保證測(cè)試的完備性。斷言方法的驗(yàn)證質(zhì)量完全取決于定義斷言的質(zhì)量。形式化方法存在需要設(shè)計(jì)之間的映射關(guān)系和狀態(tài)空間爆炸等問(wèn)題。本文首先綜述了SoC高層等價(jià)性檢驗(yàn)技術(shù)及相關(guān)技術(shù)迄今為止的研究進(jìn)展,對(duì)現(xiàn)有SoC高層等價(jià)性檢驗(yàn)方法進(jìn)行了分類(lèi),介紹了每種方法的研究現(xiàn)狀,分析了各種方法的優(yōu)缺點(diǎn)。最后分析了目前SoC高層等價(jià)性檢驗(yàn)還存在的問(wèn)題。本文的研究工作圍繞SoC高層等價(jià)性檢驗(yàn)的關(guān)鍵技術(shù)展開(kāi),針對(duì)目前SoC高層等價(jià)性檢驗(yàn)中存在的問(wèn)題,提出了新的算法并取得了如下創(chuàng)新成果:首先,針對(duì)模擬方法驗(yàn)證效率較低,驗(yàn)證開(kāi)銷(xiāo)大,無(wú)法保證設(shè)計(jì)完備性等問(wèn)題,本文提出了一種基于覆蓋率指導(dǎo)的模擬等價(jià)性檢驗(yàn)算法。首先分析了系統(tǒng)級(jí)與事務(wù)級(jí)(Transaction Level Modeling,TLM)的相似性(算法描述,模塊劃分,數(shù)據(jù)類(lèi)型)以及覆蓋率在不同層次間的關(guān)系,根據(jù)分析結(jié)果,引入代碼覆蓋率和功能覆蓋率作為高層測(cè)試矢量的質(zhì)量測(cè)度。利用復(fù)合覆蓋率(代碼覆蓋率和功能覆蓋率)在系統(tǒng)級(jí)產(chǎn)生高質(zhì)量測(cè)試矢量,并利用該測(cè)試矢量模擬系統(tǒng)級(jí)與TLM模型,比較觀察變量的值是否相等。實(shí)驗(yàn)結(jié)果表明,該方法能重用高層的驗(yàn)證努力,高效地驗(yàn)證系統(tǒng)級(jí)與TLM模型的等價(jià)性,同時(shí)還能有效地提高模擬方法的驗(yàn)證完備性。其次,針對(duì)形式化方法需要設(shè)計(jì)映射信息和驗(yàn)證效率較低等問(wèn)題,提出了一種基于深度路徑的等價(jià)性檢驗(yàn)算法。該方法提取系統(tǒng)級(jí)模型的帶數(shù)據(jù)通路的有限狀態(tài)機(jī)(Finite State Machines with Data Paths,FSMD),隨后提取FSMD中所有深度路徑。利用測(cè)試矢量生成技術(shù),產(chǎn)生所有深度路徑的測(cè)試矢量。將輸出狀態(tài)語(yǔ)句插入RTL模型中,利用產(chǎn)生的測(cè)試矢量模擬RTL模型,輸出對(duì)應(yīng)的深度路徑。最后,利用符號(hào)模擬和約束求解器驗(yàn)證對(duì)應(yīng)路徑的等價(jià)性。該方法能夠驗(yàn)證無(wú)映射信息的設(shè)計(jì)之間的等價(jià)性,同時(shí),只需驗(yàn)證對(duì)應(yīng)的深度路徑,避免了盲目的深度路徑比較。實(shí)驗(yàn)結(jié)果表明,該方法相比于目前的基于深度路徑的方法,減少了深度路徑驗(yàn)證次數(shù),提高了等價(jià)性檢驗(yàn)效率。再次,針對(duì)形式化方法需要設(shè)計(jì)映射信息和驗(yàn)證效率較低等問(wèn)題,提出了一種基于機(jī)器學(xué)習(xí)的等價(jià)性檢驗(yàn)算法。該方法無(wú)需提取模型的FSMD,減小了驗(yàn)證開(kāi)銷(xiāo)。將狀態(tài)輸出語(yǔ)句插入系統(tǒng)級(jí)與RTL代碼中,利用硬件設(shè)計(jì)開(kāi)發(fā)過(guò)程中產(chǎn)生的大量測(cè)試數(shù)據(jù),模擬系統(tǒng)級(jí)與RTL模型,得到FSMD狀態(tài)序列。利用機(jī)器學(xué)習(xí)技術(shù)劃分狀態(tài)序列,得到分類(lèi)狀態(tài)集合。根據(jù)狀態(tài)的類(lèi)別,構(gòu)造系統(tǒng)級(jí)與RTL對(duì)應(yīng)的路徑。最后利用符號(hào)模擬和約束求解器驗(yàn)證對(duì)應(yīng)路徑的等價(jià)性。該方法能夠有效解決差異巨大設(shè)計(jì)之間的等價(jià)性并能驗(yàn)證無(wú)對(duì)應(yīng)信息設(shè)計(jì)的等價(jià)性。利用機(jī)器學(xué)習(xí)技術(shù)識(shí)別對(duì)應(yīng)的路徑,減少盲目的路徑比較。實(shí)驗(yàn)結(jié)果表明,該方法能夠高效的驗(yàn)證無(wú)映射信息的系統(tǒng)級(jí)與RTL設(shè)計(jì)等價(jià)性。最后,針對(duì)高級(jí)綜合調(diào)度前后驗(yàn)證效率不高,循環(huán)結(jié)構(gòu)需要多次迭代等問(wèn)題,提出了一種基于共享值圖(Shared-Value Graph,SVG)的等價(jià)性檢驗(yàn)算法。該方法利用割點(diǎn)技術(shù),產(chǎn)生高級(jí)綜合調(diào)度前后設(shè)計(jì)的潛在互模擬位置,利用SVG驗(yàn)證互模擬位置之間公共變量的等價(jià)性。割點(diǎn)技術(shù)能夠劃分大規(guī)模設(shè)計(jì),驗(yàn)證大規(guī)模設(shè)計(jì)的等價(jià)性。通過(guò)定義互模擬關(guān)系減少自動(dòng)定理證明器求解的次數(shù),提高驗(yàn)證效率。同時(shí),SVG能夠一次性的驗(yàn)證循環(huán)結(jié)構(gòu),避免了進(jìn)行固定點(diǎn)迭代過(guò)程中大量的計(jì)算。實(shí)驗(yàn)結(jié)果表明,該方法能夠高效的驗(yàn)證高級(jí)綜合調(diào)度前后設(shè)計(jì)的等價(jià)性。
【學(xué)位授予單位】：國(guó)防科學(xué)技術(shù)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：TN47

【相似文獻(xiàn)】

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

1 古天龍;;歐洲高等院校計(jì)算機(jī)學(xué)科形式化方法教育探析[J];中國(guó)大學(xué)教學(xué);2007年11期

2 古天龍;董榮勝;;歐洲高校計(jì)算機(jī)專(zhuān)業(yè)的形式化方法課程教學(xué)[J];計(jì)算機(jī)教育;2008年10期

3 柴振榮;《編程中的形式化方法及其應(yīng)用》會(huì)議[J];管理科學(xué)文摘;1995年06期

4 鄭士貴;智能服務(wù)網(wǎng)絡(luò)形式化方法的模擬和實(shí)質(zhì)[J];管理科學(xué)文摘;1997年01期

5 姜利;孫永強(qiáng);;形式化方法的發(fā)展及展望[J];計(jì)算機(jī)科學(xué);1998年02期

6 張廣泉;關(guān)于軟件形式化方法[J];重慶師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2002年02期

7 鹿蕾;;形式化方法B的證明技術(shù)[J];現(xiàn)代電子技術(shù);2005年23期

8 陳澎;設(shè)計(jì)模式形式化方法分析和初步比較[J];計(jì)算機(jī)工程;2005年02期

9 李建華;李紅革;;形式化及其歷史發(fā)展[J];自然辯證法研究;2008年08期

10 曹源;唐濤;徐田華;穆建成;;形式化方法在列車(chē)運(yùn)行控制系統(tǒng)中的應(yīng)用[J];交通運(yùn)輸工程學(xué)報(bào);2010年01期

相關(guān)會(huì)議論文 前7條

1 李文健;;形式化的涵義及其認(rèn)識(shí)論本質(zhì)[A];1993年邏輯研究專(zhuān)輯[C];1993年

2 吳允曾;;關(guān)于形式化的幾個(gè)問(wèn)題[A];金岳霖學(xué)術(shù)思想研究——金岳霖學(xué)術(shù)思想研討會(huì)論文集[C];1985年

3 鄭宇軍;石海鶴;薛錦云;;Spec#語(yǔ)言中的形式化特性[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

4 雷敏;雷友殉;;一種UML到SDL轉(zhuǎn)換方法的研究與應(yīng)用[A];2006通信理論與技術(shù)新進(jìn)展——第十一屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集[C];2006年

5 苗潔君;王克;;密碼模塊的形式化設(shè)計(jì)和驗(yàn)證研究[A];第二十一次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2006年

6 繆道期;;評(píng)審計(jì)算機(jī)安全等級(jí)[A];第二次計(jì)算機(jī)安全技術(shù)交流會(huì)論文集[C];1987年

7 趙曉峰;;城市軌道交通自主化信號(hào)系統(tǒng)全面創(chuàng)新實(shí)踐[A];中國(guó)系統(tǒng)工程學(xué)會(huì)第十八屆學(xué)術(shù)年會(huì)論文集——A12系統(tǒng)科學(xué)與系統(tǒng)工程理論在各個(gè)領(lǐng)域中的應(yīng)用研究[C];2014年

相關(guān)重要報(bào)紙文章 前1條

1 殷杰 安軍 山西大學(xué)科學(xué)技術(shù)哲學(xué)研究中心;21世紀(jì)科學(xué)哲學(xué)的關(guān)鍵詞:語(yǔ)境、科學(xué)理性與形式化[N];中國(guó)社會(huì)科學(xué)報(bào);2011年

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

1 劉艷;互聯(lián)網(wǎng)內(nèi)容分級(jí)服務(wù)技術(shù)標(biāo)準(zhǔn)體系的形式化設(shè)計(jì)與驗(yàn)證[D];華中師范大學(xué);2015年

2 胡健;片上系統(tǒng)高層等價(jià)性檢驗(yàn)關(guān)鍵技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2016年

3 錢(qián)振江;安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D];南京大學(xué);2013年

4 劉強(qiáng);設(shè)計(jì)模式的形式化研究及其EMF實(shí)現(xiàn)[D];華東師范大學(xué);2011年

5 張鵬;形式化方法在云計(jì)算中的應(yīng)用研究[D];吉林大學(xué);2014年

6 劉洋;網(wǎng)絡(luò)式軟件需求驗(yàn)證的形式化方法研究[D];電子科技大學(xué);2013年

7 王邁;語(yǔ)言形式化原理[D];上海外國(guó)語(yǔ)大學(xué);2011年

8 胡靜;基于Pi-演算的Web服務(wù)形式化描述模型[D];天津大學(xué);2013年

9 周寧;代數(shù)化符號(hào)模擬驗(yàn)證的應(yīng)用研究[D];北京交通大學(xué);2015年

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

1 王春曉;MDF連續(xù)平壓質(zhì)量控制形式化建模及優(yōu)化研究[D];東北林業(yè)大學(xué);2015年

2 王亞麗;面向機(jī)器人規(guī)劃的形式化研究[D];北京化工大學(xué);2015年

3 韓佳芮;基于Event-B和MAS的車(chē)站進(jìn)路聯(lián)鎖控制邏輯的形式化方法研究[D];蘭州交通大學(xué);2015年

4 徐世澤;基于Timed RAISE的RBC切換建模與分析[D];蘭州交通大學(xué);2015年

5 郭葉芳;電網(wǎng)控制系統(tǒng)軟件可靠性分析的形式化方法研究[D];華北電力大學(xué);2015年

6 溫晉杰;Z規(guī)范對(duì)國(guó)產(chǎn)化軟件工程實(shí)踐的探討[D];石家莊鐵道大學(xué);2016年

7 丁寧;基于要素投影的事件本體形式化方法及其在情感分析中的應(yīng)用[D];上海大學(xué);2016年

8 沈崗;基于UML的形式化框架及其在安全協(xié)議驗(yàn)證中的應(yīng)用[D];天津大學(xué);2014年

9 傅蘇姍;針對(duì)SOFL形式化軟件規(guī)格說(shuō)明書(shū)完備性的自動(dòng)檢測(cè)方法研究[D];華中科技大學(xué);2015年

10 李婉;群論問(wèn)題的形式化及驗(yàn)證研究[D];西南交通大學(xué);2017年

，

本文編號(hào)：2533174