第5章 驗證演算法#

驗證占晶片設計 60~70% 的工程時間，「設計是對的嗎」遠比「把它做出來」更難。本章介紹三大驗證支柱：模擬與驗證策略（覆蓋率驅動的隨機化）、SAT 求解與 DPLL（完備布林可滿足性的演算法核心）、以及模型檢查（對所有可能行為做窮盡的性質證明）。模擬只能證明「有錯」，模型檢查與形式驗證才能證明「無錯」。三種方法在成本與完備性上互補：模擬便宜但不完備，SAT 完備且實務高效，模型檢查最徹底但面臨狀態爆炸。本章的演算法還有一個共同特色——它們都是第 2~4 章基礎的延伸：SAT 建立在 CNF 與布林推理上，模型檢查的符號引擎用的正是 BDD，而覆蓋率驅動驗證中的約束求解器本質上是小型 SAT/SMT。學完本章，你將掌握現代驗證工具鏈（UVM、MiniSat、NuSMV）背後的演算法本質。