芯片首次流片成功率正在下降，主要原因是設計復雜度上升和成本削減的嘗試。這意味著管理層必須深入審視其驗證策略，確保工具和人員的潛力得到最大發(fā)揮。

自半導體時代伊始，通過仿真驗證設計是否具備所需功能，一直是功能驗證的核心。當設計規(guī)模較小時，這是一種簡單有效的方法。但隨著設計規(guī)模擴大，手動編寫足夠測試用例以覆蓋所有功能變得不再現(xiàn)實。測試平臺技術隨之發(fā)展，實現(xiàn)了部分流程的自動化。這在一段時間內有效，但如今卻導致驗證變得高度復雜且低效——芯片首次流片成功率的下降便是明證。

「眾所周知，隨著芯片復雜度以每 18 個月翻一番的速度增長，驗證狀態(tài)空間呈指數(shù)級膨脹，」Cadence 產品管理團隊總監(jiān)皮特·哈迪（Pete Hardee）表示，「仿真一直是主要驗證方法，但五年前驗證一個相對簡單的處理器內核需要 1013次仿真周期，而驗證 GPU 則需要 101?次?！谷缃瘢@些數(shù)字更是高出了幾個數(shù)量級。

「仿真方法缺乏智能，」Ansys 產品營銷總監(jiān)馬克·斯溫嫩（Marc Swinnen）指出，「你輸入一個向量，觀察結果；再輸入另一個向量，再觀察結果。但你并不清楚每個向量的預期作用和目標，因此基本上是在進行蒙特卡洛模擬，寄希望于覆蓋所有極端情況，或試圖主動導向這些情況?！?/p>

仿真早已力不從心?！付唐趦?，提升仿真速度是解決方案，這也推動了仿真市場的爆發(fā)式增長，」Real Intent 首席執(zhí)行官普拉卡什·納拉因（Prakash Narain）表示，「我們需要更強的計算能力。與此同時，形式驗證開始嶄露頭角——它并非與仿真并駕齊驅，而是填補了仿真在關鍵功能行為全覆蓋上的漏洞?！?/p>

目前，多種驗證技術可與仿真互補，但許多團隊難以將其成功整合到整體方法論中。原因包括：需要各類專家才能正確使用這些技術；無法展示整體進展或完成度；部分團隊仍依賴現(xiàn)有方法的經驗性成功。

靜態(tài)驗證和形式驗證工具各有優(yōu)勢，一類借助人工智能技術的新工具也開始涌現(xiàn)。例如，輔助工具可在代碼開發(fā)過程中確保其可靠性，或執(zhí)行等價性檢查。團隊需要持續(xù)評估每種工具的價值，同時了解威脅其成功的缺陷來源和類型。

功能驗證流程的全面評估，始于理解芯片可能失敗的原因?！改承┊a品的工作模式數(shù)量激增，」是德科技（Keysight）新機遇業(yè)務經理克里斯·穆思（Chris Mueth）表示，「只要其中一種模式未經驗證，產品就可能失敗。如何記錄所有模式？如何建立驗證流程以涵蓋所有模式組合？如何記錄性能要素？」

首先需要了解缺陷的本質，這將決定發(fā)現(xiàn)缺陷的最佳工具。「芯片流片后出現(xiàn)的缺陷，要么是設計中的結構性缺陷，如溢出/下溢、未知狀態(tài)（Xs）、有限狀態(tài)機（FSM）問題、死代碼、冗余代碼；要么是設計中的語義差異，如功能缺陷，」Axiomise 首席執(zhí)行官阿希什·達爾巴里（Ashish Darbari）表示，「形式驗證工具可通過應用驅動的流程，在設計啟動時自動分析并發(fā)現(xiàn)大多數(shù)結構性缺陷，這大幅節(jié)省了功能仿真的開銷?！?/p>

