半導體 AI 驗證與矽晶正確性

您的團隊已經在 Verilog 上使用 LLM。它無法捕捉的那些缺陷類別，正是足以毀掉矽晶的那些。

2024 年 Wilson Research Group / Siemens EDA 功能驗證研究將首次矽晶成功率定為 14%，這是二十年追蹤以來的最低數字。2020 年時為 32%。原因並非工程怠惰，而是複雜度超越了驗證工具、規格變異速度快過測試平台，以及通用型 LLM 帶入 RTL 的一類新型故障。我們在 HDL 程式碼中看到五種幻覺模式，業界尚未為它們清楚命名。

第 1 類

語法幻覺

無法編譯的程式碼。在數秒內由 Verilator、Icarus 或合成前端捕捉。這是業界已經知道如何處理的類別。

第 2 類

語意幻覺（阻塞式與非阻塞式賦值）

以 Python 和 C 訓練的 LLM 撰寫 Verilog 時，彷彿陳述句是循序執行的。它們使用阻塞式賦值（=）此種阻塞式賦值置於時脈驅動的 always_ff 區塊內，但此處需要的是非阻塞式賦值（<=）。模擬器可能以某種掩蓋競爭的順序排程事件。合成則產生不同的邏輯。矽晶因此死鎖。

// LLM 所寫的程式碼。在某些模擬器中「正常」模擬。
always_ff @(posedge clk) begin
  stage2 = stage1;  // 阻塞式
  stage3 = stage2;  // 現在看到的是「新的」stage2，而非舊的
end
// 設計者想要的是 2 週期管線。矽晶出貨的卻是 1 週期旁路。

第 3 類

協定幻覺（AXI、AHB、TileLink、PCIe）

程式碼能編譯並通過 90% 的定向測試。然後它斷言 WVALID 早於 AWREADY，或在翻轉資料的同時持續拉高 VALID ，又或者違反埋藏在 AMBA 規格第 84 頁的某個子條款。晶片在內部測試平台上運作正常，卻在連接第三方記憶體控制器的那一刻掛起。我們以針對各協定預先驗證的 SVA 函式庫來捕捉這類問題，而非以更多模擬週期。

第 4 類

空泛幻覺（危險的那一種）

LLM 產生一個 SVA 屬性。形式化引擎證明它成立。您出貨了。但該屬性之所以平凡為真，是因為其前提條件從未觸發。這比毫無驗證更糟，因為您手上握有一張對有缺陷設計標示「已證明」的證書。任何不執行空泛性檢查的形式化流程都是作秀。Siemens 自 2017 年起就一直在警告此事，而業界至今仍在出貨不含此檢查的工具。

// LLM 生成的「核准跟隨請求」屬性
property p_grant;
  @(posedge clk) req |-> ##[1:$] gnt;
endproperty
// 如果 LLM 同時設定了一個強制 req = 0 恆成立的 assume，
// 形式化引擎便會在毫秒內「證明」這個屬性。
// 真正的仲裁器是壞的。這張證書毫無價值。

第 5 類

CDC／亞穩態盲點

LLM 看到的是訊號名稱，而非時脈域。它們將一個 2 GHz CPU 域訊號直接連接到一個 400 MHz 周邊域的正反器，跳過雙正反器同步器，而模擬無法捕捉到這一點，因為 RTL 模擬並不對亞穩態建模。Accellera 在 2024 年開啟了一項 CDC/RDC/Glitch 互通性標準，正是因為 SpyGlass、Questa CDC 與 Conformal CDC 之間的碎片化破壞了簽核。

為何這在金錢上至關重要： 70% 的重新流片是由規格變更引起，而非純粹的邏輯缺陷（2024 年 Wilson / Siemens 資料）。因此一個只捕捉邏輯缺陷的驗證流程僅處理了其中一個子集。上述第 2 類至第 5 類正是那個仍會炸掉流片的子集，因為它們繞過模擬，只在矽晶中現形。一次 5nm 重新流片代價是光罩 $10M，外加 3 至 6 個月的進度延誤。在 18 個月的產品週期上，6 個月的延誤可能抹去一半的生命週期營收。

