關(guān)于形式驗(yàn)證的11個(gè)誤區(qū)

形式驗(yàn)證如何在 signoff之前發(fā)現(xiàn)bug。

形式化驗(yàn)證在數(shù)學(xué)上能夠詳盡地證明一個(gè)芯片設(shè)計(jì)符合一組斷言的能力。

形式化技術(shù)是當(dāng)今芯片成功設(shè)計(jì)、驗(yàn)證和實(shí)現(xiàn)的核心。

形式化驗(yàn)證的優(yōu)點(diǎn)在芯片開發(fā)中是眾所周知和公認(rèn)的。但事實(shí)并非總是如此；幾十年前，形式技術(shù)被廣泛認(rèn)為是一種需要“魔法”才能在實(shí)際項(xiàng)目中成功使用的外來技術(shù)。在這段時(shí)間里，許多在signoff前發(fā)現(xiàn)的真正可怕的bug的成功故事，幫助提高了人們對(duì)形式驗(yàn)證的認(rèn)識(shí)和信心。 用數(shù)學(xué)方式詳盡地證明芯片設(shè)計(jì)滿足一組斷言的能力與仿真形成鮮明對(duì)比，仿真不能證明沒有bug。如果由于合法的設(shè)計(jì)方案違反了斷言而不能實(shí)現(xiàn)證明，形式化工具就會(huì)把這些作為反例提出來，并提供信息以幫助設(shè)計(jì)者調(diào)試它們。用戶提供約束條件，使形式化分析保持在合法范圍內(nèi)，確保反例是在硅片后使用中可能發(fā)生的的真實(shí)故障場(chǎng)景。 這一切聽起來很好，那么為什么不是每個(gè)人都在運(yùn)行形式驗(yàn)證呢？它每天都被數(shù)百家芯片和系統(tǒng)公司的數(shù)千人成功使用，但一些設(shè)計(jì)者和驗(yàn)證工程師仍然不情愿。這可能部分是由于一些持續(xù)存在的關(guān)于形式化技術(shù)的誤區(qū)所致，使它看起來太難或太昂貴。這篇文章研究了這些誤解，并解釋了為什么它們不應(yīng)該成為擔(dān)憂的原因。1. 您需要博士學(xué)位才能使用形式驗(yàn)證。對(duì)于第一代形式化工具來說，這個(gè)誤區(qū)可以說是正確的，這些工具是為學(xué)術(shù)目的而設(shè)計(jì)的。他們需要學(xué)習(xí)一種晦澀難懂的數(shù)學(xué)符號(hào)來指定斷言和約束。這些工具需要大量的手動(dòng)指導(dǎo)，所以大多數(shù)用戶實(shí)際上是專門研究形式驗(yàn)證技術(shù)的教授和博士生。 比如考慮RISC-V弱內(nèi)存模型的負(fù)載值公理。它表示，對(duì)于線程i、j和k，如果線程i執(zhí)行一個(gè)STORE操作，接著線程j執(zhí)行另一個(gè)STORE操作，然后線程k執(zhí)行LOAD操作，那么LOAD從內(nèi)存中檢索的值將是STORE更新的最新值。形式上，數(shù)學(xué)上精確的符號(hào)可以表示這一點(diǎn)，如圖1所示。然而，一個(gè)普通的設(shè)計(jì)或驗(yàn)證工程師可能無法理解這些符號(hào)，它們對(duì)形式方法博士來說是友好的，但對(duì)其他人來說則不然。

