Formal验证简单入门一

Formal验证简单入门

背景

近几年慢慢开始接触到formal形式化验证，简单聊聊这是什么，了解其环境搭建和适用范围

核心内容

1. 什么是formal验证
2. 验证环境怎么搭
3. 什么模块适合用formal进行验证

我的理解

不同于使用SV和UVM框架的动态仿真，formal属于静态验证。静态验证的意思就是formal工具在往接口灌的激励是随机的、不遵循时间进行规律变化的。或者说formal验证过程中没有仿真时间的概念，它只在这一刻给接口灌入随机值，检查信号是否根据你期望的进行变化。

下面是UVM仿真框架和Formal仿真框架，可以看到formal的代码量明显小于UVM。

仿真开始后formal工具对接口可能的信号变化进行穷举，然后检查output或者内部信号是否遵循assert中的行为，所以我认为对于formal来讲适合的模块会有以下几种特点：

1、模块相对较小，方便进行穷举；
2、暴露出的输入口行为变化和想要检查的信号关联性较强；

当然这并不意味着大型的设计不适合用formal，如果想要更加完备地对设计进行验证，将大设计拆分成小模块使用formal会更加高效。

实战要点

• 工作中可以这么用：对于小模块的验证，特别是控制类的、协议类的、对信号约束明确的更适合用formal
• 容易踩的坑：如果输入信号和检查的信号关联较小，则容易出现假pass的情况

一句话总结

formal是一种用穷举法证明模块没有bug的静态验证方法，适合用来验信号约束明确的模块