跳轉到

1990-符號模型檢查#

案件摘要#

「這個晶片永遠不會死鎖」——這樣的證明，模擬永遠給不出（模擬只能試有限向量）。CTL 模型檢查（Clarke-Emerson-Sifakis, 1981）能形式化驗證性質，但狀態集合顯式枚舉在 \(10^{20}\) 個狀態前崩潰。1990 年，CMU 的 J. R. Burch、Edmund Clarke、Ken McMillan 與史丹佛的 David Dill 發表符號模型檢查：用 BDD（1986）表示整個狀態集合與轉移關係，不動點（fixpoint）計算在 BDD 上進行——狀態數 \(10^{20}\) 的電路，BDD 只需數萬節點。這是形式驗證從玩具變工業的分水嶺：2007 年 Clarke、Emerson、Sifakis 以此獲 Turing 獎，今日所有 model checker（SMV、NuSMV）與工業級驗證引擎皆其後裔。

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

  • 模擬的哲學極限：模擬 = 有限樣本採樣；「永遠不會」與「存在一條路徑使」是全稱/存在量詞問題——樣本法原則上無法證明。
  • 顯式模型的爆炸： \(n\) 個鎖存器的電路有 \(2^n\) 狀態； \(n = 100\) 就超過宇宙原子數——顯式枚舉不可行。
  • CTL 語言就緒（1981）：Clarke-Emerson-Sifakis 的分支時序邏輯 + 模型檢查演算法，語意與演算法已定，缺可規模化的表示法。
  • BDD 就緒（1986）：Bryant 的典範布林表示——兩塊積木分別完成，1990 年合流。

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

核心：狀態集合 = 布林函數#

把 \(n\) 位元的狀態空間編碼為布林函數：狀態集合 \(S \subseteq \{0,1\}^n\) 表示為特徵函數 \(\chi_S : \{0,1\}^n \to \{0,1\}\) ，轉移關係 \(T(s, s')\) 同樣是布林函數——兩者用 BDD 表示：

\[ |\text{顯式狀態}| = 2^n \quad \longrightarrow \quad |\text{BDD 節點}| \approx \text{數千（控制電路）} \]

不動點：CTL 的符號計算#

CTL 公式的滿足集用不動點（least/greatest fixpoint）計算：

  • 安全性 \(AG\,p\) （永遠 p）：最大不動點
\[ \nu Z.\ p \wedge \text{pre}(Z), \quad \text{pre}(Z) = \{s : \forall s', T(s,s') \Rightarrow s' \in Z\} \]
  • 可達性 \(EF\,p\) （可能到達 p）：最小不動點
\[ \mu Z.\ p \vee \text{EX}(Z), \quad \text{EX}(Z) = \{s : \exists s', T(s,s') \wedge s' \in Z\} \]

每次迭代是 BDD 上的布林運算（Apply），收斂即驗證完成。推理：指數個狀態的集合運算被壓縮成 BDD 的布林運算——與 STA 把指數路徑壓縮成線性掃描（1982）同一數學精神。

界界模型檢查（BMC, 1999）：BDD 的對照組#

Biere、Clarke 等（1999）提出 bounded model checking：只查 \(k\) 步內的反例，編成 CNF-SAT 交給 SAT 求解器（Chaff, 2001）——BDD 慢但完備，SAT 快但界內。兩者互補，構成今日形式驗證的雙引擎。

結案 -- 後果與影響#

  • 形式驗證工業化：SMV（McMillan, 1992）及其工業化後代（IBM RuleBase、Cadence FormalCheck）成為工業標準——設計者第一次可以「證明」而非「測試」。
  • Turing 獎（2007）：Clarke、Emerson、Sifakis 以模型檢查獲獎——EDA 演算法直接誕生的 Turing 級成果。
  • 數學的合流：BDD（1986）+ 不動點理論（Dana Scott 的模態 mu-calculus）+ 自動機理論在此案合流——EDA 理論的黃金時刻。
  • 與 SAT 的雙引擎：BMC（1999）+ CDCL SAT（2001）之後，BDD-based 與 SAT-based 驗證互補分工，今日 IC3/PDR（2011）等演算法繼續推進。

關鍵人物與文獻#

  • Edmund M. Clarke（1945–2020）：CMU，CTL 模型檢查與符號化，2007 Turing 獎。
  • Kenneth L. McMillan：CMU 博士生，SMV 作者，後為 Cadence/Arm 研究員，IC3/PDR 發明者之一。
  • 文獻：
  • J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, "Sequential Circuit Verification Using Symbolic Model Checking," DAC 1990.
  • E. M. Clarke, E. A. Emerson, A. P. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," ACM TOPLAS 8, 244 (1986)（CTL 基礎）。
  • A. Biere et al., "Bounded Model Checking," CAV 1999.