形式驗證 (Formal Verification)

3 秒看懂

一句話： 形式驗證是用數學證明（而非模擬/測試）來保證晶片設計或軟體邏輯”零 bug 地滿足規格”的方法論——它不是”跑更多測試”，而是”從原理上證明沒有遺漏”。

3 分鐘產業解釋

為什麼形式驗證突然變重要？

在 AI 晶片時代，一顆 SoC 的電晶體規模動輒數百億，設計週期中的 驗證工作量已佔總研發人力的 60%–70% [行業經驗估算，Synopsys/Cadence 多次公開報告引用類似比例]。傳統的模擬（Simulation）方法本質上是”列舉輸入看輸出”，面對天文級狀態空間根本跑不完。形式驗證的核心優勢在於：它窮舉所有可能的輸入組合，在數學上給出”屬性成立”或”反例”的確定性結論。

從產業鏈位置看，形式驗證處於 EDA（電子設計自動化）工具鏈的 驗證環節，與模擬（Simulation）、硬體模擬（Emulation）和原型驗證（Prototyping）並列為四大驗證支柱。它與 AI 晶片設計 的交匯點在於：

規模爆炸：大型模型晶片的互連網路（NoC）、快取一致性協議、DMA 控制器等模組狀態空間巨大，傳統模擬覆蓋不到的角落恰恰是形式驗證的強項；
安全關鍵：自動駕駛、具身智慧等場景要求晶片功能安全等級（ISO 26262 ASIL-D），標準明確要求或推薦使用形式方法；
上行流片成本：先進製程一次流片成本 [估計數千萬至數億美元，具體取決於製程節點和晶片規模]，bug 逃逸的代價極高。

15 分鐘專家深入

形式驗證在 EDA 驗證流程中的定位

┌──────────────────────────────────────────────────────┐
│              晶片設計驗證全景                          │
│                                                      │
│  ┌────────────┐  ┌────────────┐  ┌──────────────┐   │
│  │  動態驗證    │  │  靜態驗證    │  │  硬體輔助驗證  │   │
│  │ (Simulation)│  │  (Formal)   │  │(Emul/Proto)  │   │
│  │            │  │            │  │              │   │
│  │ RTL模擬     │  │ 等價性檢查   │  │ 硬體模擬器    │   │
│  │ UVM測試平台 │  │ 屬性檢查     │  │ FPGA原型      │   │
│  │ 隨機激勵     │  │ 模型檢驗     │  │              │   │
│  │ 覆蓋率驅動   │  │ 定理證明     │  │              │   │
│  └────────────┘  └────────────┘  └──────────────┘   │
│                                                      │
│  覆蓋率=機率性的     結論=確定性的    速度≈真實執行      │
│  可處理大規模        規模有上限       可處理大規模        │
└──────────────────────────────────────────────────────┘

三大核心方法論

1. 等價性檢查 (Equivalence Checking)

用途： 驗證兩個設計描述在邏輯功能上是否等價。最常見的場景是 RTL-to-Gate（RTL vs 綜合後網表） 等價性檢查——綜合工具把 RTL 變成門級網表後，要證明變換沒有引入功能錯誤。

技術本質： 將兩個電路的對應輸出構造為異或（XOR）門，然後證明該異或表示式恆為 0（即不可滿足）。這本質上歸約為 SAT（布林可滿足性） 問題。

關鍵引數（定性）：

組合等價性檢查：已基本工業化成熟，可處理超大規模電路；
順序等價性檢查（Sequential EC）：需要考慮暫存器狀態對映，複雜度顯著上升，仍是研究前沿之一。

2. 模型檢驗 (Model Checking)

用途： 驗證一個有限狀態系統是否滿足用時態邏輯（如 CTL / LTL / SVA）描述的屬性。

技術本質： 窮舉系統的所有可達狀態，檢查每個狀態（或狀態路徑）是否滿足屬性。如果違反，自動生成 反例（Counterexample）。

關鍵瓶頸——狀態空間爆炸：

狀態數隨暫存器數量呈指數增長（n 個暫存器 → 2^n 個狀態）；
應對策略：
- 符號模型檢驗（Symbolic Model Checking）：用 BDD（二元決策圖）或 SAT/SMT 符號化表示狀態集合，避免逐狀態列舉；
- 有界模型檢驗（Bounded Model Checking, BMC）：只檢驗 k 步以內的執行路徑，將問題編碼為 SAT/SMT 例項；逐步增大 k（k-induction）可擴充套件到無界證明；
- 抽象-精化（Abstraction-Refinement, CEGAR）：先在抽象模型上驗證，如遇反例再精化抽象層次。