一位無廠 DV 主管實際上正在從中抉擇的供應商版圖

您真正的替代方案並非理論上的存在。它們是三大 EDA 巨頭（您幾乎肯定已在付費）、六家資金雄厚、在 DVCon 與 DAC 上向您推銷的代理式 AI 新創、四大系統整合商，以及專精的形式化驗證顧問公司。我們沒有要與它們對打的產品。我們協助您挑選、整合並營運正確的組合。

選項	他們實際上做什麼	優勢	誠實的缺口
Cadence JasperGold、Cerebrus AI Studio、ChipStack Super Agent	黃金標準的形式化引擎。多區塊 RL 驅動的數位實作。代理式 AI 超級代理於 2026 年 2 月發表。	JasperGold 是形式化工具的標竿。深度晶圓代工整合。約佔 EDA 市場 30%。	JasperGold 歷史基準定價（$225K 基礎 + $45K/席位）對多數早期階段的 RISC-V／AI 加速器新創而言遙不可及。雲端優先的代理式功能不符合對 IP 敏感的本地部署需求。
Synopsys VC Formal、DSO.ai、AgentEngineer	L4 代理式工作流程（AgentEngineer，2026 年 3 月），宣稱可提升 2 至 5 倍生產力。基於 RL 的設計空間探索。$35B 收購 Ansys 增添了多物理場能力。	最深厚的客戶基礎。每一家大型無廠廠商都已有 VC Formal 合約。AgentEngineer 是當今最具公信力的供應商代理式技術堆疊。	有明確主張的客製化流程不是他們的生意。他們不會建議您使用開放權重模型或 SymbiYosys。小型公司只能得到範本化的關注。
Siemens EDA Questa Formal、Questa CDC、Catapult HLS	強大的 Questa 形式化與 CDC 業務。發布 Wilson 研究。最深厚的車用 ISO 26262 實績記錄。	車用認證專業。良好的 CDC／RDC 論述。工具認證套件已就緒。	代理式 AI 論述落後於 Cadence 與 Synopsys。對 RISC-V 生態系的聚焦較少。
ChipAgents 總計 $74M，2026 年 2 月	多代理 RTL 設計與驗證。在 DVCon 2026 展示了無需人工介入的多代理根本原因分析。	最強的純代理式論述。Matter Ventures（台積電支持）、Bessemer、Micron、MediaTek、Ericsson 都在其股東名單上。	雲端平台。對 IP 敏感的客戶而言，本地／氣隙隔離部署路徑並不明確。整合進既有的 Jenkins/CI 簽核流程仍須自行動手。
Normal Computing 總計 $85M 以上，2026 年 3 月	自動形式化：LLM 將工程師意圖翻譯為形式化屬性並加以證明。Samsung Catalyst 領投了上一輪募資。ARIA Scaling Compute 計畫。	在 LLM + 形式化論點上最接近的同儕。宣稱前十大半導體設計公司中有半數正在使用 Normal EDA。已交付真實矽晶（CN101）。	是產品，而非顧問服務。如果您需要針對自有專屬 RTL 語料庫的客製化微調，或整合進一個您不會徹底替換的老舊流程，那就不適合。
Axiomise 專精的形式化驗證顧問	formalISA 應用已部署於 Ibex、CVA6、cheriot-ibex、0riscy、cv32e40p、WARP-V。在 Ibex 中找出 65 個以上的缺陷，包括六個除錯單元分支缺陷。	業界最具公信力的 RISC-V 形式化驗證實績記錄。真實、可發表的缺陷發現。深厚的 ISA 專業。	團隊小。僅做形式化方法；沒有 LLM 輔助的 SVA 生成、沒有本地 LLM 論述、也未與代理式 AI 浪潮整合。
四大／大型系統整合商 Accenture、Deloitte、Wipro、HCL	龐大的 VLSI／驗證服務業務。現成的人力。	規模。離岸交付。與您採購部門既有的主服務協議（MSA）。	人力派遣式經濟模式。有明確主張的 AI 驗證架構不是他們的生意。把這個案子賣給您的合夥人，這輩子從沒寫過一條 SVA 屬性。
Veriprajna 供應商中立的客製化打造	在您的 RTL 語料庫上微調一個開放權重的程式碼 LLM，將它包覆在您已擁有的任何形式化引擎周圍，接入您的 Jenkins/CI，加上空泛性與覆蓋率指標。全部在您的硬體上。	沒有要推銷的產品。預設即為本地／氣隙隔離。RISC-V、AXI4、RISC-V 除錯以及形式化覆蓋率經濟學是我們的舒適圈。對形式化方法能與不能做什麼誠實以對。	我們不會取代您的形式化引擎。我們不會出貨我們自有的、經 ISO 26262 認證的工具。規格漂移與組織變革是顧問服務無法解決的問題；我們只能繞著它們做設計。