從理論上講，形式驗證相比仿真具有重大優(yōu)勢。「無需編寫測試用例來激勵被測設計（DUT）的所有行為并驗證不良反應，形式驗證工具會自動生成激勵，」Cadence 的哈迪表示，「除非受到約束，否則形式驗證工具會考慮所有可能的輸入組合。隨著我們走出特定應用時代，這一優(yōu)勢愈發(fā)顯著。我們將 DUT 的預期行為定義為一組屬性，要么證明這些屬性在所有情況下都成立，要么得到潛在缺陷的反例?！?/p>

沒有任何一種技術能獨立解決問題，需要找到最佳組合方式。「控制這種復雜性所需的全部智慧，蘊含在方法論和工程師身上，」Real Intent 的納拉因表示，「我們一直在為這些工具投入更強的計算能力，但這正是問題所在。另一種思路是從根本上質疑：基于布爾邏輯的傳統(tǒng)技術能否應對這種復雜性爆炸？這正是靜態(tài)驗證的用武之地，因為它們更抽象。但靜態(tài)驗證的問題在于依賴抽象，而這種抽象依賴于針對特定問題的定制化技術?！?/p>

沒有放之四海而皆準的解決方案。「歷史經驗需要融入驗證環(huán)境，」弗勞恩霍夫 IIS 自適應系統(tǒng)工程部門高級混合信號自動化團隊經理本杰明·普勞奇（Benjamin Prautsch）表示，「管理層很難理解這一點，因為需要處理許多細節(jié)。測試 IP 或驗證 IP 專家掌握的信息成為重要資產。必須將兩者結合，并且一旦現(xiàn)場出現(xiàn)錯誤或設計存在缺陷，必須將其納入設計指南或添加斷言，以改進整體測試和驗證環(huán)境。」

規(guī)避成本巨大。「如今變化速度極快，如果今天不采取行動，三個月后可能會陷入更糟糕的境地，」Synopsys 形式驗證高級產品總監(jiān)張晉（Jin Zhang）表示，「看看大語言模型（LLM）每周都在更新的速度，你必須升級工具、擁抱新技術，別無選擇，否則將被淘汰。」

失敗成本同樣高昂?！敢虼?，改變看似有效的現(xiàn)有方法需要克服巨大的恐懼心理，」納拉因表示，「這就是為什么人們仍依賴傳統(tǒng)驗證簽收方法。機會在于『左移』——盡早部署驗證技術，在缺陷修復成本低且快速的階段發(fā)現(xiàn)問題。雖然這可能不會影響當前的仿真工作，但隨著仿真中發(fā)現(xiàn)的錯誤減少，對『左移』的依賴將逐漸增加?！?/p>

小錯誤引發(fā)大問題

首先需要了解可能威脅成功的缺陷類型。在許多情況下，這些缺陷在流片前才被發(fā)現(xiàn)，看似極其復雜，但實際上很多是由深埋在邏輯中的小錯誤導致的?！竿ㄟ^運行靜態(tài)檢查（lint）和形式屬性驗證，很容易發(fā)現(xiàn)計數(shù)器中的功能缺陷，」Axiomise 的達爾巴里舉例稱，「它可能導致 SoC 中的 DDR 性能計數(shù)器溢出。在一個真實案例中，設計驗證（DV）團隊花了三周時間通過仿真調試，最終發(fā)現(xiàn)問題出在計數(shù)器上?！?/p>

形式驗證的傳統(tǒng)缺點是計算密集，這意味著它僅用于小規(guī)模（通常是控制路徑主導的）模塊和子系統(tǒng)。「具有諷刺意味的是，推動驗證需求爆炸式增長的計算能力提升，反而使形式驗證更有效，」哈迪表示，「現(xiàn)代形式驗證工具可驗證中型處理器內核，對于大型處理器，可先將其分解為子系統(tǒng)，再在頂層使用分治策略創(chuàng)建端到端屬性進行驗證。形式驗證還能在數(shù)分鐘或數(shù)小時內全面驗證復雜數(shù)學模塊。例如，32 位整數(shù)乘法器（GPU 或 AI 加速器中許多算術邏輯單元或數(shù)學協(xié)處理器的典型構建模塊）有 2??種可能的輸入組合，通過仿真覆蓋所有組合是不可行的。」