3. 定理證明 (Theorem Proving)

用途： 對無限狀態系統、複雜演算法正確性進行證明，表達能力最強。

技術本質： 在某種形式邏輯（如高階邏輯 HOL、一階邏輯）中，由人類引導（互動式）或自動地構造證明。

代表工具： Isabelle/HOL、Coq、Lean、ACL2。在工業晶片驗證中的直接使用相對較少，但在 微處理器指令集驗證（如 ARM、RISC-V 形式化規約）和 安全關鍵軟體 領域有重要應用。

核心求解引擎：SAT 與 SMT

形式驗證工具的”發動機”是 SAT/SMT 求解器：

概念	說明
SAT（Boolean Satisfiability）	給定一個布林公式，判斷是否存在一組變數賦值使公式為真。NP-完全問題，但現代 DPLL/CDCL 求解器在工業例項上表現驚人
SMT（Satisfiability Modulo Theories）	SAT 的擴充套件，支援位向量算術、陣列理論、未解釋函式等。代表性求解器：Z3（微軟）、CVC5、Yices
BDD（Binary Decision Diagram）	布林函式的規範表示形式，在等價性檢查和符號模型檢驗中廣泛使用

產業趨勢： SAT/SMT 求解器效能在過去 20 年有數個量級的提升（DPLL → CDCL → 並行 SAT），這是形式驗證工具實用化的根本推動力。

屬性描述語言：SVA（SystemVerilog Assertions）

在晶片驗證中，形式屬性檢查通常使用 SVA 來描述待驗證的屬性：

// 簡化示例：請求發出後 3 週期內必須得到應答
property req_grant;
  @(posedge clk) req |-> ##[1:3] grant;
endproperty

assert property (req_grant)
  else $error("Grant not received within 3 cycles");

SVA 屬性可以在模擬（動態檢查）和 形式驗證（窮舉證明）中同時使用，這使得形式驗證可以無縫嵌入現有 UVM 驗證流程。

技術原理（最深）

從 SAT 求解到屬性證明的完整路徑

以”屬性檢查（Property Checking）“為例，說明形式驗證工具的內部工作流：

輸入:  RTL設計 + SVA屬性
          │
          ▼
┌─────────────────────┐
│ 1. 展開 (Unrolling)  │  將時序電路展開為組合邏輯
│    k-cycle unroll    │  (BMC 場景下展開 k 步)
└─────────┬───────────┘
          │
          ▼
┌─────────────────────┐
│ 2. 編碼 (Encoding)   │  將 RTL 邏輯 + 屬性違例條件
│    → SAT/SMT 例項    │  編碼為可滿足性問題
└─────────┬───────────┘
          │
          ▼
┌─────────────────────┐
│ 3. 求解 (Solving)    │  CDCL SAT / SMT Solver
│    找解 or UNSAT     │  輸出: SAT(反例) 或 UNSAT(證明)
└─────────┬───────────┘
          │
     ┌────┴────┐
     ▼         ▼
   SAT       UNSAT
 (反例)    (屬性在 k 步內成立)
     │         │
     ▼         ▼
  報告Bug   增大 k 或
            使用歸納法
            證明無界成立

k-Induction（k 歸納法）

單純的 BMC 只證明”前 k 步內無反例”，不是無界證明。k-induction 補全了這一缺陷：

Base case： 證明屬性在前 k 步內成立（BMC）；
Inductive step： 假設屬性在前 k 步都成立，證明第 k+1 步也成立；
若兩者均通過 → 屬性對所有可達狀態無界成立。

形式驗證的計算複雜度邊界

方法	理論複雜度	實際可處理規模（定性）
組合等價性檢查	coNP-完全	工業級 SoC 子模組均可處理
BMC (k-bounded)	NP (每步)	依賴 k 值和電路寬度，數百至數千暫存器可行
無界模型檢驗	PSPACE	狀態空間爆炸嚴重，通常需要高度抽象
定理證明	半可判定	表達力最強但需要大量人工互動

關鍵認知：形式驗證不是萬能的。 它適合驗證 區域性模組的精確屬性（如協議合規、FIFO 滿/空邏輯、時鐘域交叉安全性），而非對整個 SoC 做端到端全覆蓋。工業實踐中的最佳模式是 “形式驗證覆蓋最危險的角落，模擬/硬體模擬覆蓋廣度”。

ABV（Assertion-Based Verification）工作流

