Formal验证简单入门背景近几年慢慢开始接触到formal形式化验证简单聊聊这是什么了解其环境搭建和适用范围核心内容什么是formal验证验证环境怎么搭什么模块适合用formal进行验证我的理解不同于使用SV和UVM框架的动态仿真formal属于静态验证。静态验证的意思就是formal工具在往接口灌的激励是随机的、不遵循时间进行规律变化的。或者说formal验证过程中没有仿真时间的概念它只在这一刻给接口灌入随机值检查信号是否根据你期望的进行变化。下面是UVM仿真框架和Formal仿真框架可以看到formal的代码量明显小于UVM。仿真开始后formal工具对接口可能的信号变化进行穷举然后检查output或者内部信号是否遵循assert中的行为所以我认为对于formal来讲适合的模块会有以下几种特点1、模块相对较小方便进行穷举2、暴露出的输入口行为变化和想要检查的信号关联性较强当然这并不意味着大型的设计不适合用formal如果想要更加完备地对设计进行验证将大设计拆分成小模块使用formal会更加高效。实战要点工作中可以这么用对于小模块的验证特别是控制类的、协议类的、对信号约束明确的更适合用formal容易踩的坑如果输入信号和检查的信号关联较小则容易出现假pass的情况一句话总结formal是一种用穷举法证明模块没有bug的静态验证方法适合用来验信号约束明确的模块