解讀芯片驗(yàn)證中的機(jī)器學(xué)習(xí)技術(shù)

ChatGPT浪潮，在各行各業(yè)引起了不小的顛覆，芯片驗(yàn)證也不無(wú)例外。隨著芯片設(shè)計(jì)復(fù)雜度的不斷增加，交付周期越來(lái)越短。設(shè)計(jì)工程師可能需要花費(fèi)將近一半的時(shí)間在功能驗(yàn)證上。功能驗(yàn)證本身具有計(jì)算和數(shù)據(jù)密集的性質(zhì)，因此也成為了機(jī)器學(xué)習(xí)（ML）技術(shù)的理想領(lǐng)域，二者的融合交叉嘗試也一直沒(méi)有間斷。

許多ML算法已經(jīng)在功能驗(yàn)證的不同領(lǐng)域進(jìn)行了嘗試，并取得了不錯(cuò)的效果。ML在功能驗(yàn)證中的應(yīng)用主要分為：需求工程、靜態(tài)代碼分析、驗(yàn)證加速、覆蓋率收集和BUG的檢測(cè)及定位。

需求工程

需求工程(Requirement Engineering)一般指定義、文檔化和維護(hù)驗(yàn)證需求的過(guò)程，這也是保證最終的設(shè)計(jì)符合spec的重要一環(huán)。

需求定義

需求定義(Requirement definition)將自然語(yǔ)言（NL）的驗(yàn)證目標(biāo)轉(zhuǎn)化為標(biāo)準(zhǔn)化的驗(yàn)證規(guī)范。傳統(tǒng)的驗(yàn)證flow需要多次手動(dòng)校對(duì)以確保質(zhì)量，借助機(jī)器學(xué)習(xí)，目前有兩種經(jīng)典的方法進(jìn)行自動(dòng)化翻譯。

第一種方法是引入約束自然語(yǔ)言（CNL）進(jìn)行描述需求，然后使用基于模板的翻譯引擎進(jìn)行翻譯。只要CNL配套的工具足夠強(qiáng)大，CNL可以描述FV中遇到的大多數(shù)需求。但這需要開發(fā)人員學(xué)習(xí)新的語(yǔ)言，具有一定的門檻[9]。

第二種方法是使用經(jīng)典的自然語(yǔ)言處理（NLP）來(lái)解析自然語(yǔ)言（NL）的需求，提取出關(guān)鍵要素[10]。隨著大模型的訓(xùn)練和演進(jìn)，后續(xù)可以直接將自然語(yǔ)言的需求翻譯為SystemVerilog、Assertions (SVA)、Property Specification Language (PSL)或其他語(yǔ)言。目前已經(jīng)有一些端到端的翻譯嘗試，但離大規(guī)模使用還有比較大的gap，主要的障礙在于訓(xùn)練數(shù)據(jù)集的稀缺[11]。

代碼總結(jié)和翻譯

Code summarization and translation to NL，與需求定義相反，將代碼翻譯成自然語(yǔ)言?？梢詭椭_發(fā)人員理解一些復(fù)雜的邏輯代碼，提升代碼的可維護(hù)性和可讀性。

但目前，IC設(shè)計(jì)驗(yàn)證領(lǐng)域的Code summarization幾乎沒(méi)有嘗試。不過(guò)跨語(yǔ)言模型的發(fā)展或許有助于將其他編程語(yǔ)言的實(shí)踐經(jīng)驗(yàn)轉(zhuǎn)移至IC設(shè)計(jì)。需要注意的是，IC設(shè)計(jì)和驗(yàn)證的code存在語(yǔ)義的并發(fā)，如fork，module等，這在其他語(yǔ)言中并不常見。

特性挖掘

特性挖掘(Specification mining)在軟件工程領(lǐng)域比較常見，Dallmeier、Valentin等人以及Wenchao、Forin和Seshia等人都曾對(duì)進(jìn)行研究[14][15]。Specification mining從待測(cè)試設(shè)計(jì)(DUT)的執(zhí)行中提取規(guī)范的方法，用于替代手寫spec的方法。機(jī)器學(xué)習(xí)可以從仿真中挖掘到某些重復(fù)的模式，可能是DUT的預(yù)期行為。此外很少出現(xiàn)的事件模式可以視為異常，也可用于debug和調(diào)試[16]。

Azeem等人提出了一種通用的軟件工程方法，利用機(jī)器學(xué)習(xí)來(lái)尋找spec，并找到可能存在問(wèn)題的協(xié)議實(shí)現(xiàn)[17]。

