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

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

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

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

4、方法驗證效率較低，驗證開銷大，無法保證設計完備性等問題，本文提出了一種基于覆蓋率指導的模擬等價性檢驗算法。首先分析了系統(tǒng)級與事務級（Transaction Level Modeling，TLM）的相似性（算法描述，模塊劃分，數(shù)據(jù)類型）以及覆蓋率在不同層次間的關(guān)系，根據(jù)分析結(jié)果，引入代碼覆蓋率和功能覆蓋率作為高層測試矢量的質(zhì)量測度。利用復合覆蓋率（代碼覆蓋率和功能覆蓋率）在系統(tǒng)級產(chǎn)生高質(zhì)量測試矢量，并利用該測試矢量模擬系統(tǒng)級與TLM模型，

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

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

7、出了一種基于機器學習的等價性檢驗算法。該方法無需提取模型的FSMD，減小了驗證開銷。將狀態(tài)輸出語句插入系統(tǒng)級與RTL代碼中，利用硬件設計開發(fā)過程中產(chǎn)生的大量測試數(shù)據(jù)，模擬系統(tǒng)級與RTL模型，得到FSMD狀態(tài)序列。利用機器學習技術(shù)劃分狀態(tài)序列，得到分類狀態(tài)集合。根據(jù)狀態(tài)的類別，構(gòu)造系統(tǒng)級與RTL對應的路徑。最后利用符號模擬和約束求解器驗證對應路徑的等價性。該方法能夠有效解決差異巨大設計之間的等價性并能驗證無對應信息設計的等價性。利用機器學

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