從「我試了一百萬個輸入」到「我把全部都證明了」
想像你蓋了一座橋，安檢員開著重卡來回輾過一千次都沒塌。這很令人安心——但它並不是橋很安全的「證明」。也許你從沒試過的那一車載重、在你從沒量過的那個溫度下，正好就是會把橋壓垮的那一筆。這條學習路徑到目前為止的每一章，都是那台卡車：指向式測試、約束隨機的 UVM 激勵、覆蓋率儀表板。它們開了天文數字那麼多台卡車過橋，盯著看會不會塌。這就是動態驗證，而且不可或缺。但它和卡車有同一個致命限制——它永遠只能跑你實際產生出來的那些輸入。
形式驗證問的是一個完全不同的問題。它不去執行設計，而是替你的邏輯建立一個數學模型，然後用一個自動推理引擎——SAT 或 SMT 求解器，跟驅動定理證明器同一家族的工具——去一次證明或推翻一個關於「所有可能輸入、所有可達狀態」的陳述。沒有激勵要寫。你陳述一條性質——「這個 FIFO 永遠不會溢位」、「同一週期內 grant 永遠不會同時給兩個 master」——工具要嘛回給你一個「它永遠成立」的證明，要嘛給你一段具體的反例波形，精確示範怎麼讓它壞掉。跑一次，等於無限台卡車。
斷言變成定理：形式性質檢查
這就是第 7 級開始回本的地方。你為了在模擬中抓協定違規而寫的那些 SystemVerilog 斷言（SVA），正好就是形式驗證需要的輸入。在模擬裡，斷言是一條絆索——只有當某個正在跑的測試剛好踩上去時才會觸發。把同一條斷言交給形式性質檢查工具，它就變成一條要被證明的定理：求解器會在整個可達狀態空間裡，搜尋任何一條會讓這條斷言失敗的軌跡。同一行程式碼，保證的強度卻天差地遠。
性質分成兩種口味。安全性（safety）性質說的是「壞事永遠不會發生」（`assert never two_grants`）。活性（liveness）性質說的是「好事終究會發生」（`assert request |-> ##[1:$] grant`——每個 request 最終都會被 grant）。安全性性質是性質檢查的日常主食；活性則需要工具對「無界的時間」做推理，比較難，但對現代引擎而言已是家常便飯。真正的功夫在於：寫出既有意義（真的捕捉到設計意圖）又可被證明（工具真的能在上面收斂）的性質。
// A round-robin arbiter for 2 masters. Rung-7 assertions, now
// handed to a FORMAL tool as theorems over ALL inputs.
module arb (input logic clk, rst_n,
input logic req0, req1,
output logic gnt0, gnt1);
// ... RTL that picks a winner each cycle ...
endmodule
// --- Properties bound to the design (in a separate .sva file) ---
// SAFETY: never grant both masters in the same cycle (mutual exclusion)
ap_mutex: assert property (@(posedge clk) disable iff (!rst_n)
!(gnt0 && gnt1));
// SAFETY: never grant a master that didn't ask
ap_no_spurious: assert property (@(posedge clk) disable iff (!rst_n)
(gnt0 |-> req0) and (gnt1 |-> req1));
// LIVENESS: a held request is eventually granted (no starvation)
ap_no_starve: assert property (@(posedge clk) disable iff (!rst_n)
req0 |-> s_eventually gnt0);
// Tool result (illustrative):
// ap_mutex : PROVEN (holds for all reachable states)
// ap_no_spurious: PROVEN
// ap_no_starve : FAILED -> counterexample (CEX) of depth 6:
// cyc0 req0=1 req1=1 gnt0=0 gnt1=1 <- req1 always wins
// cyc1 req0=1 req1=1 gnt0=0 gnt1=1 because priority is
// ... fixed, not rotating
// => req0 starves forever. Fix the arbiter, not the property.求解器如何在時間裡搜尋：有界模型檢查
工具怎麼可能不跑任何輸入，卻能證明關於*所有*輸入的陳述？最主力的技術是有界模型檢查（BMC）。它的想法極為具體：把你的時序電路像翻頁動畫一樣在時間軸上展開。每個時脈週期複製一份組合邏輯，把每一份正反器的輸出接到下一份的輸入，你就得到一個巨大、純組合的公式，代表前 *k* 個週期內的所有行為。再把你性質的「否定」加進去——「找出一個會讓它*失敗*的狀態」——然後把整包丟給 SAT 求解器。
Unrolling the circuit for Bounded Model Checking (depth k):
state s0 --[comb logic]--> s1 --[comb logic]--> s2 -- ... --> sk
| in0 | in1 | in2
v v v
P(s0)? P(s1)? P(s2)? <- property
SAT query: s0 = reset_state
AND (transition s0->s1) AND (transition s1->s2) ...
AND ( NOT P(s0) OR NOT P(s1) OR ... OR NOT P(sk) )
SAT -> the solver found inputs in0..ink that reach !P => BUG (CEX)
UNSAT-> no failing trace exists within k cycles => safe so far
Push k deeper (k=20, 50, 200...) until either a CEX appears
or a PROOF technique (k-induction / IC3) closes it for ALL k.如果求解器回 SAT，它就是真的找到了「每個週期該餵什麼輸入」才能把電路逼進失敗狀態——那*就是*你的反例。如果它在深度 *k* 回 UNSAT，代表這條性質至少撐了 *k* 個週期。關鍵的微妙之處在於：一次普通的 BMC 若什麼都沒找到，它只證明了到那個界限為止的安全性；臭蟲可能潛伏在第 *k+1* 週期。要得到無界的證明——「永遠成立」——工具會疊上歸納式技術（k-歸納、插值法，或著名的 IC3/PDR 演算法）來確立這條性質是「歸納不變式」：若現在成立，下一週期就必定成立，對所有狀態皆然。一旦它收斂，你就有了完整的證明；在那之前，你手上是一個非常強的有界保證。
把圍籬畫出來：約束與假設
每個形式驗證的新手都有一個陷阱在前面等著。若你不設限就直接跑一條性質，求解器會樂呵呵地餵給你的設計一堆*物理上不可能*的輸入——reset 每個週期亂跳、匯流排協定的 request 在沒有合法交握的情況下就拉高、同一拍出現兩個非法 opcode——然後回報一個在真實系統裡根本不會發生的「失敗」。這些是假反例，源自求解器去探索了你的環境根本不會產生的輸入。解法是用約束與假設去*界定證明空間*。
在 SVA 裡，關鍵字是 `assume`。`assert` 說的是*「工具必須證明這件事永遠為真」*，而 `assume` 說的是*「工具可以把這件事當成合法輸入、視為理所當然」*。假設用來描述真實環境：包圍你區塊的匯流排協定、reset 序列、某個輸入是 one-hot 的事實。約束得太少，你會被假失敗淹沒；約束得太多——也就是過度約束（over-constraint）——你等於不小心叫求解器去忽略「臭蟲正好藏身」的那個情境，於是拿到一個毫無意義的綠色 PROVEN。把這道圍籬校準到剛好，是形式驗證裡最重要的一項功夫。
// Without assumptions, the solver invents illegal stimulus and
// reports bogus failures. Assumptions pin the inputs to legal ones.
// ASSUME the environment holds reset, then releases it once:
am_reset_seq: assume property (@(posedge clk)
$fell(rst_n) |=> rst_n[*1:$]); // reset deasserts and stays high
// ASSUME the upstream master obeys the handshake:
am_valid_stable: assume property (@(posedge clk) disable iff(!rst_n)
(valid && !ready) |=> valid && $stable(data));
// ASSUME the opcode is always one of the legal encodings:
am_legal_op: assume property (@(posedge clk) disable iff(!rst_n)
op inside {ADD, SUB, LD, ST, NOP});
// Now ASSERT the real property; the proof is valid ONLY inside
// the world carved out by the assumptions above.
ap_result_correct: assert property (@(posedge clk) disable iff(!rst_n)
(op == ADD) |=> (result == $past(a) + $past(b)));
// RULE OF THUMB: assert = "prove this" assume = "trust this input"
// An over-tight assume can turn a real bug into a false PROVEN.
// => Always sanity-check assumptions (formal coverage / vacuity).合成有沒有騙人？等價性檢查
形式驗證還有第二項、完全不同的超能力，而且幾乎每一顆晶片都靠它。當你跑邏輯合成時，你那份人讀得懂的 RTL 會被機械式地轉換成閘級網表（netlist）——接著被最佳化、重新計時（retiming）、插入時脈閘控、縫入掃描鏈，並在佈局繞線時加上緩衝器。每一步都是工具為了面積、時序與功耗在改寫你的邏輯。你怎麼知道送進晶圓廠的那份網表，仍然算的是跟你辛苦驗過的 RTL *一樣的函數*？你不可能在閘級網表上把整套 UVM 重跑一遍——那得花好幾週。於是你改用等價性檢查。
等價性檢查器——嚴格說是日常用的*組合式*等價性檢查器（CEC）——會吃進兩份設計，先辨識出它們相對應的狀態元件與主要 I/O（也就是關鍵點 / key points），然後形式地證明：對*每一個*可能的輸入，驅動每條輸出的邏輯錐在 RTL 與網表之間都是布林等價的。它不做模擬，而是用同一套 SAT 引擎直接證明等價。正因為它只比較暫存器之間的組合邏輯，它繞開了狀態爆炸問題，能擴展到上億閘規模的設計——這也正是它幾乎會在每個區塊、每一次合成與佈局繞線交接時都跑一遍的原因。
Equivalence Checking: golden RTL vs. synthesized netlist
RTL (golden) Gate netlist (revised)
┌────────────────────┐ ┌──────────────────────────┐
in ─►│ a&b | c │─► out in ─►│ NAND-NAND remap, buffers,│─► out
│ (behavioural) │ │ clock-gating, scan FFs │
┌─►ff │ │ ┌─►ff │ (logically equal?) │
└────────────────────┘ └──────────────────────────┘
│ │
└──────── match key points ──────┘
For each output cone: prove RTL(out) XOR NETLIST(out) == 0
for ALL input combinations.
PASS : every key point is logically identical -> synthesis safe
FAIL : a miscompare point + input pattern that distinguishes them
(e.g. a wrong don't-care optimization, dropped reset, or a
mis-set retiming option) -> netlist does NOT equal RTL.兩張網，一次簽核：形式與動態並肩
我們很容易想把形式驗證捧為贏家——畢竟它會*證明*。但請忍住。形式與動態驗證不是對手，而是橫跨在不同缺口上的兩張網，真正的簽核兩者都需要。形式驗證徹底卻局部：它擅長有界、以控制為主的性質，以及等價性，但它在很深的資料路徑上會卡住，也很難表達「這個 JPEG 解碼器產生的影像在視覺上是正確的」。模擬與 UVM 則淺卻全域：它們用真實的軟體、真實的模型、完整的系統情境去跑*整顆* SoC，但只跑你產生出來的那些激勵。驗證的前沿，就在於懂得每張網當初是為了補哪一個缺口而設計的。
- 控制邏輯優先想到形式：那些一旦出錯就會釀災、而狀態空間又還算可控的地方——仲裁器、FSM、FIFO、暫存器存取映射、死結與匯流排協定遵循。在這裡，徹底的證明勝過再多的隨機模擬。
- 端到端行為靠模擬／UVM：整體行為、效能、嵌入式軟體開機、混合訊號、寬資料路徑——凡是「跑起真實系統」比「證明單一性質」更重要的地方。
- 讓斷言架起橋樑。同一條 SVA 既能在 UVM 裡當絆索跑，*也*能在形式驗證裡當定理證——寫一次，模擬端拿到覆蓋率、形式端拿到證明。
- 每一次交接都跑等價性檢查：從 RTL 一路到佈局資料庫——它不容妥協、輕量，而且能抓到「在 RTL 上模擬永遠看不到」的那一類臭蟲，因為那類臭蟲就活在合成／佈局繞線的轉換本身裡。
這條學習路徑也就此收尾。你從寫測試平台、盯波形開始；學會了隨機化激勵、量測覆蓋率、把 UVM 環境搭起來，並用斷言把行為釘死。如今，那些斷言已變成數學定理，你的合成被證明是忠實的，而你也說得清楚：為什麼一個成熟的專案會同時把數百萬美元砸進一座回歸測試農場、又砸進一支形式驗證團隊。驗證的重點從來不是跑更多測試——而是在第一片晶圓被蝕刻之前，建立一個有根據、分層的論證，去主張這顆晶片是正確的。