第6章 邏輯等效性與等價檢查#

晶片在設計流程中會被反覆轉換：RTL → 邏輯合成 → 掃描鏈插入 → 時脈樹合成 → 優化重寫。每一步都可能引入錯誤，因此「轉換前後功能是否相同」的等價檢查（Equivalence Checking, EC）是每次轉換後的必經關卡。本章從組合等效性（兩電路對所有輸入組合輸出相同）講起，介紹以 BDD 與 SAT 為引擎的檢查方法，最後觸及順序等效性（含狀態機的時序等價）這個更難的問題。等效檢查的演算法骨架「miter 構造 + 不可滿足性證明」是形式方法的入門典範：它把一個看似要窮舉 2ⁿ 的問題，轉化成結構比對、隨機模擬快篩與 SAT 嚴格證明的多層漏斗。這個漏斗式設計思想，也會在第 8 章的繞線流程中再次出現。