定價、募資與產品資訊反映截至 2026 年初的公開揭露內容。請務必直接向各供應商查證當前條款。

我們打造什麼

每一項合作都是客製化的。以下是大多數無廠客戶最終會要求的五種樣態，以及我們在每一種中所做的明確主張選擇。

1. 本地 LLM + 形式化黏合層

一個微調後的開放權重程式碼模型（Qwen 2.5 Coder、DeepSeek Coder、Llama 3.3 或 Mistral Large），執行於您自己的 H100 或 H200 叢集上，並包覆在您已擁有的任何形式化引擎周圍。沒有任何 RTL 離開您的網路。

我們所採用的工具：以 vLLM 進行推論、為每個 IP 系列配置 LoRA 適配器以共享基礎權重、在您的規格文件與過往缺陷歷史上建立本地 RAG，以及一個透過 Tcl/Python API 呼叫 JasperGold、VC Formal、Questa Formal 或 SymbiYosys 的輕量編排層。LLM 永遠不執行求解器。它撰寫屬性並詮釋反例。

為何這不是託管 API：因為您的 RTL 是皇冠寶石級的 IP，而您的資安長不會與一家去年才成立的美國或歐盟新創簽署資料處理協議。

2. RISC-V 形式化測試平台與 SVA 函式庫

針對 AXI4、AXI4-Lite、APB、AHB 與 TileLink 合規性的預建 SystemVerilog 斷言函式庫，加上 RISC-V 管線危障偵測、載入儲存單元計分板、除錯單元正確性以及 CSR 存取檢查，並針對您的客製化擴充 ISA 調校。

參考基準點： Axiomise 透過形式化在 Ibex 核心中找出 65 個以上的缺陷，包括六個模擬遺漏的除錯單元分支缺陷。形式化方法在 RISC-V 上是有效的。瓶頸在於能撰寫斷言的工程師稀缺。我們建好函式庫，讓您的團隊無須親力親為。

誠實的但書：一套精選的斷言函式庫比 LLM 從零生成更可靠，但仍無法證明每一類缺陷都不存在。我們會搭配 COI（影響錐）與基於變異的覆蓋率分析。

3. 供應商中立的工具選型與試行

您的 DV 主管正被 ChipAgents、Normal Computing、MooresLabAI、Silimate、Bronco AI，以及 Cadence 與 Synopsys 內建的代理式產品輪番推銷。六項產品、六種不同的宣稱、在您實際 RTL 上零個獨立基準測試。

我們所做的：在 NDA 之下，於您的程式碼庫上進行一場結構化的四週競測。相同的測試套件、相同的缺陷預算、相同的覆蓋率目標。一份誠實的報告，比較缺陷發現率、誤報率、設置工作量、整合債務，以及各供應商實際提供給您的定價條款。

