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

1、當(dāng)今片上系統(tǒng)（System-on-chip, SoC）設(shè)計(jì)復(fù)雜度越來(lái)越高，很多復(fù)雜設(shè)計(jì)已經(jīng)無(wú)法從寄存器傳輸級(jí)（Register Transfer Level，RTL）開始建模，對(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)題。

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

3、量。形式化方法存在需要設(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)行了分類，介紹了每種方法的研究現(xiàn)狀，分析了各種方法的優(yōu)缺點(diǎn)。最后分析了目前SoC高層等價(jià)性檢驗(yàn)還存在的問(wèn)題。本文的研究工作圍繞SoC高層等價(jià)性檢驗(yàn)的關(guān)鍵技術(shù)展開，針對(duì)目前SoC高層等價(jià)性檢驗(yàn)中存在的問(wèn)題，提出了新的算法并取得了如下創(chuàng)新成果:
　　首先，針對(duì)模擬

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

5、比較觀察變量的值是否相等。實(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，F(xiàn)SMD），隨后提取FSMD中所有深度路徑。利用測(cè)試矢量生成技

6、術(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)題，提

7、出了一種基于機(jī)器學(xué)習(xí)的等價(jià)性檢驗(yàn)算法。該方法無(wú)需提取模型的FSMD，減小了驗(yàn)證開銷。將狀態(tài)輸出語(yǔ)句插入系統(tǒng)級(jí)與RTL代碼中，利用硬件設(shè)計(jì)開發(fā)過(guò)程中產(chǎn)生的大量測(cè)試數(shù)據(jù)，模擬系統(tǒng)級(jí)與RTL模型，得到FSMD狀態(tài)序列。利用機(jī)器學(xué)習(xí)技術(shù)劃分狀態(tài)序列，得到分類狀態(tài)集合。根據(jù)狀態(tà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é)

8、習(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à)性