代碼分析

芯片開發(fā)中的錯(cuò)誤修復(fù)成本呈現(xiàn)一種指數(shù)級(jí)增長(zhǎng)的規(guī)律，越是靠后的開發(fā)階段，其錯(cuò)誤修復(fù)成本越高。因此靜態(tài)代碼分析(Static code analysis)可以作為設(shè)計(jì)開發(fā)早期階段的一種有效手段，用來(lái)改進(jìn)代碼質(zhì)量和可維護(hù)性。

代碼質(zhì)量評(píng)價(jià)

Code smell detection and quality assessment.

Code smell指那些功能正確，但是維護(hù)性以及可讀性差，違反一些規(guī)范或者最佳實(shí)踐。典型的例子就是在多處重復(fù)編寫相同功能的代碼。

常見的code smell檢測(cè)，依賴于定義好的規(guī)則來(lái)識(shí)別源代碼中的問(wèn)題。而機(jī)器學(xué)習(xí)的方法是，在大量可用的源代碼上進(jìn)行訓(xùn)練，以識(shí)別出code smell的模式，而不是手動(dòng)編寫這些規(guī)則或指標(biāo)。Fontana等和Aniche等所述的研究表明，使用機(jī)器學(xué)習(xí)的方法可以顯著減少模式實(shí)現(xiàn)的工作量[18][19]，并幫助開發(fā)人員持續(xù)改進(jìn)產(chǎn)品質(zhì)量。此外，基于機(jī)器學(xué)習(xí)的代碼重構(gòu)可以為改善code smell提供有用的提示，甚至進(jìn)一步提供更改方案。

遺憾的是，這方面的應(yīng)用在FV中還不太明顯，而且缺乏大規(guī)模的訓(xùn)練數(shù)據(jù)集也是其重要的阻礙因素。

輔助編碼

簡(jiǎn)單的代碼補(bǔ)全或者提示是集成開發(fā)環(huán)境（IDE）的標(biāo)準(zhǔn)功能，開發(fā)人員的效率也可以得到提升。而深度學(xué)習(xí)則提出了更高級(jí)的技術(shù)[21]，并且正在快速迭代成熟[22]。現(xiàn)在可以從許多大規(guī)模開源代碼庫(kù)中訓(xùn)練具有數(shù)十億個(gè)參數(shù)的人工神經(jīng)網(wǎng)絡(luò)（ANN），并給出開發(fā)人員實(shí)現(xiàn)意圖或基于上下文的合理代碼片段的建議。

ML也有可能幫助IC開發(fā)人員通過(guò)語(yǔ)義代碼來(lái)進(jìn)行搜索，通過(guò)自然語(yǔ)言查詢來(lái)檢索相關(guān)代碼[23]。雖然理論上，應(yīng)用于其他編程語(yǔ)言的相同ML技術(shù)可以應(yīng)用于IC設(shè)計(jì)，但目前還沒(méi)有相關(guān)的研究。

驗(yàn)證加速

Verification Acceleration包括Formal和Simulation-based兩種。

Formal verification

Formal使用形式化數(shù)學(xué)算法來(lái)證明設(shè)計(jì)的正確性。作為一種統(tǒng)計(jì)方法，機(jī)器學(xué)習(xí)雖然不能直接解決Formal驗(yàn)證的復(fù)雜度問(wèn)題，但是在資源調(diào)度方面很有幫助。通過(guò)預(yù)測(cè)計(jì)算資源和解決問(wèn)題的概率，然后以最佳方式利用這些資源來(lái)縮短驗(yàn)證時(shí)間 [25]，即先調(diào)度具有更低計(jì)算資源消耗、可求解成功的任務(wù)?；?a target="_blank">Ada-boost決策樹的分類器可以將成功解決的比例從95%提高到97%，平均加速1.85倍。[25]中的另一個(gè)實(shí)驗(yàn)?zāi)軌蝾A(yù)測(cè)Formal驗(yàn)證的資源需求，平均誤差為32%。

Simulation-based verification

和Formal驗(yàn)證不同，simulation通過(guò)對(duì)DUT添加隨機(jī)或固定模式的激勵(lì)，把DUT輸出和參考輸出進(jìn)行比較，以驗(yàn)證設(shè)計(jì)行為的正確性?；趕imulation的功能驗(yàn)證也是芯片開發(fā)流程中耗時(shí)較長(zhǎng)的一步。