為何買家在此事上信任我們：我們不轉售這些產品中的任何一項。如果正確答案是「繼續用 JasperGold 並加上一層輕量 LLM 輔助」，我們就會這麼說。

4. CI 中的代理式 RTL 審查

每一個觸及 RTL 的拉取請求，都會在人工檢視之前先經過一條多代理流程審查。一個代理進行 lint 並檢查風格。第二個代理執行從變更檔案衍生的形式化屬性集。第三個代理檢查 CDC 與 RDC 路徑。第四個代理生成一份人類可讀的摘要，並在屬性失敗處附上反例軌跡。

明確主張的選擇：我們在您既有的 CI（Jenkins、GitLab、BuildKite，無論哪一種）內執行這些代理。我們不會用新平台取代您的 CI。這些代理是流程所呼叫的服務。當您解雇我們時，您仍保有這條流程。

我們拒絕打造的東西：一個未經人工審查就自動合併 RTL 的代理。矽晶不是微服務。您無法對一顆晶片發布熱修補。

5. 小晶片／3D-IC 熱感知佈局規劃（在適當時，用於 RL 佈局）

這是我們認為強化學習用於佈局真正值得部署的唯一場合。既有業者（Cadence Cerebrus、Synopsys DSO.ai）是為單體 2D SoC 而調校的。小晶片／UCIe 浪潮開啟了一類新的佈局規劃問題（小晶片間的線長、熱堆疊、凸塊間距限制），而公開工具在此尚不成熟。

我們所打造的：在 OpenROAD 之上，為小晶片分割階段打造一個混合式模擬退火 + RL 佈局規劃器，並以熱約束作為一等的獎勵項。在我們動您的設計之前，會先對已發表的 ISPD／ICCAD 結果進行基準測試。

我們直接正視 AlphaChip 爭議。 Igor Markov 於 2023 年的批評顯示，Google Circuit Training 耗時 32 小時，而一次調校過的模擬退火執行耗時 12.5 小時，一個 Cadence 商用工具則耗時 0.05 小時。我們不會把 RL 推銷為在充分理解的問題上取代調校過的 SA 的方案。我們將它用在設計空間真正全新、人類直覺沒有先驗可資借鑑的地方。

我們如何工作

每一項合作都從在您一小塊 RTL 上進行為期兩週的範圍界定階段開始，然後才碰任何更大的東西。我們寧願在第二週就退出，也不願在不合適的配對上燒掉您的進度。一次完整打造的典型節奏如下。

範圍界定 · 2 週

閱讀您的規格、走過您既有的流程、挑選一個具代表性的區塊（通常是匯流排介面、仲裁器，或單一 RISC-V 管線階段），並在其上執行我們的基準形式化測試平台。產出：一份書面報告，列出我們看到的缺陷類別、我們將會建構的斷言，以及整項合作的成本估算。如果答案是「您應該繼續做您現在在做的事」，我們就會這麼說，並只收取這兩週的費用。

基礎建設 · 4 至 6 週

在您的叢集上部署本地 LLM 技術堆疊。基礎模型以 LoRA 適配器在您的 RTL 語料庫上微調。RAG 在您的規格與過往缺陷資料庫上建立索引。接入您的形式化引擎、您的 Jenkins/CI 以及您的問題追蹤系統。從第一天起，我們就以證明覆蓋率、空泛性與有界深度等指標來檢測一切。

斷言函式庫與啟用 · 6 至 10 週

我們為您前 3 至 5 個 IP 區塊移植或撰寫 SVA 函式庫（協定合規、管線、CDC）。我們執行形式化回歸。我們與您的 DV 主管一同分類處理發現的問題。在這個階段結束時，您的團隊擁有每一條斷言。沒有黑盒子。

交接 · 2 至 4 週

您的工程師在我們的旁觀下，將這套流程跑滿兩個完整的衝刺。我們將我們所做的每一個明確主張選擇記錄成文，讓下一個人能理解原因。我們退出。如您偏好，可選擇性簽訂回歸調校的顧問留任合約。

