Formal验证简单入门
背景
以Cadence家的JasperGold为例简单介绍一下formal工具
核心内容
我的理解
市面上的Formal工具会有些许差别但是主要功能都大差不差，以Cadence家的JasperGold为例，我举几个我个人比较比较常用的APP。
| 形式化属性验证（Formal Property Verification， FPV） | 通过写约束和断言的方式来验证DUT功能的正确性 |
| 设计覆盖率验证（Design Coverage Verification, COV） | 用于生成一组全面的覆盖率数据，需要和其他APP一起使用，也可以和Cadence家的EDA工具生成的覆盖率结合 |
| X态传播检查（X- Propagation Verification， XPOP） | 检查设计中是否有不希望的X态传播 |
| 连接性验证（Connectivity Verification, CONN） | 用于检查信号之间的连接性 |
FPV
FPV应该是Formal工具中最常用的APP，一般会使用TCL脚本来将DUT、assume和assert文件编译到一起，然后用FPV进行证明。
就如我在[[formal验证简介]]中介绍的，FPV就是formal工具将Assume、Assert文件bind到DUT上，然后工具再对暴露出来的input进行随机后检查assert是否准确的验证方式，formal工具会通过遍历input信号组合的方式来检查每一种情况下assert是否成立，成立则输出proven，不成立则输出反例。
当然还有一种undetermined情况，这种情况表示工具虽然进行了遍历，但是可能由于assert的条件不满足的原因，对应的assert并没有得到完全的证明。此时就需要检查你的约束是否合适，是否会导致空间爆炸，又或是你的断言是否太过复杂，导致工具在规定时间内没有检查到信号的变化。
TCL脚本
一般简单的TCL脚本中包含几个关键字
analyze用于解析rtl和env文件，将对应文件“吃”进工具里
elaborate用于解析文件，对DUT中暴露出来的input接口打入随机数。如果DUT中调用了外部的库，需要家-bbox对部分不关注的库进行黑盒处理，如果调用了外部的断言库或者代码需要家宏定义，则需要在elaborate后面加+define+宏定义的形式将宏定义编译进来。
clock用于定义DUT中的时钟
reset用于定义DUT中的复位信号
prove -all 工具进行证明
report 输出证明报告
而后在terminal中输入jg -fpv -tcl xxx.tcl就可以执行tcl脚本，并打开JasperGold的图形化界面。
实战要点
- 工作中可以这么用：尽可能不进行assume约束，而在assert中减少无关input的影响
- 容易踩的坑：assume写得太多，反而过约束，让断言无法得到完整证明
一句话总结
FPV是所有formal app的精华
