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

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

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

形式化驗證的優(yōu)點在芯片開發(fā)中是眾所周知和公認的。但事實并非總是如此；幾十年前，形式技術(shù)被廣泛認為是一種需要“魔法”才能在實際項目中成功使用的外來技術(shù)。在這段時間里，許多在signoff前發(fā)現(xiàn)的真正可怕的bug的成功故事，幫助提高了人們對形式驗證的認識和信心。 用數(shù)學(xué)方式詳盡地證明芯片設(shè)計滿足一組斷言的能力與仿真形成鮮明對比，仿真不能證明沒有bug。如果由于合法的設(shè)計方案違反了斷言而不能實現(xiàn)證明，形式化工具就會把這些作為反例提出來，并提供信息以幫助設(shè)計者調(diào)試它們。用戶提供約束條件，使形式化分析保持在合法范圍內(nèi)，確保反例是在硅片后使用中可能發(fā)生的的真實故障場景。 這一切聽起來很好，那么為什么不是每個人都在運行形式驗證呢？它每天都被數(shù)百家芯片和系統(tǒng)公司的數(shù)千人成功使用，但一些設(shè)計者和驗證工程師仍然不情愿。這可能部分是由于一些持續(xù)存在的關(guān)于形式化技術(shù)的誤區(qū)所致，使它看起來太難或太昂貴。這篇文章研究了這些誤解，并解釋了為什么它們不應(yīng)該成為擔(dān)憂的原因。

1. 您需要博士學(xué)位才能使用形式驗證。

對于第一代形式化工具來說，這個誤區(qū)可以說是正確的，這些工具是為學(xué)術(shù)目的而設(shè)計的。他們需要學(xué)習(xí)一種晦澀難懂的數(shù)學(xué)符號來指定斷言和約束。這些工具需要大量的手動指導(dǎo)，所以大多數(shù)用戶實際上是專門研究形式驗證技術(shù)的教授和博士生。 比如考慮RISC-V弱內(nèi)存模型的負載值公理。它表示，對于線程i、j和k，如果線程i執(zhí)行一個STORE操作，接著線程j執(zhí)行另一個STORE操作，然后線程k執(zhí)行LOAD操作，那么LOAD從內(nèi)存中檢索的值將是STORE更新的最新值。形式上，數(shù)學(xué)上精確的符號可以表示這一點，如圖1所示。然而，一個普通的設(shè)計或驗證工程師可能無法理解這些符號，它們對形式方法博士來說是友好的，但對其他人來說則不然。

1. RISC-V弱內(nèi)存模型的負載值公理示例。 不過近年來發(fā)生了很大變化。斷言和約束通常使用 SystemVerilog 斷言 （SVA） 指定，SVA 是設(shè)計人員和驗證工程師已經(jīng)知道和使用的 SystemVerilog 語言的子集。正式工具變得更加智能和獨立，并且更少依賴用戶專業(yè)知識。現(xiàn)在，許多都為調(diào)試反例或幫助實現(xiàn)完整證明提供了可視化和更好的提示。不需要博士學(xué)位。 還有一大類形式化應(yīng)用（App），通常不需要用戶編寫任何斷言。例如，一個時鐘域交叉（CDC）工具可以自動確定芯片中出現(xiàn)交叉的位置，以及必須證明哪些斷言以保證正確的操作。用戶只需要提供一些關(guān)于時鐘的信息，其中大部分信息在綜合和布局工具使用的約束文件中已經(jīng)存在。

2. 形式化驗證很難，因為你需要形式化專用的規(guī)范。

規(guī)格說明對于其他形式的驗證(如模擬或仿真)是不必要的，這是不正確的SoC 仿真中的固件和驅(qū)動程序堆棧已經(jīng)提供了合適的環(huán)境來將激勵驅(qū)動到芯片中進行測試;檢查程序依賴于需求來確定在運行測試時需要發(fā)生什么。如果沒有規(guī)范，驗證工程師就不能為模擬、通用驗證方法(UVM)或功能覆蓋編寫定向測試。 形式化方法對規(guī)范明顯更敏感，因為定義不明確的需求的影響更加嚴重。形式化測試（指定為斷言、約束和覆蓋）會產(chǎn)生意想不到的結(jié)果，因為形式化工具驅(qū)動激勵模式的所有可能組合。如果從需求中捕獲的約束不準(zhǔn)確，這可能會導(dǎo)致驅(qū)動虛假激勵。 在許多情況下，從規(guī)范派生形式驗證需求的行為可能會暴露bug。事實上，一個好的規(guī)范是成功的形式化驗證的一個隱藏的條件（圖2）。

2. Better specifications are a hidden bargain for formal verification

3. 您無法將形式化技術(shù)擴展到大型設(shè)計。

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

3. 這個功能漏洞，在一個有超過 10億個門的設(shè)計中，是 Axiomise 使用 CadenceJasperGold 發(fā)現(xiàn)的。 形式化應(yīng)用程序可能具有更大的容量，因為它們專注于單個任務(wù)。例如，CDC分析始終在全芯片上運行，以檢查整個時鐘網(wǎng)絡(luò)。

4. 形式驗證需要很長時間才能收斂。

在某些情況下可能會發(fā)生這種情況，尤其是當(dāng)形式測試testbench沒有自然設(shè)計為最佳性能時。但是，在大多數(shù)情況下，形式屬性收斂得非常快。 當(dāng)然，形式驗證工具的運行時間取決于設(shè)計大小、設(shè)計復(fù)雜性以及斷言和約束的數(shù)量。有多種方法可以管理形式驗證流程以保持運行時合理。隨著設(shè)計的增長以增量方式運行和在分布式模式下運行都有幫助。