時程是誠實的範圍，不是銷售數字。一個 2 階段的管線區塊可在三週內完成。一個具有客製化擴充的完整 RISC-V 核心則更接近五個月。我們會在一開始就說清楚，而且我們不會為了趕上一個人為設定的日期而硬擠。

重新流片風險敞口計算器

三項輸入。告訴您光罩成本敞口、預期的進度延誤，以及在您所處製程節點上一次矽晶重新流片的營收風險。這些數字來自 2024 年 Wilson Research Group / Siemens 研究、近期 SemiAnalysis 光罩成本資料，以及典型的 18 個月產品週期。在您下一次流片就緒度審查中使用它。結果會推薦您在不雇用我們的情況下可採取的具體行動。

製程節點

本產品的年度營收目標（$M）

專責的形式化驗證工程師

DV 主管與 CTO 實際會問的問題

這些是來自無廠與 RISC-V 客戶的真實問題。每一個答案都增添了上述各節未涵蓋的深度。

有任何 RTL 或 GDSII 會離開我們的網路嗎？

不會。我們交付的每一種部署架構都在您的硬體上執行。微調後的模型權重存放於您的叢集。帶有您 IP 專屬調校的 LoRA 適配器存放於您的防火牆之後。vLLM 推論在您的 GPU 上執行。RAG 從您自有的文件儲存庫索引您的規格文件。我們的工程師透過您標準的 VPN 與 SSO（含稽核日誌記錄）存取該環境。對於國防、航太與 SCIF 客戶，我們以簽署過的離線更新套件交付整個技術堆疊，且不要求該環境有任何對外連線。唯一的例外是初始的基礎模型下載，這是在一個未分類系統上完成後再轉移進去的。如果您需要比這更嚴格的氣隙隔離，我們也做過。

我們如何得知 LLM 生成的斷言並非空泛的？

空泛性是我們最擔心的故障模式，也正是我們交付的每一個形式化流程都執行三層檢查的原因。第一，形式化引擎的原生空泛性檢查（JasperGold 與 VC Formal 都有；SymbiYosys 需要我們提供的包覆器）。第二，一項基於變異的健全性檢查，我們在設計中注入一個缺陷並確認斷言會觸發。一條通過空泛性檢查卻無法捕捉注入缺陷的斷言，對您毫無助益。第三，一份 COI（影響錐）報告，精確顯示每條屬性觸及哪些訊號。如果一條屬性的 COI 為空，它就是死碼，我們會刪除它。這些正是 Siemens 自 2017 年起就在《Verification Horizons》中持續發表的相同指標，而我們將它們視為基本門檻。

我們是瞄準 ISO 26262 ASIL D 的車用客戶。我們能用這套流程做簽核嗎？

不能直接用於簽核，我們也不會假裝可以。ISO 26262 要求工具認證（依您使用工具的方式而定為 TCL2 或 TCL3），並附帶一份文件化的認證套件。Synopsys、Cadence 與 Siemens 都出貨已認證的流程；一個客製化的 LLM 輔助工具不在那份清單上。我們為車用客戶建構的，是一個與已認證工具並行執行、而非取而代之的 AI 輔助層。已認證的工具仍然產出簽核證據。我們的層加速斷言撰寫、審查屬性是否空泛，並標記 CDC 路徑供人工檢查。您已簽核工具上的認證鏈不受觸動。ASIL D 客戶還應規劃在輔助層與已認證驗證之間進行一次文件化的獨立性審查，我們會協助您建構此架構。

我們為何不乾脆改買 ChipAgents 或 Normal Computing？