1. RISC-V弱內(nèi)存模型的負(fù)載值公理示例。 不過近年來發(fā)生了很大變化。斷言和約束通常使用 SystemVerilog 斷言 （SVA） 指定，SVA 是設(shè)計(jì)人員和驗(yàn)證工程師已經(jīng)知道和使用的 SystemVerilog 語言的子集。正式工具變得更加智能和獨(dú)立，并且更少依賴用戶專業(yè)知識(shí)?，F(xiàn)在，許多都為調(diào)試反例或幫助實(shí)現(xiàn)完整證明提供了可視化和更好的提示。不需要博士學(xué)位。 還有一大類形式化應(yīng)用（App），通常不需要用戶編寫任何斷言。例如，一個(gè)時(shí)鐘域交叉（CDC）工具可以自動(dòng)確定芯片中出現(xiàn)交叉的位置，以及必須證明哪些斷言以保證正確的操作。用戶只需要提供一些關(guān)于時(shí)鐘的信息，其中大部分信息在綜合和布局工具使用的約束文件中已經(jīng)存在。2. 形式化驗(yàn)證很難，因?yàn)槟阈枰问交瘜Ｓ玫囊?guī)范。規(guī)格說明對(duì)于其他形式的驗(yàn)證(如模擬或仿真)是不必要的，這是不正確的SoC 仿真中的固件和驅(qū)動(dòng)程序堆棧已經(jīng)提供了合適的環(huán)境來將激勵(lì)驅(qū)動(dòng)到芯片中進(jìn)行測(cè)試;檢查程序依賴于需求來確定在運(yùn)行測(cè)試時(shí)需要發(fā)生什么。如果沒有規(guī)范，驗(yàn)證工程師就不能為模擬、通用驗(yàn)證方法(UVM)或功能覆蓋編寫定向測(cè)試。 形式化方法對(duì)規(guī)范明顯更敏感，因?yàn)槎x不明確的需求的影響更加嚴(yán)重。形式化測(cè)試（指定為斷言、約束和覆蓋）會(huì)產(chǎn)生意想不到的結(jié)果，因?yàn)樾问交ぞ唑?qū)動(dòng)激勵(lì)模式的所有可能組合。如果從需求中捕獲的約束不準(zhǔn)確，這可能會(huì)導(dǎo)致驅(qū)動(dòng)虛假激勵(lì)。 在許多情況下，從規(guī)范派生形式驗(yàn)證需求的行為可能會(huì)暴露bug。事實(shí)上，一個(gè)好的規(guī)范是成功的形式化驗(yàn)證的一個(gè)隱藏的條件（圖2）。

2. Better specifications are a hidden bargain for formal verification3. 您無法將形式化技術(shù)擴(kuò)展到大型設(shè)計(jì)。這是前幾代形式技術(shù)的另一個(gè)誤區(qū);用戶僅限于分析小型設(shè)計(jì)塊。今天的形式驗(yàn)證工具具有更大的容量，并且許多工具能夠在服務(wù)器或云上以分布式模式運(yùn)行。形式驗(yàn)證的技術(shù)和方法也得到了擴(kuò)展。 設(shè)計(jì)人員和驗(yàn)證工程師通常會(huì)將形式驗(yàn)證應(yīng)用于大型復(fù)雜子系統(tǒng)，包括端到端地驗(yàn)證整個(gè)多線程 64 位處理器。圖 3 顯示了基于Axiomise抽象的解決方案在具有超過 10 億個(gè)門（3.38 億觸發(fā)器）的高度參數(shù)化片上網(wǎng)絡(luò) （NoC） 中捕獲的bug示例。

3. 這個(gè)功能漏洞，在一個(gè)有超過 10億個(gè)門的設(shè)計(jì)中，是 Axiomise 使用 CadenceJasperGold 發(fā)現(xiàn)的。 形式化應(yīng)用程序可能具有更大的容量，因?yàn)樗鼈儗Ｗ⒂趩蝹€(gè)任務(wù)。例如，CDC分析始終在全芯片上運(yùn)行，以檢查整個(gè)時(shí)鐘網(wǎng)絡(luò)。4. 形式驗(yàn)證需要很長(zhǎng)時(shí)間才能收斂。在某些情況下可能會(huì)發(fā)生這種情況，尤其是當(dāng)形式測(cè)試testbench沒有自然設(shè)計(jì)為最佳性能時(shí)。但是，在大多數(shù)情況下，形式屬性收斂得非?？?。 當(dāng)然，形式驗(yàn)證工具的運(yùn)行時(shí)間取決于設(shè)計(jì)大小、設(shè)計(jì)復(fù)雜性以及斷言和約束的數(shù)量。有多種方法可以管理形式驗(yàn)證流程以保持運(yùn)行時(shí)合理。隨著設(shè)計(jì)的增長(zhǎng)以增量方式運(yùn)行和在分布式模式下運(yùn)行都有幫助。5. 形式化技術(shù)只對(duì)構(gòu)建證明有用。這個(gè)誤區(qū)也源于學(xué)術(shù)形式工具，其中的重點(diǎn)完全是實(shí)現(xiàn)完整的證明。雖然完整的證明為設(shè)計(jì)正確性提供了最大的信心，但形式驗(yàn)證通過發(fā)現(xiàn)棘手的極端情況bug（如圖 4 中的示例）來增加價(jià)值。