┌───────────────────────────────────────────────┐
│              ABV 統一架構                       │
│                                               │
│  SVA 屬性/斷言                                  │
│       │                                       │
│       ├──→ 模擬環境(UVM) ── 動態檢查            │
│       │    隨機激勵下觸發斷言違例即報錯            │
│       │                                       │
│       └──→ 形式驗證引擎 ── 靜態窮舉證明           │
│            數學證明屬性無界成立/給出反例            │
│                                               │
│  同一套屬性 → 兩種驗證手段複用                    │
└───────────────────────────────────────────────┘

技術演進史

時期	里程碑	意義
1960s	數學邏輯基礎奠定（命題邏輯、一階邏輯）	理論根基
1981	Edmund Clarke & Allen Emerson 提出模型檢驗（Model Checking）	時序邏輯+狀態空間搜尋的範式誕生
1986	Bryant 發表 BDD 論文	符號模型檢驗的數學工具
1990s	SAT 求解器從 DPLL 演進到 CDCL（Chaff, MiniSat 等）	實用化關鍵突破
1994	Pentium FDIV bug（浮點除法缺陷）導致 Intel 數億美元損失	業界痛感：驗證不足的代價
1996	Intel 成立專門形式驗證團隊	大廠全面擁抱形式方法
2010s	Cadence 收購 Jasper Design Automation（2014），整合 JasperGold 平台	形式驗證產品化深度整合，商用化加速
2007	Clarke, Emerson, Sifakis 獲圖靈獎	形式驗證方法論獲最高學術認可
2010s	Synopsys 推出 VC Formal；形式驗證與 UVM/SVA 深度整合	工業流程標準化
2018+	RISC-V 形式化驗證（如 RISC-V Sail 模型、SiFive 形式化驗證實踐）	開源 ISA 驅動形式方法民主化
2021	Siemens EDA (Mentor) 收購 OneSpin Solutions	形式驗證賽道整合加速
2022+	AI 輔助形式驗證探索（用 ML 引導 SAT 求解、自動屬性生成）	新一代範式探索

技術路線對比

維度	模擬 (Simulation)	形式驗證 (Formal)	硬體模擬 (Emulation)
結論性質	機率性的（“未發現 bug”）	確定性的（“證明無 bug”或給出反例）	機率性的
狀態覆蓋	僅覆蓋激勵觸達的狀態	窮舉所有可達狀態（可處理範圍內）	僅覆蓋激勵觸達的狀態
設計規模上限	大（可完整 SoC）	中小（通常模組級）	大（可完整 SoC）
執行速度	慢（RTL 級 ~kHz）	不執行，求解時間取決於 SAT/SMT	快（~MHz 級）
除錯便利性	好（波形回溯）	反例 trace 可除錯，但不如波形直觀	好
屬性表達	Testbench 程式碼	SVA / 時態邏輯（更精確）	Testbench 程式碼
典型用途	功能驗證廣度覆蓋	協議合規、關鍵路徑證明、等價性檢查	系統級驗證、軟體聯調
工具代表	Synopsys VCS, Cadence Xcelium, Siemens QuestaSim	Synopsys VC Formal, Cadence JasperGold, Siemens Questa Formal	Cadence Palladium, Synopsys ZeBu
成本	中	中（工具+專業人才）	高（專用硬體）

上下游

上游（形式驗證工具依賴什麼）

層次	具體要素
求解引擎	SAT/SMT 求解器（Z3、ABC、MiniSat 等）；BDD 庫
設計輸入	RTL 程式碼（Verilog/SystemVerilog/VHDL）；形式規約（SVA、PSL）
硬體平台	通用伺服器（CPU 密集型，記憶體密集型）；部分場景可用 GPU 加速 SAT
知識與人才	形式驗證工程師（稀缺崗位，需同時懂硬體設計和數學邏輯）

下游（形式驗證輸出服務於什麼）

層次	具體要素
直接輸出	驗證通過報告 / 反例 trace / 覆蓋率度量
服務物件	晶片 tape-out 決策、功能安全認證（ISO 26262 / DO-254）、IP 籤核（sign-off）
終端應用	AI 晶片、自動駕駛晶片、航空電子、通訊晶片、處理器

產業鏈位置圖

晶片設計公司(Fabless)          EDA 工具廠商
 ┌─────────────┐         ┌─────────────────┐
 │ 架構設計      │         │ Synopsys        │
 │ RTL編碼      │◄───────►│ Cadence         │
 │ 驗證(含形式)  │  工具授權 │ Siemens EDA     │
 │ 綜合/P&R     │         │ (以及創業公司)    │
 └──────┬──────┘         └─────────────────┘
        │
        ▼
   代工廠(Foundry) tape-out

