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