4. 端到端RISC-V形式驗(yàn)證：使用Axiomise formalISA，在本例中，使用西門子的QuestaPropCheck，在30分鐘內(nèi)完成50%。 圖 5 所示的波形顯示了使用 Axiomise 形式驗(yàn)證解決方案在 ibex RISC-V 內(nèi)核中捕獲的bug。僅當(dāng)調(diào)試請(qǐng)求在控制器 FSM 處于解碼狀態(tài)時(shí)以相同的時(shí)鐘周期到達(dá)時(shí)，此Bug才會(huì)出現(xiàn)在設(shè)計(jì)中。該Bug不會(huì)以任何其他狀態(tài)顯示。調(diào)試到來的精確時(shí)間將使這種bug很難通過動(dòng)態(tài)仿真來捕獲，其中激勵(lì)的可控性和詳盡的覆蓋范圍將是一個(gè)重大挑戰(zhàn)。

5. 由于 ibex RISC-V 內(nèi)核中的bug而導(dǎo)致 BEQ 指令失敗，僅當(dāng)FSM 控制器處于解碼狀態(tài)時(shí)，才會(huì)由傳入的調(diào)試請(qǐng)求觸發(fā)。6. 如果您以 100% 的覆蓋率運(yùn)行了模擬仿真，則不需要正式的技術(shù)。如前所述，形式驗(yàn)證非常適合查找模擬或仿真遺漏的極端情況bug。此外，這個(gè)誤區(qū)夸大了覆蓋指標(biāo)的價(jià)值。它們?cè)谧R(shí)別尚未執(zhí)行的設(shè)計(jì)部分方面非常有價(jià)值，在這種情況下，不可能找到所有bug。 但是，如前所述，仿真無法建立詳盡的數(shù)學(xué)證明。即使是 100% 的功能覆蓋率也不能保證沒有bug逃逸——它只是確認(rèn)了所選指標(biāo)所涵蓋的設(shè)計(jì)部分的實(shí)踐。正式分析將考慮所有可能的行為，并且很可能會(huì)發(fā)現(xiàn)其他bug。7. 形式化技術(shù)只對(duì)查找極端情況的bug有用。許多形式化的用戶對(duì)形式化的bug搜索深信不疑，有時(shí)甚至使他們的管理層認(rèn)為形式化只適合于bug搜索。形式化最大的好處之一是確定在設(shè)計(jì)中不存在與形式化證明的需求有關(guān)的bug。 例如，考慮一下RISC-V。許多以前通過仿真驗(yàn)證的處理器最終都有bug逃逸，然后被形式化抓住。形式化可以毫無疑問地證明，一旦bug被修復(fù)，就不存在bug了，因?yàn)樾问交膶傩宰C明了設(shè)計(jì)的所有可達(dá)到的狀態(tài)（圖6）。

6. 這種情況下與JasperGold 一起使用的 Axiomise formISA 應(yīng)用程序如何用于查找bug并構(gòu)建架構(gòu)正確性證明，以便對(duì) 64 位 RISC-V 處理器進(jìn)行端到端驗(yàn)證。 當(dāng)然，沒有什么比發(fā)現(xiàn)一個(gè)深層的、可怕的、需要翻轉(zhuǎn)芯片的bug更能證明形式化的力量了。一個(gè)驗(yàn)證工程師說 "我們?cè)谀M仿真中永遠(yuǎn)不會(huì)發(fā)現(xiàn)這個(gè)問題"，很快就會(huì)讓人相信形式化。 但是形式驗(yàn)證可以更快地發(fā)現(xiàn)各種bug，包括通常在仿真中發(fā)現(xiàn)的bug。出于這個(gè)原因，今天的芯片項(xiàng)目通常包含多個(gè)區(qū)塊，其中一些區(qū)塊相當(dāng)大，無需任何區(qū)塊級(jí)仿真即可正式驗(yàn)證。8. 一旦你應(yīng)用了形式化技術(shù)，你就不需要模擬及仿真了。通常，每個(gè)形式驗(yàn)證環(huán)境都使用約束來描述接口。這些約束需要在仿真中驗(yàn)證，以檢查它們是否被正確建模和解釋以進(jìn)行形式驗(yàn)證。 此外，形式通常在流程的早期應(yīng)用，以獲得驗(yàn)證shift-left的最大值。當(dāng)設(shè)計(jì)成熟并編碼更多模塊時(shí)，某些接口約束可能不再有效，因此必須在仿真中重新驗(yàn)證它們。 此外，仿真和形式化對(duì)于查找與硬件-軟件交互相關(guān)的bug很有價(jià)值，這些bug僅在軟件在嵌入式或主機(jī)處理器上運(yùn)行時(shí)在模擬或仿真中發(fā)生。同樣，模擬-數(shù)字接口上的bug可能僅在運(yùn)行混合信號(hào)仿真時(shí)發(fā)現(xiàn)。9. 形式化技術(shù)不提供任何覆蓋指標(biāo)，因此很難知道您是否做得足夠多。這顯然是不正確的，因?yàn)樽C明提供了一種形式的覆蓋指標(biāo)。知道設(shè)計(jì)中100%的斷言永遠(yuǎn)不會(huì)被違反，這顯然是一個(gè)強(qiáng)有力的聲明。 但是，所有現(xiàn)代工具現(xiàn)在都會(huì)生成與形式展示中經(jīng)過驗(yàn)證的斷言相關(guān)的代碼覆蓋率視圖（圖 7）。它顯示了在形式證明期間激活并運(yùn)行了哪些設(shè)計(jì)代碼行。

