本发明公开了一种Chisel断言语言的类SVA扩展及形式化验证方法，其步骤包括：1)将SVA支持的若干算子引入Chisel断言语言中，得到断言语言中对应的扩展算子；2)接收用户编写的算子序列；3)将Chisel硬件设计代码编译成FIRRTL，并利用FIRRTL生成设计代码的迁移系统；4)在FIRRTL层次生成相应的Büchi自动机；5)将结构调整后的自动机翻译到FIRRTL的迁移系统上，得到断言转换后的迁移系统；6)将转换后的迁移系统与硬件设计对应的迁移系统做同步得到一全局迁移系统；7)根据全局迁移系统生成btor2文件；8)对btor2文件进行模型检测，完成对断言所描述性质的形式化验证。