本文由半導(dǎo)體產(chǎn)業(yè)縱橫（ID：ICVIEWS）編譯自semiengineering

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

展望人工智能

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

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

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

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

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

應(yīng)用形式驗證

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

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

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

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

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

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

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

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