7. JasperGold 覆蓋 32 位 cv32e40p 處理器的檢查器覆蓋率應(yīng)用程序顯示，已通過 RISC-V 的 Axiomise 正式ISA 應(yīng)用程序驗(yàn)證。 以前使用形式工具在沒有任何形式檢查器的情況下評(píng)估代碼覆蓋率。他們?nèi)匀豢梢蕴峁?duì)無法訪問和死代碼的見解，這可能是由于設(shè)計(jì)代碼或配置沖突的結(jié)果。正式工具還廣泛用于證明UVM環(huán)境中無法訪問的代碼覆蓋漏洞可能始終無法訪問，或者可能會(huì)在UVM中發(fā)現(xiàn)覆蓋差距。 Axiomise 開發(fā)的六維覆蓋流程描述了如何從定性和定量上計(jì)算形式覆蓋率（圖 8）。

8. 正規(guī)覆蓋的六個(gè)維度。10. 模擬仿真和形式驗(yàn)證不能合并使用。如前所述，這兩種核查辦法是相輔相成的。每個(gè)人都可以找到對(duì)方可能不會(huì)找到的某些類型的bug。沒有一個(gè)芯片項(xiàng)目運(yùn)行一個(gè)而沒有另一個(gè)?？梢詫⑵湟暈榧僭O(shè)接口假設(shè)以保證形式驗(yàn)證中塊不存在bug，然后在仿真中驗(yàn)證假設(shè)以關(guān)閉完整的循環(huán)。 此外，在仿真中使用形式化來建立覆蓋差距是結(jié)合這兩種技術(shù)的一個(gè)很好的例子。許多跟蹤覆蓋率結(jié)果的項(xiàng)目管理工具從模擬和形式驗(yàn)證中收集指標(biāo)，以提供驗(yàn)證進(jìn)度的統(tǒng)一視圖。這有助于讓老板相信團(tuán)隊(duì)正在滿足指標(biāo)驅(qū)動(dòng)驗(yàn)證的要求。11. 形式化技術(shù)僅對(duì)功能驗(yàn)證有用。斷言、約束、詳盡的數(shù)學(xué)分析、證明和反例的一般概念出現(xiàn)在芯片開發(fā)領(lǐng)域，而不僅僅是檢查功能正確性。 如今，形式驗(yàn)證工具被廣泛部署用于驗(yàn)證架構(gòu)需求、CDC、連接、電源、死鎖、微架構(gòu)功能需求、安全性、安保和 X 傳播（圖 9）。

9. 形式驗(yàn)證的普遍使用。 在DAC 2021上展示的最新示例顯示了如何使用形式驗(yàn)證來查找RISC-V內(nèi)核中的安全漏洞（機(jī)密性，完整性和可用性），并根據(jù)漏洞評(píng)分對(duì)其進(jìn)行排名。安全性的最大挑戰(zhàn)是處理未知的攻擊場(chǎng)景。這就是形式真正閃耀的地方，因?yàn)樗肓烁鞣N輸入激勵(lì)，試圖做到詳盡無遺，找到設(shè)計(jì)師通常永遠(yuǎn)不會(huì)考慮的場(chǎng)景。 部署正式的行為迫使設(shè)計(jì)師和架構(gòu)師考慮在架構(gòu)開發(fā)的早期階段利用漏洞，避免下游出現(xiàn)任何的意外。 形式化技術(shù)是當(dāng)今芯片成功設(shè)計(jì)、驗(yàn)證和實(shí)現(xiàn)的核心。隨著11個(gè)誤區(qū)的消除，相信您將會(huì)毫不猶豫的接受形式驗(yàn)證技術(shù)。

審核編輯 ：李倩