基于多核片上系統(tǒng)的自動(dòng)驗(yàn)證平臺(tái)關(guān)鍵技術(shù)研究的綜述報(bào)告

基于多核片上系統(tǒng)的自動(dòng)驗(yàn)證平臺(tái)關(guān)鍵技術(shù)研究的綜述報(bào)告隨著芯片技術(shù)的不斷進(jìn)步，單核CPU已經(jīng)不能滿足大規(guī)模計(jì)算的需求，多核片上系統(tǒng)（Multi-coreSystem-on-Chip，簡(jiǎn)稱MPSoC）逐漸成為當(dāng)前高性能計(jì)算的主要形式。為了保證MPSoC的正確性和可靠性，自動(dòng)驗(yàn)證平臺(tái)成為了必不可少的技術(shù)手段。本文將從多核片上系統(tǒng)自動(dòng)驗(yàn)證平臺(tái)關(guān)鍵技術(shù)進(jìn)行綜述，包括驗(yàn)證模型構(gòu)建、驗(yàn)證算法以及驗(yàn)證案例應(yīng)用等方面。一、驗(yàn)證模型構(gòu)建MPSoC的自動(dòng)驗(yàn)證平臺(tái)的關(guān)鍵是構(gòu)建一個(gè)驗(yàn)證模型，以便對(duì)硬件的正確性進(jìn)行驗(yàn)證。驗(yàn)證模型主要包括以下兩個(gè)方面。1.功能模型MPSoC功能模型用于描述系統(tǒng)的功能實(shí)現(xiàn)。在功能模型中，需要對(duì)系統(tǒng)的各種功能進(jìn)行抽象描述，構(gòu)建抽象層次目標(biāo)模型（AbstractTargetModel，ATM）是驗(yàn)證功能模型的常用方法。ATM比系統(tǒng)具體實(shí)現(xiàn)的RTL還要高一個(gè)抽象層次，但又要比系統(tǒng)級(jí)別的規(guī)格說明書要具體，ATM是最接近于規(guī)格說明的模型。這樣的模型通常是在Verilog或VHDL的RTL級(jí)描述縮減的模型，通常不包括具體的設(shè)計(jì)元素，例如鎖或多媒體協(xié)處理器。2.可訪問性模型MPSoC可訪問性模型用于描述系統(tǒng)的輸入輸出特性。在可訪問性模型中，需要進(jìn)行端口剖析，從而確定正確的端口連接文件，以確保先前驗(yàn)證模型的正確性，以及確保正確的控制表達(dá)式，以允許所有端口與模擬器進(jìn)行通信。如果沒有正確的驗(yàn)證模型，將無法進(jìn)行任何其他模擬或驗(yàn)證。二、驗(yàn)證算法驗(yàn)證算法是MPSoC自動(dòng)驗(yàn)證平臺(tái)的另一個(gè)關(guān)鍵技術(shù)，旨在通過算法驗(yàn)證模型的正確性。下面介紹兩種常見的驗(yàn)證算法。1.基于模型檢測(cè)的驗(yàn)證算法模型檢測(cè)是一種常用的自動(dòng)驗(yàn)證技術(shù)，由計(jì)算機(jī)自動(dòng)推導(dǎo)系統(tǒng)模型的狀態(tài)，以確定是否滿足某些性質(zhì)。這種技術(shù)通常采用有限狀態(tài)機(jī)（FiniteStateMachine，F(xiàn)SM）模型來表示目標(biāo)硬件的行為，常用的算法有SPIN和NuSMV等。但是，由于MPSoC系統(tǒng)的規(guī)模較大，這種方法通常會(huì)面臨狀態(tài)爆炸的問題。2.基于仿真的驗(yàn)證算法基于仿真的驗(yàn)證算法利用VerificationIP（VIP）來驗(yàn)證設(shè)計(jì)的標(biāo)準(zhǔn)和協(xié)議，如AMBA和PCIExpress等。VIP主要以外部硬件接口或示波器格式為輸入，以檢查設(shè)計(jì)是否符合第三方架構(gòu)標(biāo)準(zhǔn)為目標(biāo)。然后，VIP可以產(chǎn)生覆蓋率報(bào)告，以幫助找到測(cè)試中未發(fā)現(xiàn)的漏洞，并針對(duì)性地進(jìn)行調(diào)整。三、驗(yàn)證案例應(yīng)用MPSoC的自動(dòng)驗(yàn)證平臺(tái)已成為當(dāng)前大規(guī)模計(jì)算的主要形式，本文對(duì)幾個(gè)驗(yàn)證案例的應(yīng)用進(jìn)行簡(jiǎn)要介紹。1.高速緩存一致性高速緩存一致性是MPSoC驗(yàn)證的一個(gè)重要方面，系統(tǒng)必須確保處理器可以訪問所有的高速緩存，并且這些緩存實(shí)時(shí)保持一致。通過將掃描鏈與同步算法相結(jié)合來檢測(cè)高速緩存一致性。2.應(yīng)用程序編程接口（API）驗(yàn)證API驗(yàn)證對(duì)于保證操作系統(tǒng)和軟件庫的正確性非常重要。該領(lǐng)域的技術(shù)包括RTL和TransactionLevelModel（TLM）驗(yàn)證等，并且需要使用高級(jí)電子設(shè)計(jì)自動(dòng)化（EDA）工具。3.硬件安全性驗(yàn)證硬件電路在執(zhí)行中可能會(huì)遭受外部攻擊或鎖定，使系統(tǒng)不能正常運(yùn)行。為了防止這種攻擊，硬件電路必須經(jīng)過安全性驗(yàn)證。該領(lǐng)域的技術(shù)包括電磁分析和物理攻擊分析等?？偟膩碚f，多核片上系統(tǒng)自動(dòng)驗(yàn)證平臺(tái)是保證硬件電路正常運(yùn)行和高性能