形式驗證的目標不僅限于功能驗證?！肝覀儾渴鹆艘环N新型面積分析應用，用于檢測芯片中消耗功率的冗余觸發(fā)器和門電路，」達爾巴里表示，「通過形式屬性驗證，用戶無需任何測試平臺或測試用例，即可快速分析整個 SoC。報告結果令人震驚，尤其是考慮到這些設計此前已通過仿真驗證?！?/p>

形式驗證的角色正在轉變?！高^去，人們使用屬性驗證來驗證簡單的局部斷言，」Synopsys 的張晉表示，「例如，驗證有限狀態(tài)機的狀態(tài)轉換，這些被稱為局部屬性。但近年來，重點已轉向驗證端到端屬性——為輸出編寫屬性，并從輸入推導邏輯。這些屬性更復雜，驗證難度更大，需要更多技術，但與僅在設計中散布局部屬性相比，能捕捉到更多真實設計缺陷和極端情況缺陷。」

管理層需要精確衡量驗證成本。「沒有衡量，整個論證就依賴經驗性成功，」達爾巴里表示，「這可能存在偶然性，且在很大程度上取決于技能、指導、管理和經驗等因素。如果管理層通過衡量驗證成本（包括工具、人力、測試平臺搭建、測試平臺運行和調試成本，以及未發(fā)現(xiàn)缺陷的成本）來評估投資回報率（ROI），結果將有效指示哪些方法可行、哪些不可行。形式驗證并非萬能，仿真仍需用于驗證形式驗證的假設，但兩者的正確結合能產生驚人效果?！?/p>

管理層正在傾聽?！笌啄昵?，推廣形式驗證的方法是向管理層展示其發(fā)現(xiàn)的仿真團隊遺漏的缺陷，」哈迪表示，「在尚未認識到形式驗證價值的組織中，這有時仍有必要，但這類組織已越來越少。如今，管理層開始信任由形式驗證專家?guī)ьI的小型團隊，他們能以仿真團隊驗證類似模塊所需時間的一小部分，完成高度復雜模塊的全面驗證，并提供更具結論性的驗證結果?！?/p>

展望人工智能

人工智能技術發(fā)展迅速，在會議上發(fā)表的成果可能已落后一代或兩代。「人工智能輔助工程可能會為你生成大量設計和驗證 IP，」是德科技的穆思表示，「人們需要一段時間來適應并學會信任這些結果。但在這種模式下，工作重心將轉移到流程前端——指定需求和參數(shù)，讓 AI 引擎執(zhí)行任務。設計過程將與機器學習引擎互動，呈現(xiàn)出不同的形態(tài)。前期的需求和參數(shù)設定至關重要，這能讓引擎高效完成工作?！?/p>

驗證一直關乎比較兩個模型并識別差異?！溉藗冋谔接懭绾螌⒋笳Z言模型（LLM）和其他人工智能方法融入驗證方法論，」弗勞恩霍夫的普勞奇表示，「一種方法是尋找需求文檔與驗證測試平臺之間的差異，以識別漏洞。這只是其中一個方面，我們期待看到此類工具的開發(fā)，以支持驗證工程師——這并非試圖實現(xiàn)完全自動化，而是為了輔助工程師并跟蹤所有信息?！?/p>

進展已在發(fā)生?！肝覀円言谑褂蒙墒饺斯ぶ悄埽?a class="contentlabel" href="http://www.bjwjmy.cn/news/listbylabel/label/GenAI">GenAI）創(chuàng)建 SystemVerilog 斷言，」張晉表示，「形式驗證應用的首要障礙是需要創(chuàng)建屬性，而 GenAI 能幫助降低這一門檻。這項技術已被部分客戶投入生產使用。根據設計和測試計劃，它能為你生成斷言，這大大提高了效率?！?/p>