關鍵指標

指標	說明
證明深度 (Proof Depth)	BMC 中 k 的最大值；無界證明是否成功
屬性覆蓋率	被形式證明覆蓋的屬性佔總屬性的比例
狀態空間大小	可達狀態數，反映驗證難度
求解時間	SAT/SMT 呼叫的 wall-clock 時間
反例深度	發現屬性違例所需的最短執行步數
引擎證明能力 (Proven/Undetermined/Fail)	工具對每條屬性輸出三種狀態：已證明、未定（超出能力範圍）、反例
收斂率 (Convergence)	在給定時間內成功完成證明的屬性比例
抽象精度 vs 計算代價	抽象程度越高求解越快但可能誤報；需權衡

供需與市場資料

市場規模（定性）

全球 EDA 市場規模約 [150–170 億美元，據 Synopsys/Cadence 財報及行業報告綜合估算]；
其中 驗證環節 佔 EDA 營收的較大比重（驗證工具 + IP 驗證服務，估計佔 30%–40%）；
形式驗證 是驗證子市場中增長最快的細分之一，但其絕對規模未被單獨揭露 [未充分揭露]；
形式驗證工具通常以 年度訂閱許可證 模式銷售，單個大型客戶年許可費 [估計數百萬至千萬美元量級]。

需求驅動因素

驅動力	方向
AI 晶片設計複雜度上升	↑
先進製程流片成本飆升	↑
功能安全法規（ISO 26262、DO-254）強制性要求	↑
RISC-V 生態對形式化驗證的需求	↑
Chiplet/UCIe 互連協議驗證	↑
形式驗證人才供給不足（瓶頸）	↓（限制需求釋放）

供給側格局

“三巨頭”壟斷：Synopsys、Cadence、Siemens EDA 佔據全球 EDA 市場絕大部分份額（合計約 [70%–80%，據公開財報估算]），形式驗證工具亦由三者主導；
創業公司 / 開源方向存在一定空間（如開源 SAT/SMT 求解器、學術工具商業化）。

代表公司與資本對映

公司	形式驗證相關產品/動作	上市/資本狀態
Synopsys (SNPS)	VC Formal；收購多家形式驗證相關資產	納斯達克上市
Cadence (CDNS)	JasperGold Formal Verification Platform（~2014 年收購 Jasper）	納斯達克上市
Siemens EDA（原 Mentor Graphics）	Questa Formal；~2021 年收購 OneSpin Solutions	Siemens 子公司（母公司法蘭克福上市）
Alphawave Semi	IP 驗證中使用形式方法	倫交所上市
Axiomise	專注形式驗證培訓與諮詢服務（英國）	私有
學術/開源生態	Z3（微軟）、ABC（UC Berkeley）、Coq、Isabelle、Lean	非商業/開源

投資邏輯

看多邏輯

EDA 賽道本身的高壁壘 + 粘性：形式驗證工具嵌入客戶設計流程後切換成本極高，續費率穩定；
AI 晶片爆發 → 驗證需求非線性增長：晶片越複雜，形式驗證從”錦上添花”變為”不可或缺”；
功能安全法規是硬性驅動：ISO 26262 ASIL-C/D 明確推薦或要求使用形式方法，自動駕駛晶片必須合規；
驗證工程師人力成本飆升：形式驗證工具自動化程度提升 → 替代人工 → TCO 優勢凸顯；
RISC-V + 開源硬體生態擴張：新 ISA 的形式化規約需求開啟增量市場。

看空/風險

形式驗證的 TAM 仍相對有限：它始終是驗證工具鏈的一部分，而非替代整個流程；
人才瓶頸可能限制滲透率提升速度；
AI 輔助驗證（ML-guided）尚未被證明能根本改變形式驗證的規模邊界；
EDA 大廠已高度集中：創業公司切入困難，併購整合已基本完成。

產業鏈投資視角

直接標的:  SNPS / CDNS / SIE.DE (EDA 三巨頭的形式驗證業務)
間接受益:  AI 晶片設計公司 (NVIDIA/AMD/Google TPU/國產AI晶片)
           → 它們的驗證支出是 EDA 廠商的營收
上游依賴:  SAT/SMT 求解器技術突破可能改變競爭格局

常見誤讀糾偏

❌ 誤讀 1：“形式驗證可以完全替代模擬”