5. 形式化技術(shù)只對構(gòu)建證明有用。

這個誤區(qū)也源于學(xué)術(shù)形式工具，其中的重點完全是實現(xiàn)完整的證明。雖然完整的證明為設(shè)計正確性提供了最大的信心，但形式驗證通過發(fā)現(xiàn)棘手的極端情況bug（如圖 4 中的示例）來增加價值。

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

5. 由于 ibex RISC-V 內(nèi)核中的bug而導(dǎo)致 BEQ 指令失敗，僅當(dāng)FSM 控制器處于解碼狀態(tài)時，才會由傳入的調(diào)試請求觸發(fā)。

6. 如果您以 100% 的覆蓋率運行了模擬仿真，則不需要正式的技術(shù)。

如前所述，形式驗證非常適合查找模擬或仿真遺漏的極端情況bug。此外，這個誤區(qū)夸大了覆蓋指標(biāo)的價值。它們在識別尚未執(zhí)行的設(shè)計部分方面非常有價值，在這種情況下，不可能找到所有bug。 但是，如前所述，仿真無法建立詳盡的數(shù)學(xué)證明。即使是 100% 的功能覆蓋率也不能保證沒有bug逃逸——它只是確認了所選指標(biāo)所涵蓋的設(shè)計部分的實踐。正式分析將考慮所有可能的行為，并且很可能會發(fā)現(xiàn)其他bug。

7. 形式化技術(shù)只對查找極端情況的bug有用。

許多形式化的用戶對形式化的bug搜索深信不疑，有時甚至使他們的管理層認為形式化只適合于bug搜索。形式化最大的好處之一是確定在設(shè)計中不存在與形式化證明的需求有關(guān)的bug。 例如，考慮一下RISC-V。許多以前通過仿真驗證的處理器最終都有bug逃逸，然后被形式化抓住。形式化可以毫無疑問地證明，一旦bug被修復(fù)，就不存在bug了，因為形式化的屬性證明了設(shè)計的所有可達到的狀態(tài)（圖6）。

6. 這種情況下與JasperGold 一起使用的 Axiomise formISA 應(yīng)用程序如何用于查找bug并構(gòu)建架構(gòu)正確性證明，以便對 64 位 RISC-V 處理器進行端到端驗證。 當(dāng)然，沒有什么比發(fā)現(xiàn)一個深層的、可怕的、需要翻轉(zhuǎn)芯片的bug更能證明形式化的力量了。一個驗證工程師說 "我們在模擬仿真中永遠不會發(fā)現(xiàn)這個問題"，很快就會讓人相信形式化。 但是形式驗證可以更快地發(fā)現(xiàn)各種bug，包括通常在仿真中發(fā)現(xiàn)的bug。出于這個原因，今天的芯片項目通常包含多個區(qū)塊，其中一些區(qū)塊相當(dāng)大，無需任何區(qū)塊級仿真即可正式驗證。

8. 一旦你應(yīng)用了形式化技術(shù)，你就不需要模擬及仿真了。

通常，每個形式驗證環(huán)境都使用約束來描述接口。這些約束需要在仿真中驗證，以檢查它們是否被正確建模和解釋以進行形式驗證。 此外，形式通常在流程的早期應(yīng)用，以獲得驗證shift-left的最大值。當(dāng)設(shè)計成熟并編碼更多模塊時，某些接口約束可能不再有效，因此必須在仿真中重新驗證它們。 此外，仿真和形式化對于查找與硬件-軟件交互相關(guān)的bug很有價值，這些bug僅在軟件在嵌入式或主機處理器上運行時在模擬或仿真中發(fā)生。同樣，模擬-數(shù)字接口上的bug可能僅在運行混合信號仿真時發(fā)現(xiàn)。

9. 形式化技術(shù)不提供任何覆蓋指標(biāo)，因此很難知道您是否做得足夠多。

這顯然是不正確的，因為證明提供了一種形式的覆蓋指標(biāo)。知道設(shè)計中100%的斷言永遠不會被違反，這顯然是一個強有力的聲明。 但是，所有現(xiàn)代工具現(xiàn)在都會生成與形式展示中經(jīng)過驗證的斷言相關(guān)的代碼覆蓋率視圖（圖 7）。它顯示了在形式證明期間激活并運行了哪些設(shè)計代碼行。

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

8. 正規(guī)覆蓋的六個維度。

10. 模擬仿真和形式驗證不能合并使用。

如前所述，這兩種核查辦法是相輔相成的。每個人都可以找到對方可能不會找到的某些類型的bug。沒有一個芯片項目運行一個而沒有另一個。可以將其視為假設(shè)接口假設(shè)以保證形式驗證中塊不存在bug，然后在仿真中驗證假設(shè)以關(guān)閉完整的循環(huán)。 此外，在仿真中使用形式化來建立覆蓋差距是結(jié)合這兩種技術(shù)的一個很好的例子。許多跟蹤覆蓋率結(jié)果的項目管理工具從模擬和形式驗證中收集指標(biāo)，以提供驗證進度的統(tǒng)一視圖。這有助于讓老板相信團隊正在滿足指標(biāo)驅(qū)動驗證的要求。

11. 形式化技術(shù)僅對功能驗證有用。

斷言、約束、詳盡的數(shù)學(xué)分析、證明和反例的一般概念出現(xiàn)在芯片開發(fā)領(lǐng)域，而不僅僅是檢查功能正確性。 如今，形式驗證工具被廣泛部署用于驗證架構(gòu)需求、CDC、連接、電源、死鎖、微架構(gòu)功能需求、安全性、安保和 X 傳播（圖 9）。

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

編輯：黃飛