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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

展望人工智能

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

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

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

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

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

應(yīng)用形式驗(yàn)證

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

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

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

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

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

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

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

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