您或許可以。兩者都資金雄厚、技術上具公信力，並擁有真實客戶。團隊在評估它們之後仍來找我們，原因通常是三件事之一。第一，雲端部署模型未能通過他們的資安審查（常見）。第二，他們需要針對一個產品團隊無法優先處理的專屬客製化擴充 ISA 進行微調。第三，他們想要客製化整合進一個既有的 Jenkins／回歸／簽核流程，而產品團隊若無一筆六位數的專業服務合約便無法支援。如果以上皆不適用於您，那麼產品很可能就是正確答案，我們也會這麼說。如果它們確實適用，我們便打造這個客製化層，並留給您一套您自己的工程師能夠維護的系統。在試行階段，我們建議將這三個選項放在同一份 RTL 上跑四週。相較於一個錯誤的賭注，這場競測很便宜。

您對 RL 佈局的 AlphaChip／Markov 爭議立場為何？

我們認為 Igor Markov 的批評在那些具體數字上技術上是正確的。Google Circuit Training 的 32 小時，相對於調校過的模擬退火的 12.5 小時，以及 Cadence 商用工具的 0.05 小時，這並不是 RL 在主流 SoC 上贏得佈局的故事。這並不意味著 RL 對矽晶毫無用處，而是意味著 2020 年的論述框架是錯的。我們認為 RL 佈局如今真正值得其運算成本的地方，是設計空間真正全新的小晶片與 3D-IC 佈局規劃、既有工具薄弱的熱感知類比佈局，以及在密切相關的 RISC-V IP 系列間進行遷移學習——在您前一代上訓練過的代理能給您一個暖啟動。我們不會在一顆 5nm 的單體數位 SoC 上拿 RL 佈局去對打 DSO.ai 或 Cerebrus。那是一場我們會輸、而由您買單的仗。

70% 的重新流片源自規格變更而非邏輯缺陷，您如何處理這個事實？

老實說，這是驗證中最棘手的問題，沒有任何 AI 工具能乾淨俐落地解決它。我們所做的，是將規格視為驗證流程的一等輸入。LLM 監看規格儲存庫（Confluence、Google Docs、Git，無論您用哪一種），並標記其底層假設已變更的屬性。當審查者將規格的某一節標記為已修訂時，相依的屬性會自動重新執行，差異報告會在下一次回歸結束之前送到 DV 主管手上。這並不能消除規格漂移。沒有任何方法能消除。它讓漂移在數小時內現形，而不是在矽晶中現形。我們在此事上看到最大的單一收穫，是在「規格兩個衝刺前變了、卻沒人重跑受影響的形式化屬性」這件事傳播穿越整個階層之前就抓住它。

我們已經擁有 JasperGold。我們應該替換它嗎？

不應該。JasperGold 是最優秀的商用形式化引擎，而當客戶已擁有它時，我們會使用它。我們所增添的，是其上的 LLM 輔助層（斷言生成、反例詮釋、空泛性健全性檢查），以及一個多數團隊還沒花時間乾淨建好的 CI 整合。您既有 JasperGold 投資的回報只會上升，不會下降。如果您不擁有 JasperGold 且無法為基礎 + 每席位的定價找到理由，我們通常會建議採用 Questa Formal（每席位較便宜）做大量回歸、搭配 SymbiYosys（開源）做自動屬性除錯的混合方案。我們曾將這套技術堆疊交付給購買 JasperGold 並非選項的 RISC-V IP 新創。

這套方案能為多小的團隊運作？

我們曾為一家 6 人的 RISC-V IP 新創建構有用的流程，也曾為一家 400 人的 AI 加速器公司建構。下限在於至少有一位工程師能自在地閱讀 SVA 並詮釋形式化反例軌跡。如果團隊中沒有人能讀懂一條 SVA 屬性，那麼沒有任何 LLM 輔助流程能彌補這道缺口，您應該在與我們或任何人合作之前，先聘用或外包這項技能。在那道基線之上，合作規模隨範圍內 RTL 的多寡而擴展。單一匯流排介面區塊是六週的工作。一個具有客製化擴充與互連結構的完整 RISC-V 核心則是四到六個月。

您的首次矽晶成功率只有 14%。而 LLM 生成 RTL 的勝算更糟。