機(jī)器學(xué)習(xí)在該領(lǐng)域的一個(gè)可能思路是對(duì)復(fù)雜系統(tǒng)的行為進(jìn)行建模和預(yù)測(cè)。多層感知器（MLP）（一種至少具有一個(gè)隱藏層的前饋人工神經(jīng)網(wǎng)絡(luò)）可以以任意精度逼近任何連續(xù)函數(shù)。而標(biāo)準(zhǔn)化循環(huán)神經(jīng)網(wǎng)絡(luò)（RNNs）（一種特殊形式的人工神經(jīng)網(wǎng)絡(luò)）則可以逼近任何具有存儲(chǔ)器的動(dòng)態(tài)系統(tǒng)。先進(jìn)的機(jī)器學(xué)習(xí)可以使人工神經(jīng)網(wǎng)絡(luò)可以對(duì)一些IC設(shè)計(jì)模塊的行為進(jìn)行建模，以加速其仿真。根據(jù)人工智能加速器的能力和機(jī)器學(xué)習(xí)模型的復(fù)雜性，可能會(huì)實(shí)現(xiàn)顯著的加速。

測(cè)試激勵(lì)產(chǎn)生和覆蓋率收集

在simulation中，除了手工編寫測(cè)試用例外，還有較為常見的受限隨機(jī)測(cè)試方法，以及基于圖形化的測(cè)試平臺(tái)生成技術(shù)。覆蓋率在驗(yàn)證前期會(huì)增長(zhǎng)很快，但也存在“長(zhǎng)尾”效應(yīng)。最后20%的覆蓋率閉環(huán)，可能需要80%的資源消耗。所以機(jī)器學(xué)習(xí)在這方面的應(yīng)用，也都集中在如何提升覆蓋率的收集速度。

一些研究表明引入機(jī)器學(xué)習(xí)，可以獲取比隨機(jī)測(cè)試更有效的case。大多數(shù)研究也都是基于“黑盒模型”，假設(shè)DUT是一個(gè)黑盒，其輸入有測(cè)試激勵(lì)控制，并監(jiān)測(cè)輸出。其重點(diǎn)是從歷史輸入/輸出/觀測(cè)數(shù)據(jù)中學(xué)習(xí)，進(jìn)而調(diào)整隨機(jī)測(cè)試生成器或減少不必要的測(cè)試上，而不是試圖學(xué)習(xí)DUT的行為。

在[31]的研究中，使用基于強(qiáng)化學(xué)習(xí)（RL）的模型來(lái)從DUT的輸出中學(xué)習(xí)并預(yù)測(cè)緩存控制器的最有效的case。當(dāng)ML模型給出的反饋是FIFO深度時(shí)，模型能夠從歷史結(jié)果中學(xué)習(xí)，并在幾次迭代中達(dá)到FIFO深度的全覆蓋，明顯優(yōu)于基于隨機(jī)測(cè)試的方法。但文中沒(méi)有進(jìn)一步實(shí)驗(yàn)證明在更復(fù)雜的設(shè)計(jì)中的表現(xiàn)，在較為復(fù)雜的設(shè)計(jì)中，反饋不容易定義。

[28]引入了一個(gè)更精細(xì)的ML架構(gòu)，對(duì)每個(gè)覆蓋點(diǎn)都訓(xùn)練一個(gè)ML模型。還采用了三進(jìn)制分類器：是否應(yīng)模擬測(cè)試、丟棄或用于進(jìn)一步訓(xùn)練模型。使用支持向量機(jī)（SVM）、隨機(jī)森林和深度神經(jīng)網(wǎng)絡(luò)對(duì)CPU設(shè)計(jì)進(jìn)行了實(shí)驗(yàn)，結(jié)果表明，達(dá)到100%的覆蓋率時(shí)，模型能夠減少67% ~ 80%的case數(shù)量。對(duì)存在狀態(tài)機(jī)設(shè)計(jì)的結(jié)果表明，與定向序列生成相比，減少了69%和72%。

但是，上面的這些研究都僅針對(duì)自有的設(shè)計(jì)進(jìn)行，其模型的訓(xùn)練結(jié)果無(wú)法作為先驗(yàn)知識(shí)，被其他模型使用。其原因也是模型的訓(xùn)練數(shù)據(jù)不可用。

Bug analysis