一些公司已在使用輔助工具?！杆鼈兪乖O計的初始編碼（如人工輸入等）更加容易，」納拉因表示，「但也帶來了可變性和輸出準確性等問題。因此，驗證變得更加關鍵——確保無論采用何種方法創(chuàng)建設計，都能經過全面驗證。這為融入人工智能技術提供了機會，而這同樣關乎『左移』。如果輔助工具和人工智能技術能推動驗證『左移』的應用場景，將是重要的進步?！?/p>

隨著大語言模型生成質量的提升，所有人都將看到效率的提升。「我認為 GenAI 將改變游戲規(guī)則，使形式驗證普及化，」張晉表示，「過去，形式驗證由專業(yè)工程師負責，但如今企業(yè)逐漸意識到必須在流程早期引入形式驗證，且應由設計者主導。過去，設計者通常僅提取少量形式屬性，不會編寫大量斷言，而 GenAI 能幫助他們在設計中添加更多斷言并真正受益。這項技術必將推動形式驗證在行業(yè)中的更廣泛應用?！?/p>

應用形式驗證

應用形式驗證并非簡單購買工具并插入流程。形式驗證可通過多種方式解決特定類型的問題。哈迪將其分為三類：

? 設計者形式驗證：寄存器傳輸級（RTL）設計者可使用形式驗證實現(xiàn)「左移」，盡早交付更高質量的代碼；

? 核心形式驗證：通過窮舉證明提高驗證質量；

? SoC 集成形式驗證：分擔仿真的特定任務，發(fā)現(xiàn)極端情況缺陷。

了解模塊級、子系統(tǒng)級和全系統(tǒng)級驗證的區(qū)別至關重要，形式驗證的角色在不同層級有所不同?！冈?IP 級或子系統(tǒng)級，團隊應使用靜態(tài)方法（如 lint 和形式驗證）而非仿真，」張晉表示，「在系統(tǒng)級和 SoC 級，則應使用動態(tài)方法進行驗證，因為形式驗證在該層級難以擴展。」

盡管 SoC 級可能需要仿真，但這并不意味著排除形式驗證?！冈谟杏媱澋貞眯问津炞C的場景中，投資回報率驚人，」達爾巴里表示，「工程師和管理層都認可對形式驗證的投資，因為它能更快發(fā)現(xiàn)缺陷、避免重新流片，并幫助優(yōu)化仿真。主要問題仍是工程團隊缺乏編寫形式驗證斷言的足夠培訓。當由經驗豐富的專家使用時，形式驗證能夠對系統(tǒng)級和子系統(tǒng)級設計、處理器功能安全及安全驗證進行簽收?！?/p>

設計的變化也要求方法論隨之改變?！冈O計不再局限于特定應用，在設計時，根本無法定義這些芯片需要處理的所有工作負載，」哈迪表示，「這意味著我們必須驗證所有可能情況。在特定應用時代，理論上可以定義包含所有指定場景測試的驗證計劃，并根據該計劃衡量覆蓋率——即便如此，定義『何時完成驗證』已很困難；而如今，即使使用受限隨機方法，我們也永遠無法確定仿真測試是否足夠，因此無法判斷何時完成驗證?！?/p>

變革需要時間?！冈S多可提高設計和驗證團隊效率的技術尚未得到應用，」張晉表示，「重新調整驗證方法論、在流程中引入最新技術，需要時間，而復雜度的提升和解決問題的時間縮短加劇了這一挑戰(zhàn)。不幸的是，團隊必須評估現(xiàn)有方法論，了解當前可用技術，并探索如何利用新技術改進流程。有了 GenAI，我相信三到五年內驗證流程將發(fā)生巨大變化，自動化和生成式技術將大幅增加，我們將看到智能驅動的流程。一旦所有自動化技術成熟，芯片一次流片成功率可能會顯著提高?！?/p>