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

【相似文獻(xiàn)】

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

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

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

3 柴振榮;《編程中的形式化方法及其應(yīng)用》會議[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 曹源;唐濤;徐田華;穆建成;;形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J];交通運(yùn)輸工程學(xué)報(bào);2010年01期

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

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

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

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

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

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

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

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

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

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

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

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

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

3 錢振江;安全操作系統(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 王邁;語言形式化原理[D];上海外國語大學(xué);2011年

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

9 周寧;代數(shù)化符號模擬驗(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的車站進(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ī)范對國產(chǎn)化軟件工程實(shí)踐的探討[D];石家莊鐵道大學(xué);2016年

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

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

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

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

，

本文編號：2533174