本書系統(tǒng)地介紹了形式化驗證的概念和原理，通過豐富的實例生動地展示了形式化驗證所需的TCL和SVA語言語法規(guī)則。書中以目前廣泛采用的RISC-V架構(gòu)為例，借助新思科技的VCFormal形式化驗證工具，全面展示了該工具中常用應用的使用方法、常見問題及其解決方案，為讀者提供了從基礎知識到高級應用的學習途徑，幫助廣大的IC工程師和學生快速入門和實踐形式化驗證。