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