糾偏： 形式驗證和模擬是互補關係，不是替代關係。形式驗證受限於狀態空間規模，通常只能在 模組級（而非全 SoC）進行窮舉驗證。工業實踐的最佳策略是：用形式驗證覆蓋最關鍵的屬性（協議合規、安全相關邏輯），用模擬覆蓋廣度和系統級場景。兩者的覆蓋率指標含義也完全不同。

❌ 誤讀 2：“形式驗證通過 = 晶片沒有 bug”

糾偏： 形式驗證證明的是 “設計滿足規格（spec）“，而規格本身可能是錯的或不完整的。形式驗證保證的是 實現與規約的一致性，而非規約與真實需求的一致性。此外，形式模型通常不涵蓋類比電路效應、時序違規（STA 覆蓋）、製造缺陷等物理層面的問題。

❌ 誤讀 3：“形式驗證只適用於安全關鍵的小眾領域”

糾偏： 雖然功能安全法規推動了形式驗證的普及，但事實上 Intel、ARM、Qualcomm、NVIDIA 等主流晶片公司在 通用處理器、GPU、移動 SoC 的設計中也廣泛使用等價性檢查（幾乎所有先進晶片的設計流程中都已標配）和屬性檢查。形式驗證早已不是小眾方法論。

❌ 誤讀 4：“AI 將很快讓形式驗證實現全自動化”

糾偏： 當前 AI 輔助形式驗證的研究（如用強化學習引導 SAT 求解、用 LLM 自動生成 SVA 屬性）仍處於 早期探索階段。形式驗證的核心難點——狀態空間爆炸和屬性規約的人工建模——尚未被 AI 有效突破。短期內 AI 更可能在 輔助屬性生成 和 求解啟發式最佳化 上提供增量幫助，而非根本顛覆。

學習路徑

入門（0–3 個月）

概念理解： 閱讀《Formal Verification: An Essential Toolkit for Modern VLSI Design》（Erik Seligman 等，Synopsys 出版）——面向工程師的入門書，不涉及過多數學；
SVA 學習： 學習 SystemVerilog Assertions 基礎語法，理解 assert/assume/cover 三類約束；
工具實操： 使用開源 SAT 求解器 MiniSat 或 Z3 做簡單練習。

進階（3–12 個月）

模型檢驗理論： 學習時態邏輯（CTL/LTL），理解符號模型檢驗和 CEGAR 架構；
BMC/k-induction 深入： 理解有界模型檢驗到無界證明的橋接方法；
工業實踐： 學習 Cadence JasperGold 或 Synopsys VC Formal 的使用方法論（可從廠商技術白皮書和培訓材料入手）；
論文精讀： “SAT/SMT 求解器” 經典論文（如 MiniSat, Z3）。

專家（12+ 個月）

定理證明： 學習 Isabelle/HOL 或 Lean，理解互動式定理證明範式；
RISC-V 形式化： 參與 RISC-V Sail 模型或相關形式化驗證開源專案；
前沿探索： 關注 AI+形式驗證交叉領域（ML-guided abstraction refinement, LLM for property generation）。

一句話總結

形式驗證是用數學窮舉取代測試列舉，在晶片設計複雜度和流片成本同步飆升的時代，它從”nice-to-have”變成了”must-have”——而 EDA 三巨頭對這一工具鏈的壟斷，構成了 AI 晶片基礎設施中最隱形但最堅固的護城河之一。

延伸閱讀與來源

資源	型別	說明
Clarke, Grumberg, Peled《Model Checking》	書籍	模型檢驗領域經典教材
Seligman et al.《Formal Verification: An Essential Toolkit for Modern VLSI Design》	書籍	工業導向入門
Cadence JasperGold 官方技術文件	工業文件	屬性檢查工具使用指南
Synopsys VC Formal Application Notes	工業文件	VC Formal 應用方法論
E. M. Clarke 圖靈獎演講 (2007)	演講	形式驗證發展史的權威敘述
RISC-V Formal Verification 工作組	社群	RISC-V 形式化驗證實踐前沿
DAC / ICCAD / FMCAD 會議論文	學術	形式驗證最新研究進展
Synopsys/Cadence 年度財報（投資者日演示）	財務	EDA 驗證工具市場資料參考

資料口徑宣告： 本文中所有具體市場數字均為基於公開財報和行業報告的估算值，已標註 [估算] 或 [未充分揭露]。硬規格（如工具版本號、精確價格等）未引用，因檢索失敗無法獲得可驗證來源。如需精確資料，請查閱各公司最新 SEC 檔案（10-K/10-Q）及 EDA 行業報告（如 SEMI、ESD Alliance 資料）。