芯片的驗證為何越來(lái)越難？

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

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

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

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

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

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

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

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

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

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

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

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

規避成本巨大?！溉缃褡兓俣葮O快，如果今天不采取行動(dòng)，三個(gè)月后可能會(huì )陷入更糟糕的境地，」Synopsys 形式驗證高級產(chǎn)品總監張晉（Jin Zhang）表示，「看看大語(yǔ)言模型（LLM）每周都在更新的速度，你必須升級工具、擁抱新技術(shù)，別無(wú)選擇，否則將被淘汰?！?/p>

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

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

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

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

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

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

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

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

展望人工智能

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

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

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

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

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

應用形式驗證

應用形式驗證并非簡(jiǎn)單購買(mǎi)工具并插入流程。形式驗證可通過(guò)多種方式解決特定類(lèi)型的問(wèn)題。哈迪將其分為三類(lèi)：

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

? 核心形式驗證：通過(guò)窮舉證明提高驗證質(zhì)量；

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

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

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

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

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