關于形式驗證的11個誤區(qū)

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

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

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

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

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

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

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

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

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

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

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

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

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

審核編輯 ：李倩