Bug analysis是指找出潛在的bug，定位包含bug的代碼塊，并提供修改建議。機(jī)器學(xué)習(xí)已用于幫助開發(fā)人員識(shí)別設(shè)計(jì)中的bug，并更快地修復(fù)bug。Bug analysis需要解決三個(gè)問(wèn)題：通過(guò)其根本原因進(jìn)行bug聚類、分類根本原因和提供修改建議。大部分的研究集中在前兩個(gè)問(wèn)題上，還沒(méi)有第三個(gè)問(wèn)題的研究結(jié)果。

在研究[34]中的方法，使用半結(jié)構(gòu)化的模擬日志文件。它從日志文件中提取元數(shù)據(jù)和消息行的616個(gè)不同特征。機(jī)器學(xué)習(xí)可以預(yù)測(cè)哪些提交最有可能包含bug，可以顯著減少手動(dòng)bug-hunting的時(shí)間。但是，由于采用的ML技術(shù)一般相對(duì)簡(jiǎn)單，無(wú)法兼顧代碼中多樣化的語(yǔ)義，以及無(wú)法從歷史bug修復(fù)中學(xué)習(xí)。因此，這些模型一般也無(wú)法解釋bug發(fā)生的原因和方式，無(wú)法自動(dòng)或半自動(dòng)地修復(fù)bug。

ML前沿技術(shù)及其在FV中的應(yīng)用

近年來(lái)，機(jī)器學(xué)習(xí)技術(shù)、模型和算法方面取得了重大突破。如果將這些新興技術(shù)引入到FV中，則有希望可以解決FV面臨的諸多難題?；诖罅课谋菊Z(yǔ)料庫(kù)訓(xùn)練出的具有數(shù)十億參數(shù)的自然語(yǔ)言處理模型，表現(xiàn)出接近或超過(guò)人類水平的性能，例如問(wèn)答、機(jī)器翻譯、文本分類、概括性總結(jié)等。

在代碼分析中應(yīng)用這些研究成果，也展示了這些模型的優(yōu)勢(shì)[12][24]。這些模型可以吸收大量的訓(xùn)練數(shù)據(jù)，將所學(xué)習(xí)的知識(shí)進(jìn)行結(jié)構(gòu)化，并提供易于訪問(wèn)的方式。這種能力在靜態(tài)代碼分析、需求工程和代碼輔助工具中是非常重要。

圖形神經(jīng)網(wǎng)絡(luò)(GNN)的進(jìn)展為FV帶來(lái)了新的機(jī)遇[33]。其研究將設(shè)計(jì)轉(zhuǎn)換成一種代碼/數(shù)據(jù)流圖，然后進(jìn)一步使用GNN來(lái)幫助預(yù)測(cè)case的覆蓋率。這種白盒方法可以洞悉設(shè)計(jì)中的控制和數(shù)據(jù)流，從而生成針對(duì)性的測(cè)試。圖形可以表示在驗(yàn)證過(guò)程中遇到的復(fù)雜多樣化的關(guān)系、結(jié)構(gòu)和語(yǔ)義信息。進(jìn)而通過(guò)在圖上訓(xùn)練機(jī)器學(xué)習(xí)模型，可以為許多FV問(wèn)題提供解決方案，例如bug analysis和coverage closure。

大規(guī)模開源驗(yàn)證數(shù)據(jù)現(xiàn)狀

盡管在 FV 中應(yīng)用機(jī)器學(xué)習(xí)取得了一些不錯(cuò)的研究成果，但要實(shí)現(xiàn)成熟和大規(guī)模的應(yīng)用，還必須解決許多難題。其中最大的挑戰(zhàn)是缺乏訓(xùn)練數(shù)據(jù)集。

由于缺乏大型數(shù)據(jù)集，許多研究只能采用相對(duì)原始的機(jī)器學(xué)習(xí)技術(shù)，這些技術(shù)只需要數(shù)百個(gè)樣本的小型訓(xùn)練數(shù)據(jù)集。這種情況不利于高級(jí)機(jī)器學(xué)習(xí)技術(shù)和算法的應(yīng)用。IC設(shè)計(jì)一直以來(lái)是私有化的，設(shè)計(jì)及其關(guān)聯(lián)的驗(yàn)證數(shù)據(jù)（包括驗(yàn)證計(jì)劃、仿真設(shè)置、斷言、回歸結(jié)果、仿真日志、覆蓋數(shù)據(jù)、跟蹤文件、修訂和提交）都是其公司內(nèi)部的商業(yè)秘密數(shù)據(jù)。一項(xiàng)調(diào)查顯示，典型的機(jī)器學(xué)習(xí)項(xiàng)目會(huì)花費(fèi)團(tuán)隊(duì)高達(dá)70%的時(shí)間用于數(shù)據(jù)準(zhǔn)備。包括數(shù)據(jù)清理、報(bào)告和可視化。

