片上系統(tǒng)高層等價性檢驗(yàn)關(guān)鍵技術(shù)研究.pdf

1、當(dāng)今片上系統(tǒng)（System-on-chip, SoC）設(shè)計復(fù)雜度越來越高，很多復(fù)雜設(shè)計已經(jīng)無法從寄存器傳輸級（Register Transfer Level，RTL）開始建模，對高層次行為和體系結(jié)構(gòu)模型的需求越來越迫切，系統(tǒng)級功能驗(yàn)證已經(jīng)成為影響SoC設(shè)計效率和質(zhì)量的最重要環(huán)節(jié)。針對SoC系統(tǒng)級功能驗(yàn)證各層巨大差異帶來的重復(fù)工作多、驗(yàn)證效率低下等突出問題，本文研究SoC高層等價性檢驗(yàn)技術(shù)，在理論和實(shí)踐上解決目前高層等價性檢驗(yàn)存在的問題。

2、
　　SoC高層等價性檢驗(yàn)技術(shù)主要采用模擬方法，斷言方法和形式化方法。模擬方法主要是通過比較在相同的測試激勵下，不同層次設(shè)計輸出結(jié)果是否相同。斷言的方法主要是通過驗(yàn)證不同層次設(shè)計是否滿足相同的功能斷言。形式化方法主要利用形式化技術(shù)（模型檢驗(yàn)，謂詞抽象和符號模擬）驗(yàn)證不同層次設(shè)計是否完全等價。三類方法目前都面臨一些困難。模擬方法通過模擬大量的測試矢量進(jìn)行驗(yàn)證，開銷較大并且無法保證測試的完備性。斷言方法的驗(yàn)證質(zhì)量完全取決于定義斷言的質(zhì)

3、量。形式化方法存在需要設(shè)計之間的映射關(guān)系和狀態(tài)空間爆炸等問題。
　　本文首先綜述了SoC高層等價性檢驗(yàn)技術(shù)及相關(guān)技術(shù)迄今為止的研究進(jìn)展，對現(xiàn)有SoC高層等價性檢驗(yàn)方法進(jìn)行了分類，介紹了每種方法的研究現(xiàn)狀，分析了各種方法的優(yōu)缺點(diǎn)。最后分析了目前SoC高層等價性檢驗(yàn)還存在的問題。本文的研究工作圍繞SoC高層等價性檢驗(yàn)的關(guān)鍵技術(shù)展開，針對目前SoC高層等價性檢驗(yàn)中存在的問題，提出了新的算法并取得了如下創(chuàng)新成果:
　　首先，針對模擬

4、方法驗(yàn)證效率較低，驗(yàn)證開銷大，無法保證設(shè)計完備性等問題，本文提出了一種基于覆蓋率指導(dǎo)的模擬等價性檢驗(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模型，

5、比較觀察變量的值是否相等。實(shí)驗(yàn)結(jié)果表明，該方法能重用高層的驗(yàn)證努力，高效地驗(yàn)證系統(tǒng)級與TLM模型的等價性，同時還能有效地提高模擬方法的驗(yàn)證完備性。
　　其次，針對形式化方法需要設(shè)計映射信息和驗(yàn)證效率較低等問題，提出了一種基于深度路徑的等價性檢驗(yàn)算法。該方法提取系統(tǒng)級模型的帶數(shù)據(jù)通路的有限狀態(tài)機(jī)（Finite State Machines with Data Paths，F(xiàn)SMD），隨后提取FSMD中所有深度路徑。利用測試矢量生成技

6、術(shù)，產(chǎn)生所有深度路徑的測試矢量。將輸出狀態(tài)語句插入RTL模型中，利用產(chǎn)生的測試矢量模擬RTL模型，輸出對應(yīng)的深度路徑。最后，利用符號模擬和約束求解器驗(yàn)證對應(yīng)路徑的等價性。該方法能夠驗(yàn)證無映射信息的設(shè)計之間的等價性，同時，只需驗(yàn)證對應(yīng)的深度路徑，避免了盲目的深度路徑比較。實(shí)驗(yàn)結(jié)果表明，該方法相比于目前的基于深度路徑的方法，減少了深度路徑驗(yàn)證次數(shù)，提高了等價性檢驗(yàn)效率。
　　再次，針對形式化方法需要設(shè)計映射信息和驗(yàn)證效率較低等問題，提

7、出了一種基于機(jī)器學(xué)習(xí)的等價性檢驗(yàn)算法。該方法無需提取模型的FSMD，減小了驗(yàn)證開銷。將狀態(tài)輸出語句插入系統(tǒng)級與RTL代碼中，利用硬件設(shè)計開發(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)路徑的等價性。該方法能夠有效解決差異巨大設(shè)計之間的等價性并能驗(yàn)證無對應(yīng)信息設(shè)計的等價性。利用機(jī)器學(xué)

8、習(xí)技術(shù)識別對應(yīng)的路徑，減少盲目的路徑比較。實(shí)驗(yàn)結(jié)果表明，該方法能夠高效的驗(yàn)證無映射信息的系統(tǒng)級與RTL設(shè)計等價性。
　　最后，針對高級綜合調(diào)度前后驗(yàn)證效率不高，循環(huán)結(jié)構(gòu)需要多次迭代等問題，提出了一種基于共享值圖（Shared-Value Graph，SVG）的等價性檢驗(yàn)算法。該方法利用割點(diǎn)技術(shù)，產(chǎn)生高級綜合調(diào)度前后設(shè)計的潛在互模擬位置，利用SVG驗(yàn)證互模擬位置之間公共變量的等價性。割點(diǎn)技術(shù)能夠劃分大規(guī)模設(shè)計，驗(yàn)證大規(guī)模設(shè)計的等價性