跳轉到

1990s - 形式驗證：窮盡狀態空間的數學偵探#

案件摘要#

1990 年代，形式驗證（Formal Verification）進入 EDA 主流：Bryant 的 BDD（1986）給出布林函式的正則形式， CMU 的 SMV 把 model checking 帶進硬體，Synopsys Formality、Cadence Conformal 把等價性檢查變成流程標準。 它不靠測試向量，而是用數學證明「兩個電路（或性質）在所有輸入下永遠一致」—— 模擬永遠漏案，形式驗證則宣稱：結案即全案終結。

前因 -- 為什麼會有這個案子#

  • 模擬的罩門：百萬狀態的設計，模擬永遠只能踩過狀態空間的一小角；致命 corner case（如 FIFO 滿溢與空讀同 cycle）往往漏網。
  • 流程需要證明：邏輯合成（1986）之後，RTL 與網表是兩個不同的電路——誰來保證合成器沒有改寫功能？
  • 學界已備好理論：Clarke–Emerson–Sifakis（1981）的 temporal logic model checking、Bryant（1986）的 BDD、1990s 的 SAT（DPLL 系）全部就位。
  • 關鍵推理：等價性檢查只需證明一個 XOR 函式恆為 0：
\[ \text{等價} \iff f \oplus g \equiv 0 \iff \underbrace{\neg\,\exists x}_{\text{不可滿足}}\ \ f(x) \ne g(x) \]

模擬說「我試了 \(10^9\) 個向量都沒事」，形式驗證說「所有 \(x\) 都沒事」。

線索與推理 -- 數學式、程式、理論#

1. 案件現場：miter 與等價性檢查#

把兩個電路接成 miter：同名輸入並聯、輸出接 XOR——

\[ \text{miter}(f,g) = f \oplus g = (f \land \bar{g}) \lor (\bar{f} \land g) \]
  • miter 可滿足（ \(\exists x: f \oplus g = 1\) ）⇔ 兩電路不等價，SAT solver 找出的滿足指派就是反例（counterexample）。
  • miter 不可滿足 ⇔ 等價，證明成立——這就是 Formality / Conformal 的核心。

2. BDD：布林函式的正則形式#

Ordered BDD（Bryant, 1986）：把布林函式表示成變數序固定的決策圖，經化簡後同構唯一——

\[ f = \text{ITE}(x_1,\ f|_{x_1=1},\ f|_{x_1=0}),\qquad \text{Shannon expansion} \]
  • 正則性：兩個等價函式化簡後的 BDD 完全同構，等價性檢查變成 \(O(1)\) 圖比對。
  • 運算封閉： \(\text{ITE}\) 、AND、OR、XOR 都可在 BDD 上以多項式時間完成（Shannon 沿途遞迴合併）。
  • 弱點：變數序不佳時 BDD 指數爆炸；乘法器等電路天生難壓——這正是後來 SAT 接班的原因。

3. Model checking：狀態空間的窮舉#

CTL model checking（Clarke–Emerson–Sifakis, 1981）：給定狀態機 \(M\) 與性質 \(\varphi\) （如 AG(request → AF ack)）， 判定 \(M, s_0 \models \varphi\) ——在所有可達狀態上成立：

\[ \text{reach}(M) = \{s : s_0 \to^{*} s\},\qquad M \models \text{AG}\,\varphi \iff \forall s \in \text{reach}(M): s \models \varphi \]
  • 以不動點迭代在 BDD 上計算可達集與 \(\varphi\) 的滿足集，狀態空間爆炸（state explosion）是主要瓶頸。
  • 反例給出具體執行軌跡（waveform），讓工程師一眼看到作案路徑。

4. SAT solver：2000 年代的接班人#

DPLL（1962）＋ clause learning ＋ VSIDS 啟發式 = Chaff SAT（2001, Princeton）：

\[ \text{SAT} \in \text{NP-complete},\quad \text{但 Chaff 讓萬級子句的實際案子秒解} \]
  • SAT-based equivalence checking 擺脫 BDD 變數序陷阱，成為 2000s 後的主流。
  • 對組合電路，structural hashing（合併同構閘）先行瘦身，SAT 只處理殘局——大多數等價性案子根本不用動用 SAT。

5. Verilog 速記：等價性檢查的現場#

// RTL：f = (a & b) | c
module rtl (input a, b, c, output f);
    assign f = (a & b) | c;
endmodule
// 合成後網表（De Morgan 改寫）：f = ~((~(a&b)) & ~c)
module netlist (input a, b, c, output f);
    wire n0, n1;
    assign n0 = ~(a & b);
    assign n1 = ~(n0 & ~c);
    assign f  = n1;
endmodule
// miter：f_rtl ^ f_netlist 恆為 0 → 等價成立，結案

6. Python 實作：Shannon expansion 等價性判定#

from functools import lru_cache

@lru_cache(maxsize=None)
def eval_f(expr, x1, x2, x3):          # 用 eval 直接評布林表示式
    return eval(expr, {'a': x1, 'b': x2, 'c': x3})

def equivalent(e1, e2, n=3):            # 窮舉 2^n 指派，找反例
    for m in range(1 << n):
        bits = tuple((m >> i) & 1 for i in range(n))
        if eval_f(e1, *bits) != eval_f(e2, *bits):
            return False, bits          # 反例指派（counterexample）
    return True, None                   # 所有指派一致 → 等價

cases = [('(a & b) | c', '~((~(a & b)) & ~c)'),   # De Morgan 等價
         ('(a & b) | c', 'a & (b | c)'),          # 分配律不成立 → 應有反例
         ('(a | b) & (a | c)', 'a | (b & c)')]    # 分配律成立 → 等價
for e1, e2 in cases:
    ok, ce = equivalent(e1, e2)
    print(f"{e1}  ≡  {e2} : {ok}" + (f"  反例 a,b,c = {ce}" if ce else ""))
# (a & b) | c  ≡  ~((~(a & b)) & ~c) : True
# (a & b) | c  ≡  a & (b | c) : False  反例 a,b,c = (0, 1, 1)
# (a | b) & (a | c)  ≡  a | (b & c) : True

結案 -- 後果與影響#

  • 等價性檢查成為流程標準：每次 synthesis、ECO、retiming 之後自動比對 RTL vs 網表；沒有 LEC 的流程是不完整的。
  • BDD 的遺產：不只驗證——symbolic simulation、可达性分析、甚至早期 SAT 前的 model checking 都靠它。
  • 圖靈獎加持：Clarke、Emerson、Sifakis 因 model checking 獲 2007 年 ACM 圖靈獎，學界承認驗證是一門科學。
  • 理論延續至今：assertion-based verification（SVA）、bounded model checking、property proof、AI 輔助驗證，源頭都在 1981–2001 這條線上。

關鍵人物與文獻#

  • Randal Bryant（CMU）：Ordered BDD 與正則形式, IEEE Trans. Computers, 1986。
  • Edmund Clarke、E. Allen Emerson、Joseph Sifakis：CTL model checking, 1981；2007 年圖靈獎。
  • Kenneth McMillan（CMU→Cadence）：SMV model checker, 1992。
  • Moshe Vardi（Rice）： temporal logic 與 model checking 理論。
  • M. Moskewicz et al., "Chaff: Engineering an Efficient SAT Solver", DAC 2001。
  • Synopsys Formality、Cadence Conformal：等價性檢查 signoff 工具。