缺乏高質(zhì)量的訓(xùn)練數(shù)據(jù)和高成本的數(shù)據(jù)準(zhǔn)備是研究 FV 的機(jī)器學(xué)習(xí)面臨的重大障礙。目前很少有研究人員愿意公開分享他們的數(shù)據(jù)、代碼或機(jī)器學(xué)習(xí)模型，因此其研究結(jié)果難以被其他研究人員重復(fù)或驗(yàn)證。

在2022年5月在GitHub、RISC-V和OpenCores上的搜索結(jié)果，在開源可用的設(shè)計(jì)數(shù)據(jù)有限，驗(yàn)證數(shù)據(jù)更少。

共約1000萬(wàn)行代碼和注釋，這個(gè)規(guī)模幾乎無(wú)法與其他流行編程語(yǔ)言中的數(shù)百萬(wàn)個(gè)項(xiàng)目和數(shù)十億行源代碼相比。更重要的是，與驗(yàn)證相關(guān)的數(shù)據(jù)非常稀缺。即使可以從源代碼集中生成驗(yàn)證數(shù)據(jù)，但也必須投入巨大的人力來(lái)進(jìn)行仿真驗(yàn)證，以提取有效數(shù)據(jù)。

業(yè)界觀察

如果機(jī)器學(xué)習(xí)能在FV中的成功應(yīng)用，除了數(shù)據(jù)的稀缺性問(wèn)題外，還有幾個(gè)問(wèn)題需要解決。

模型泛化是許多機(jī)器學(xué)習(xí)研究結(jié)果中最常見的挑戰(zhàn)之一。泛化能力衡量了將訓(xùn)練出來(lái)的模型應(yīng)用于新問(wèn)題時(shí)的易用性。在特定類型的設(shè)計(jì)、編碼風(fēng)格、某些特定項(xiàng)目或某些小眾數(shù)據(jù)的數(shù)據(jù)集上訓(xùn)練出的模型，可能無(wú)法很好地適用于其他領(lǐng)域。如果模型無(wú)法做到很好的泛化能力，其工業(yè)應(yīng)用價(jià)值非常有限。

模型的可擴(kuò)展性是另一個(gè)挑戰(zhàn)。一個(gè)模型可能在相對(duì)簡(jiǎn)單的設(shè)計(jì)中表現(xiàn)得很好。然而，無(wú)法保證它在應(yīng)用于數(shù)十億個(gè)RTL門的大型設(shè)計(jì)，以及來(lái)自多個(gè)開發(fā)團(tuán)隊(duì)的代碼時(shí)能夠同樣有效。模型壓縮投入、額外的計(jì)算資源，都是引入機(jī)器學(xué)習(xí)需要考慮的成本。

第三個(gè)挑戰(zhàn)與機(jī)器學(xué)習(xí)應(yīng)用中的數(shù)據(jù)管理有關(guān)。在實(shí)際應(yīng)用中，用于訓(xùn)練機(jī)器學(xué)習(xí)模型的數(shù)據(jù)集所有者、FV工具開發(fā)者和工具用戶可能屬于不同的組織。結(jié)合計(jì)算能力的分布和 MLOps 專業(yè)知識(shí)的可用性，他們共同決定了選擇哪些機(jī)器學(xué)習(xí)模型。例如，數(shù)據(jù)私有化，而且沒(méi)有機(jī)器學(xué)習(xí)基礎(chǔ)設(shè)施的組織，可能無(wú)法使用需要大量計(jì)算的機(jī)器學(xué)習(xí)模型。

總結(jié)

FV本質(zhì)上是一個(gè)數(shù)據(jù)分析問(wèn)題，盡管使用了不同的機(jī)器學(xué)習(xí)技術(shù)，但研究大多仍采用原始的機(jī)器學(xué)習(xí)技術(shù)，并受到訓(xùn)練數(shù)據(jù)規(guī)模的限制。目前的機(jī)器學(xué)習(xí)應(yīng)用還沒(méi)有完全利用許多語(yǔ)義、關(guān)系和結(jié)構(gòu)信息，開源和高質(zhì)量的訓(xùn)練數(shù)據(jù)可能是目前遇到的最大問(wèn)題。機(jī)器學(xué)習(xí)在FV領(lǐng)域的應(yīng)用是非常有希望的，前途是光明的，不過(guò)目前距離大規(guī)模的應(yīng)用，還須更多努力。