跳轉到

2005-ABC合成系統#

案件摘要#

BDD（1986）有變數順序的阿基里斯腱、SIS（1986）的 SOP 表示在中等規模就吃緊——合成與驗證各自為政，引擎重複投資。2000 年代中期，UC Berkeley 的 Alan Mishchenko 推出 ABC：以And-Inverter Graph（AIG）為唯一表示——整個電路只用 AND 閘與反相器兩種節點——配上結構雜湊（structural hashing）、SAT sweeping（等價合併）、cut-based 映射：極簡的表示 + SAT 求解器的威力，讓合成、驗證、映射在同一框架裡高速運轉。ABC 成為開源合成/驗證的旗艦，OpenROAD（2019）等開源流程以它為心臟，其「AIG + SAT」的極簡主義重塑了整個邏輯合成的演算法設計。

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

  • BDD 的瓶頸：變數順序敏感（乘法器等函數指數爆炸）、記憶體重；SOP 的指數積項——兩大表示都撐不住大電路。
  • CDCL SAT 就緒（2001）：Chaff 之後 SAT 求解器實務上極快——「AIG + SAT」的組合條件成熟。
  • 工具的重複投資：合成（SIS）、驗證（BDD model checker）、映射（DAGON 系）各有表示與引擎——維護成本高、演算法不能共享。
  • Berkeley 的傳統：Espresso、SIS 的同一實驗室，需要一代新框架接棒——合成研究斷層的焦慮。

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

核心：AIG——極簡的典範#

AIG 只用兩種節點：AND 與 NOT（以邊的補數標記表示）：

f = a·b̄ + c̄·d  →  AIG:
    OR(a, NOT(b), NOT(c), d) → 分解成 AND 樹 + 邊上反相標記
  • 任意布林函數皆可表示（AND + NOT 函數完備）；
  • 結構雜湊（structural hashing）：相同的 AND 子式自動合併——建圖即去重；
  • 固定順序、無需變數排序——BDD 的阿基里斯腱不存在。

SAT sweeping：等價的合併#

兩節點功能等價 ⇒ 合併為一（圖縮小）。Mishchenko 的演算法： 1. 用模擬（simulation）的位並行簽章快速篩出可能等價的節點對（ \(O(n)\) 模擬）； 2. 對候選對，用 SAT 檢查真正等價（在共識框架下證明 \(f_i \oplus f_j = 0\) 不可滿足）； 3. 等價者合併（SAT sweeping）——反覆掃直到圖不再縮小。

\[ \text{模擬篩選（快、可能誤）} + \text{SAT 驗證（準、慢）} = \text{又快又準的等價合併} \]

這個「模擬篩 + SAT 驗」的分工是 sweeping 的靈魂——把 CDCL 的威力嫁接到圖的簡化上。

cut-based 映射與分解#

  • cut 枚舉：每節點的 \(k\) -cut（≤ k 個輸入的錐）動態枚舉——FPGA LUT 映射（ \(k\) =6）與標準單元映射共用框架；
  • DAGON 樹覆蓋的 AIG 版：在 AIG 上做 cut-based mapping，深度/面積雙目標；
  • 分解（technology decomposition）：AIG 轉工藝庫，配 timing-driven 權重。

為什麼贏：表示法最小化的推理#

表示 節點種類 典範性 SAT 相容
SOP（SIS） AND/OR/NOT 積項 無 弱
BDD 變數節點 有（但順序敏感） 間接
AIG AND + 邊反相 結構雜湊即局部典範 直接（CNF 線性轉換）

AIG→CNF 線性轉換（每個 AND 一條 Tseitin 子句），SAT 求解器直接吃——表示法、求解器、驗證三位一體。

結案 -- 後果與影響#

  • 開源合成的旗艦：ABC 成為學界與開源 EDA 的合成/驗證核心，OpenROAD、Yosys（可與 ABC 串接）都以它為引擎——開源晶片流程的基石。
  • 「AIG + SAT」成為新正統：等價檢查、sweeping、映射、驗證共用 AIG 表示——EDA 演算法的表示法之戰以 AIG 暫勝（BDD 退居狀態集合表示）。
  • 合成與驗證合流：同一框架裡做合成與等價檢查——「設計即驗證」的工程實踐，縮短收斂迴圈。
  • Mishchenko 的譜系：從 SIS（Brayton/Rudell）到 ABC（Mishchenko）——Berkeley 合成研究的接力，Espresso 的精神在 AIG 時代以新形態延續。

關鍵人物與文獻#

  • Alan Mishchenko：Berkeley 教授，ABC 作者，AIG 與 SAT sweeping 的集大成者。
  • 文獻：
  • A. Mishchenko, S. Chatterjee, R. Brayton, "DAG-aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis," DAC 2006.
  • A. Mishchenko, S. Chatterjee, R. Brayton, "SAT Sweeping with Local Observability Don't-Cares," ASP-DAC 2006.
  • A. Kuehlmann, F. Krohm, "Equivalence Checking Using Cuts and Heaps," DAC 1995（等價檢查前身）。
  • 工具：ABC repository, UC Berkeley, 2005–（持續維護）。