
王亮 譚永亮
本書系統介紹了形式化驗證的概念和原理,並通過豐富的實例生動展示了形式化驗證所需的TCL和SVA語言語法規則,同時揭示了其在商業上的潛在價值和廣闊前景。書中以目前廣泛採用的RISC-V架構爲例,藉助新思科技的VC Formal形式化驗證工具,深入淺出地講解了各種形式化驗證應用的流程、使用方法以及常見陷阱,爲讀者提供了從基礎知識到高級應用的學習途徑。 本書包括三個部分: ? 基礎篇(第1~6章),主要介紹形式化驗證的工具、語言和設計; ? 實戰篇(第7~13章),主要展示相關工具的使用方法、常見問題以及對應的解決方案; ? 進階篇(第14~17章),主要探討簡化、籤核和加速等關鍵形式化驗證技術。 本書不僅適合芯片設計和開發領域的從業人員快速入門和實踐形式化驗證,也可以作爲電子工程等相關專業的教學參考書。