1986-BDD二元決策圖#

案件摘要#

布林函數的表示是一場戰爭：真值表 \(2^n\) 行、SOP 積項指數——每種表示都撐不住大電路，且「兩個電路是否等價」這個驗證核心問題遲遲無高效解。1986 年，CMU 的 Randal Bryant 在《IEEE Trans. Computers》發表 BDD（二元決策圖）論文：規定變數順序、合併同構子圖、刪除冗餘節點——得到一個典範（canonical）表示：同一函數的 BDD 唯一，因此等價檢查 = 指標比較， \(O(1)\) ！加上高效的 Apply 運算子，BDD 讓百萬閘電路的等價檢查、符號模擬、模型檢查第一次可行。這是 EDA 驗證革命（1990 符號模型檢查）的數學地基，也是 Bryant 獲 1998 ACM Turing 時代前最重要的一篇 EDA 論文之一。

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

驗證是瓶頸：1980 年代設計規模達數萬閘，模擬驗證（向量 + 模擬器）覆蓋率無法窮盡——「證明等價」是夢想。
表示法的混亂：真值表 \(O(2^n)\) 、SOP/DNF 指數、電路圖非典範（同一函數多種畫法）——沒有一種表示兼顧緊湊與唯一。
決策圖的先例：Shannon 展開（1938）的遞迴分解、Lee（1959）的二元決策程式、Akers（1978）的 binary decision diagrams 雛形——概念已存在，缺「典範化」的關鍵一步。
CMU 的現場：Bryan? （Bryant）研究符號模擬與 MOS 電路驗證，需要能操作「整個輸入空間」的表示法。

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

核心：三條規則鑄成典範#

以固定變數順序 \(\pi\) ，用 Shannon 展開遞迴建樹：

\[ f = \bar{x}_i \cdot f|_{x_i=0} + x_i \cdot f|_{x_i=1} \]

樹會指數爆；Bryant 的三條化簡規則把它壓成 DAG： 1. 冗餘測試：若 \(f|_{x_i=0} = f|_{x_i=1}\) ，刪除該節點（函數不依賴 \(x_i\) ）； 2. 同構合併：相同子函數的節點只留一個（hash-consing 唯一化）； 3. 順序固定：所有節點沿 \(\pi\) 遞增。

結果：每個布林函數的 ROBDD（約化有序 BDD）唯一——典範性（canonicity）：

\[ f = g \iff \text{ROBDD}(f) = \text{ROBDD}(g) \iff \text{根指標相同} \]

等價檢查從指數級的 SAT 化為 \(O(1)\) 指標比較——這是驗證的奇蹟時刻。

Apply：布林運算在 DAG 上#

兩 BDD 的 AND/OR/XOR 用記憶化遞迴（memoization）在 DAG 上做：

\[ f \otimes g = \begin{cases} \text{端點直接算} & \text{若一方是常數} \\ \text{對較小序變數展開：} (\bar{x} \otimes f_0 g_0,\ x \otimes f_1 g_1) & \text{否則} \end{cases} \]

複雜度 \(O(|BDD(f)| \cdot |BDD(g)|)\) ——雖然最壞指數（乘法器函數是 BDD 的天敵），但控制邏輯實務上極為緊湊（萬閘電路常僅數千節點）。

變數順序：BDD 的阿基里斯腱#

同函數不同順序，BDD 大小可差指數倍（如 \(f = x_1 y_1 + x_2 y_2 + \cdots\) ）——變數排序本身 NP-hard，實務用動態重排（sifting, Rudell 1993）。這個弱點最終由 AIG/SAT（2005 案）接手補位。

結案 -- 後果與影響#

符號模型檢查的燃料：Burch-Clarke-McMillan（1990）把 CTL 模型檢查的狀態集合用 BDD 表示——工業級驗證自此可行，2007 年 Clarke 等獲 Turing 獎。
等價檢查成為流程必備：合成前後、版圖前後的等價性（LEC）工具全部以 BDD/其後繼為引擎——今日驗證流程的心臟之一。
學科的合流：BDD 把 Shannon 展開（1938）、圖論（DAG）、動態規劃（Apply 的記憶化）鑄成一體——EDA 驗證自此有了嚴格的數學基礎。
Bryant 的雙程：BDD（1986）之後，Bryant 又是形式驗證理論與 model checking 的持續推手，2007 年與 Clarke、Emerson、Sifakis 同獲 Turing 級認可（Clarke/Emerson/Sifakis 獲獎；Bryant 獲 1998 ACM Kanellakis 獎）。

關鍵人物與文獻#

Randal E. Bryant：CMU 教授，BDD 典範化之父，後為 ACM/IEEE 雙會士、DARPA 計畫推手。
文獻：
R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers C-35, 677 (1986).
S. B. Akers, "Binary Decision Diagrams," IEEE Trans. Computers C-27, 509 (1978)（前身）。
R. L. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," ICCAD 1993（sifting 重排）。