AI 寫出的那個 1,000 萬美元錯誤——以及我為何創辦一家公司來根除它
我清楚記得自己決定創辦 Veriprajna 的那一刻。
那不是一閃而過的靈感，而是一通電話。那種前五秒沒有人開口的電話，因為電話另一端的人，正努力想著該怎麼把要說的話說出口。一支設計團隊——都是我敬重的人，都是真正擅長本職工作的人——剛從晶圓代工廠拿回一款客製化 RISC-V 加速器的首批矽晶。那顆晶片死了。不是「需要一個變通方案」的那種死。也不是「我們可以用韌體打補丁」的那種死。是徹底報廢。 在一種特定而罕見的組合下——熱節流與高頻寬記憶體流量恰好同時發生——仲裁模組進入了未定義狀態，整個系統陷入死鎖。
根本原因是一個競爭條件。RTL 中，阻塞式賦值與非阻塞式賦值之間一個單一而細微的不匹配——那種模擬起來完美無瑕、lint 檢查連一聲都不吭、你丟什麼回歸測試給它都能通過，然後卻在沒有第二次機會的晶片裡背叛你的東西。
那顆 5nm 晶片的光罩組成本大約是 1,000 萬美元。全沒了。但真正的損害並不是光罩本身，而是為了診斷、修復、重新驗證與重新製造所需要的那六個月。在產品世代大約只持續 18 個月的 AI 加速器市場中，六個月的延誤可能侵蝕掉一項產品整個生命週期總毛利的 50%。對一家營收目標為 1 億美元的公司來說，那個競爭條件的代價並不是 1,000 萬美元，而是 5,000 萬美元。
而真正讓我夜不能寐的是這一點：導致這一切的程式碼，是由一個 LLM 生成的。
無人質疑的淘金熱
此刻，半導體產業正處在一場淘金熱的中央。每一個人——我是說每一個人——都在爭相把大型語言模型接進電子設計自動化（EDA）的工作流程裡。這套說辭令人無法抗拒：把過去需要數年的設計週期壓縮到數個月。讓晶片設計走向普及化。讓 AI 去處理繁瑣的暫存器傳輸層級（RTL）編碼，好讓工程師能專注於架構。
我理解這種吸引力，我自己也曾感受過。當我第一次看到一個 LLM 從自然語言提示生成出語法正確的 Verilog 模組時，我心想：這將改變一切。
但接著，我開始更仔細地審視：當你寫的是硬體而非軟體時，「語法正確」究竟意味著什麼。然後我意識到，這個產業是把地基蓋在沙子上。
此刻湧入市場的那些工具，就是我所謂的「外殼」（Wrappers）。它們拿一個通用型 LLM——GPT-4、Claude、Llama——用一個聊天介面加上一些帶 Verilog 風味的系統提示把它包起來，然後當作「晶片設計副駕駛」來賣。其中有些確實是令人印象深刻的展示。程式碼看起來很乾淨。它能編譯。它甚至能模擬。
但這些工具的本質是：披著硬體外皮的隨機詞元預測器。 它們不懂電路拓撲，不懂時序收斂，也不懂亞穩態。它們只是根據訓練資料中的統計模式，預測下一個最可能出現的詞元。
當一個 LLM 在軟體中產生幻覺時，你得到的是一個可以透過無線更新來修補的執行期錯誤。當一個 LLM 在硬體中產生幻覺時，你得到的是一個價值 1,000 萬美元的紙鎮。
正是這種不對稱，構成了 Veriprajna 存在的全部理由。
AI 為什麼會寫出糟糕的硬體程式碼？
這是我最常被問到的問題，通常來自那些看過 LLM 寫出功能完美的 Python、卻無法理解 Verilog 為何不同的軟體工程師。答案比「硬體更難」要深得多。它是 LLM 的思考方式與硬體運作方式之間一種根本性的不匹配。
LLM 的訓練資料絕大多數是軟體——Python、Java、C++、JavaScript。這些都是命令式、循序執行的語言。A 行先執行，然後才是 B 行。系統的狀態由運算的先後順序決定。LLM 對這套範式的內化如此之深，這基本上已成了它們的母語。
Verilog 和 VHDL 則是宣告式且並行的。 在一個硬體模組中，每一個 always 區塊、每一條 assign 陳述式、每一次模組實例化，都是同時且持續地執行的。 原始碼中各行的先後順序，往往與晶片中實際的執行順序毫無關係。
在我們早期的一次實驗中，我親眼看到了這一幕。我們要求三個不同的前沿 LLM 實作一個簡單的三級管線暫存器。三者都使用了阻塞式賦值（=）而不是非阻塞式賦值（<=）。如果你把它當成 C 程式碼瞇著眼看，這段程式碼看起來完全合理。但在硬體中，在時脈區塊裡使用阻塞式賦值意味著 stage2 會被更新為 stage1 的值，而且是立即發生，接著 stage3 取得 新的 值，來自 stage2 ——實際上把一個原本兩週期的管線壓縮成了一個週期。
我的一位工程師 Priya 盯著輸出看了一分鐘，說：「它是在寫 C，只是把分號放錯了地方。」她說得完全正確。這個 LLM 帶著一種循序偏誤——它把 Verilog 當成一種程式語言來對待，但 Verilog 其實是一種描述語言。這個區別在語法上很細微，在物理層面上卻是災難性的。
而且情況還會更糟。硬體設計仰賴嚴格的介面協定——AXI、AHB、PCIe、TileLink——伴隨著複雜的時序規則。「Ready 不得等待 Valid。」「Grant 必須在 5 個週期內被拉起。」LLM 生成的程式碼有 90% 的時候能遵守這些規則，這聽起來很棒，直到你意識到它出錯的那 10%，正是會讓晶片喪命的邊角案例。一個 AXI 主控端若讓 WVALID 早於 AWREADY 就被拉起，這在某條特定子條款上構成違規，卻不會拋出任何語法錯誤。它能編譯、能模擬，然後在晶片中連接到一個合規的記憶體控制器時就會當機卡死。
訓練資料的問題讓一切雪上加霜。可供訓練的高品質、生產級 Verilog，其數量要小上好幾個數量級，遠不及 Python 或 JavaScript。GitHub 上大量的開源 Verilog 都是學生專案、被棄置的原型、玩具級的實作，這些東西根本通不過流片審查。當你用平庸的資料來訓練，得到的就是平庸的輸出——看起來很專業，骨子裡卻帶著業餘錯誤的 DNA。
困擾每一位晶片設計師的法則
半導體設計中有一條經驗法則，叫做「十倍法則」（Rule of Ten），一旦你理解了它，就會明白我為什麼如此執著於及早抓出錯誤。
修復一個缺陷的成本會增加10 倍，而且是在設計生命週期的每一個後續階段都增加這麼多。一個在 RTL 設計階段被抓到的錯誤，修復成本大約是 100 美元——某個人改一下檔案、重跑一次檢查。同樣的錯誤若在區塊驗證階段才被抓到，成本是 1,000 美元。到了系統驗證，是 1 萬美元。如果它逃到了矽後驗證——也就是你在實驗室裡對實際晶片除錯的時候——一次重新流片（respin）就要花你 1,000 萬美元甚至更多。而如果它一路溜到了客戶手上呢？那就是 1 億美元的等級了。召回、訴訟、品牌崩毀。去問問 Intel 那個 Pentium FDIV 錯誤吧。
那些「外殼」型 AI 工具幾乎只在 RTL 設計階段運作。它們幫工程師更快地寫程式碼。但由於它們除了「能不能編譯」之外沒有任何驗證能力，它們注入的錯誤會一路順利通過區塊驗證與系統驗證，最後在晶片中引爆。
殘酷的諷刺就在這裡：這些工具在提高程式碼生成速度的同時，卻沒有相應地提高驗證的嚴謹度，於是加速了高成本缺陷被注入整條流程的過程。 你不只是「快速行動、打破陳規」而已，你是在快速行動的同時，把錯誤烘焙進了價值 1,000 萬美元的光罩組。
產業數據印證了這一點。只有 32% 的設計能達成首次流片成功。剩下的 68% 至少需要一次重新流片，而首要原因就是邏輯與功能上的瑕疵——正是 LLM 在對協定產生幻覺或誤解並行性時所生成的那類錯誤。
在我們早期募資時，我曾向一位投資人解釋這一切。他耐心聽完，然後說：「你們難道不能就用 GPT-4，把提示寫好一點嗎？」
我調出了那個管線暫存器的例子。我讓他看那個阻塞式賦值的錯誤。我讓他看到它通過了 lint 檢查、通過了模擬、通過了外殼工具所提供的每一項自動化檢查。然後我讓他看到它在晶片中會做出什麼事。
他沒有再問更好的提示這件事。
如果你能「證明」程式碼正確，而不只是「測試」它，會怎樣？
故事就在這裡出現轉折。因為 LLM 幻覺問題的解答，不是更好的提示、更大的模型，或更多的訓練資料。它是一種在本質上截然不同的驗證方法。
傳統的驗證仰賴模擬——你撰寫測試平台（testbench），跑上數百萬個週期，檢查設計是否如你預期地運作。這就像是繞著街區開上一千圈來測試一輛車的煞車。如果煞車沒失效，你就假定它是安全的。但如果它只有在下雨、你的時速剛好是 62 英里、而且收音機調到某個特定頻率時才會失效呢？模擬只能驗證它明確測試過的情境。其餘的一切，都只能靠祈禱。
形式化驗證完全不執行這個設計。它把整個設計轉換成一道數學公式，再運用「可滿足性模理論」（SMT）求解器——例如微軟的 Z3——來窮盡地證明某個性質在每一種可能的輸入組合與內部狀態下都成立。 每一種，無一例外。不是取樣，不是統計上的近似，而是一個數學證明。
模擬問的是：「在我測試過的情況裡，這行得通嗎？」形式化驗證問的是：「有沒有任何一種可能的情況會讓它失效？」這兩者的差別，就是希望與證明之間的差別。
當求解器回傳「UNSAT」——不可滿足——時，代表不存在任何反例。這個性質在數學上得到了保證。當它回傳「SAT」時，它會交給你一組具體的輸入序列，能夠擊垮你的設計，而且精確到確切的時脈週期。
形式化驗證已經存在了數十年。它之所以未能席捲整個產業，是因為撰寫那些形式化性質——SystemVerilog 斷言，也就是 SVA——是出了名的困難。它需要一套大多數設計團隊並不具備的專業技能。這些斷言就是硬體的「契約」：「若 request 拉高，grant 必須在 N 個週期內跟上。」「從位址 X 讀取的資料，必須與最後一次寫入位址 X 的資料相符。」「管線絕不能死鎖。」要正確地寫出這些斷言是一門藝術，而懂這門藝術的人手根本不夠用。
而這正是 AI 派上用場的地方——不是用來寫硬體程式碼，而是用來寫那份證明。
「形式化三明治」——我們實際上是怎麼打造它的
我花了好幾個月，跟團隊爭論到底該用什麼樣的架構。那場辯論很激烈，如今回想起來，也很有釐清作用。一派人想把一個 LLM 微調到讓它預設就生成正確的 Verilog。另一派——也就是我最終站到的那一邊——則主張「靠訓練達成正確性」是一種幻想。你無法把幻覺訓練掉，你只能把它抓出來。
我們最終落腳在一個我們稱之為「形式化三明治」的東西——一種神經符號式（neuro-symbolic）的架構，其中 LLM 是創意引擎，而形式化驗證求解器則是毫不留情的批判者。兩者單獨都無法成事。攜手合作，它們能做到任何一方獨自都做不到的事。
它在實務中的運作方式如下。設計者提供一份規格——「設計一座 APB 轉 AXI 的橋接器」，甚至只是一張時序圖的截圖。我們的規格分析器（Spec Analyzer）代理會把它拆解成功能需求。接著就是關鍵的創新之處：LLM 不只生成程式碼，而是要生成兩份產物，而且是同時生成。
產物 A 是 RTL 實作——也就是 Verilog 程式碼本身。 產物 B 則是形式化規格——一組源自相同需求的 SVA 性質。如果規格說「Grant 必須跟在 Request 之後」，LLM 會生成那個狀態機，以及能證明該狀態機確實如其所宣稱般運作的那個斷言。
接著我們就放出求解器。它拿起產物 A，試著用產物 B 去攻破它。首先是一次空洞性檢查（vacuity check）——確保那些斷言不是恆真的廢話（一種「偷懶」的生成，其觸發條件永遠不會被引發）。然後是有界模型檢查，深入探索龐大的狀態空間——深達 50、100 個週期——搜捕死鎖、競爭條件與協定違規。
如果求解器找到一個錯誤，它不會只是把它標記出來而已。它會產生一份反例軌跡（counter-example trace）——一段精確的波形，準確顯示出這個錯誤是如何顯現的。而閉環就在這裡完成：我們把那段軌跡當作提示，回饋給 LLM。「你的設計失敗了。這是軌跡：週期 1，Reset 解除。週期 2，Request 拉高。週期 10，Grant 仍然是低電位。grant 從未到達。修好這個狀態機。」
LLM 分析這段軌跡，找出缺失的狀態轉換，重寫程式碼。求解器再次檢查。這個循環會自動重複，直到設計被證明為正確為止。
關於這套架構，我在我們研究的互動版本裡有過深入得多的著墨，但核心洞見很簡單：我們用 AI 來撰寫證明，再用數學來檢查 AI。 兩者互不信任。兩者也都讓對方變得更好。
讓我成為信徒的那些錯誤
我之所以真正成為這套方法的信徒，不是透過理論，而是透過那些我們抓到、卻是其他任何手段都不可能發現的具體錯誤。
開源 RISC-V 社群確實打造出了一些極為出色的處理器核心——Ibex（用於 Google 的 OpenTitan 安全晶片）、蘇黎世聯邦理工學院（ETH Zurich）的 PULP 平台。這些都是經過嚴密審視、背後有真正工程人才的設計。然而它們依舊藏著只有形式化驗證才找得到的錯誤。
形式化驗證顧問公司 Axiomise 在 Ibex 核心中找到一個錯誤：當一個除錯請求在分支指令執行期間的某個特定週期抵達時，可能導致核心死鎖或執行錯誤的指令。想想看——一個攸關安全的核心，經過數十位工程師審查，卻被一個形式化工具找出了模擬完全遺漏的錯誤。
在 PULP 平台中，發現了一個錯誤：AXI 互連在一種特定的「忙碌」模式下，可能讓某個匯流排主控端無限期地被餓死，而這種模式源自 AWVALID 與 AWREADY 之間的互動。這是一種典型的活性（liveness）失效——系統不會當機，它只是停止推進。你絕不會為那種特定的互動模式去寫一個定向測試。可能的模式實在太多，根本無法一一列舉。
當我們把 Veriprajna 對準一個 RISC-V 載入儲存單元（Load-Store Unit）時，它會自動生成針對介面合規性的斷言（「若 valid 被拉起，它必須保持高電位直到 ready」）、資料完整性的斷言（「從位址 X 讀取的資料，須與最後一次寫入位址 X 的資料相符」），以及前向推進的斷言（「該單元最終必須回傳一個回應」）。這些並不是事後才拴到程式碼上的補充。它們是與程式碼一起、從同一份規格生成的，並且在任何一行 RTL 離開我們系統之前就被強制執行。
若想完整了解我們方法論與形式化驗證引擎的技術細節，請參閱我們的詳細研究論文。
「但形式化驗證無法規模化」
人們總在這一點上提出反駁，我也理解原因。形式化驗證素有「運算量會爆炸」的名聲——現代 SoC 的狀態空間大到天文數字，而天真的形式化方法一碰到比玩具設計更大的東西就會噎住。
我們在這件事上投入了大量心力。我們的系統運用自動化的抽象技術，讓形式化方法在規模化的情況下仍然可解。黑箱化（Black-boxing） 讓我們能夠驗證黏合邏輯，同時把 RAM 或複雜 ALU 這類大型子區塊，當成具有既定介面的抽象實體來看待。切點（Cut-points） 則切斷 valid/ready 握手路徑，讓我們能夠獨立於資料處理之外去驗證流量控制。對稱性化簡（Symmetry reduction） 讓我們能為一個多埠路由器的其中一個通道證明某個性質，再以數學方式歸納推及全部 N 個通道。
這問題被徹底解決了嗎？沒有。類比物理永遠會帶來形式化方法碰不到的挑戰。但那些邏輯錯誤——競爭條件、死鎖、協定違規——在生成的程式碼中會變得在數學上不可能發生。而正是這些錯誤，導致了重新流片。
我聽到的另一個反對意見是關於速度。「跑一個形式化求解器，難道不會拖慢設計流程嗎？」是的，它會增加運算成本。但我每一天都願意拿運算時間去換取時程上的確定性。一個形式化求解器多跑一個小時，比起一次為期六個月的重新流片，便宜得無可比擬。
關於「AI 設計晶片」的一個令人不安的真相
業界有一種說法正逐漸流行——說 AI 很快就能端到端地設計晶片，說我們正從電腦輔助設計（Computer-Aided Design）邁向電腦自動化設計（Computer-Automated Design）。我認為這種說法在方向上是對的，但危險地並不完整。
我們正朝著代理式（agentic）工作流程邁進，讓自主的 AI 代理彼此協作——一個負責高階分割的架構師代理、一個負責實作的 RTL 編碼員、一個負責撰寫測試平台與斷言的驗證工程師，以及一個負責在功耗、效能與面積約束下協調整個流程的管理者。我們運用檢索增強生成（Retrieval-Augmented Generation，RAG），不只用於程式碼，也用於知識——擷取特定的協定規則、製程設計套件（PDK）約束，以及內部編碼規範，好讓 LLM 生成合規的程式碼而不產生幻覺。
但這一切都行不通——一點都不行——只要少了一根形式化驗證的骨幹便是如此。AI 變得越自主，「每一項輸出在流向下游之前都必須經過數學驗證」這件事就越關鍵。一個能更快生成程式碼的 AI 代理，唯有在那份程式碼正確時才有價值。而一個能更快生成程式碼、並且還能證明它正確的 AI 代理呢？那，才是未來。
半導體產業的問題，不在於 AI 寫硬體程式碼寫得太慢。問題在於，AI 寫那些暗藏細微錯誤的硬體程式碼，寫得太快了。
我們不是一個副駕駛（copilot）。我們不是一個聊天機器人。我們是一座形式化驗證的鑄造廠，只是碰巧用生成式 AI 當作它的前端。這個區別很重要，因為它決定了你在為什麼而最佳化。副駕駛為速度最佳化。我們為正確性最佳化。在一個單一漏網錯誤就要付出 1,000 萬美元光罩成本、5,000 萬美元營收損失的世界裡，我很清楚自己會選哪一種最佳化。
這個選擇，其實早已做出
半導體產業再也承擔不起那種「生成後祈禱」的做法。十倍法則不是一個建議——它是物理與經濟合謀，要懲罰任何出貨未經驗證晶片的人。在 5nm 及以下的製程、光罩組成本逼近 2,000 萬美元的情況下，容錯的餘地已經崩塌至零。
每一週，我都會跟一些設計團隊交談，他們既為 LLM 能為自己生產力帶來的好處而興奮，又為 LLM 可能對自己流片時程造成的影響而恐懼。他們同時感受到這兩種情緒，是完全正確的。這項技術確實帶來變革。但在沒有安全網的情況下，它也確實危險。
Veriprajna 就是那張安全網。我們給你的是 AI 的速度，加上數學的確定性。不是「大概正確」，也不是「通過了回歸測試」。而是經過證明的正確——橫跨每一種可能的輸入、每一種可能的狀態、每一個模擬永遠不會想到要去測試的可能邊角案例。
今天每一位晶片設計師所面對的選擇，並不是要不要使用 AI。那艘船早已駛離。真正的選擇是：要使用一個能證明自己成果的 AI，還是一個只會祈求最好結果的 AI。
我很清楚，自己會拿 1,000 萬美元押在哪一個上。
