本文由半導體產業縱橫（ID：ICVIEWS）編譯自semiengineering

過去，仿真曾是驗證的唯一工具，但如今選擇已變得多樣。平衡成本與收益并非易事。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

小錯誤引發大問題

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

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

形式驗證的目標不僅限于功能驗證。“我們部署了一種新型面積分析應用，用于檢測芯片中消耗功率的冗余觸發器和門電路，”達爾巴里表示，“通過形式屬性驗證，用戶無需任何測試平臺或測試用例，即可快速分析整個SoC。報告結果令人震驚，尤其是考慮到這些設計此前已通過仿真驗證。”

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

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

管理層正在傾聽。“幾年前，推廣形式驗證的方法是向管理層展示其發現的仿真團隊遺漏的缺陷，”哈迪表示，“在尚未認識到形式驗證價值的組織中，這有時仍有必要，但這類組織已越來越少。如今，管理層開始信任由形式驗證專家帶領的小型團隊，他們能以仿真團隊驗證類似模塊所需時間的一小部分，完成高度復雜模塊的全面驗證，并提供更具結論性的驗證結果。”

展望人工智能

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

驗證一直關乎比較兩個模型并識別差異。“人們正在探討如何將大語言模型（LLM）和其他人工智能方法融入驗證方法論，”弗勞恩霍夫的普勞奇表示，“一種方法是尋找需求文檔與驗證測試平臺之間的差異，以識別漏洞。這只是其中一個方面，我們期待看到此類工具的開發，以支持驗證工程師——這并非試圖實現完全自動化，而是為了輔助工程師并跟蹤所有信息。”

進展已在發生。“我們已在使用生成式人工智能（GenAI）創建SystemVerilog斷言，”張晉表示，“形式驗證應用的首要障礙是需要創建屬性，而GenAI能幫助降低這一門檻。這項技術已被部分客戶投入生產使用。根據設計和測試計劃，它能為你生成斷言，這大大提高了效率。”

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

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

應用形式驗證

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

設計者形式驗證：寄存器傳輸級（RTL）設計者可使用形式驗證實現“左移”，盡早交付更高質量的代碼；

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

SoC集成形式驗證：分擔仿真的特定任務，發現極端情況缺陷。

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

盡管SoC級可能需要仿真，但這并不意味著排除形式驗證。“在有計劃地應用形式驗證的場景中，投資回報率驚人，”達爾巴里表示，“工程師和管理層都認可對形式驗證的投資，因為它能更快發現缺陷、避免重新流片，并幫助優化仿真。主要問題仍是工程團隊缺乏編寫形式驗證斷言的足夠培訓。當由經驗豐富的專家使用時，形式驗證能夠對系統級和子系統級設計、處理器功能安全及安全驗證進行簽收。”

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

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