IC形式化验证FPV

Formal Verification的应用

1 Introduction

Tool: JasperGold (cadence/JASPER/2021.03)
Formal Verify :适用与DUT规模较小的，在接口处打上随机的激励，只需要给予约束，非常适合快速验证； 不适合跑性能；但非常适合应用于BT级的功能验证；
最大的区别：不用构造激励，不用大量仿真时间；原理：assertion check；assertion check的组合来等价DUT的功能；
UVM dynamic Verify:定向的编写case；前期搭平台和调试平台时间较长，前期根据测试点来写定向case；

2 Body

2.1 how to use

1.先创建一个运行perl脚本，进而以后执行perl脚本；
----也可根据Cadence 的Demo来修改；
2.填写filelist.f文件
3.Generate
a.binding 文件：自动识别接口将SVA文件和DUT进行绑定；
b.SVA 文件：整个SVA的框架、接口生成好，只需在里面填充assertion即可；
c.TCL 文件：pre.tcl和post.tcl两种；

在SVA中添加assertion后，重新仿真只需再加载pre.tcl和post.tcl

2.2 whether use Formal or not

在开发assertion之前，首先进行一下DUT规模分析，看DUT是否符合FV验证的条件；
1。DUT规模逻辑门一般不超过10M；在JasperGold页面Console命令窗口中敲get_design_info指令来获取DUT的逻辑门数量；
2。DUT功能分析：一般是控制逻辑功能，算法类不建议；
3。DUT是否含有加密IP代码（若有，则无法使用）；

2.3 SVA commoin Key words

1.Assume
–假定一些条件，作约束用。these condition will always be True in simulation;
–example: ass_rx_factor:assume property(@(posedge mc_clk)) (rx_factor>0)
在读三拍期间，约束不打激励；
2.Assertion
–是一种描述，期望输出的某些属性一直为真；
–Key:assert
–Example: ast_is: assert(a&&b)

3.coverage
–代码覆盖率和功能覆盖率；—》检测属性计算的覆盖范围；
–Keywords:cover/covergroup
–Example:

2.4 覆盖率收集

2.4.1 功能覆盖率

编写功能覆盖率文件，放在tcl脚本 analyze一下，跑仿真的时候会自动收集功能覆盖率；

2.4.2 覆盖率收集指令

编写全部asserttion后，进行覆盖率收集；
branch code FSM toggle…

2.4.3 覆盖率merge

1.有不同的SVA文件，且SVA文件之间具有相同的assume，就可以放在同一tcl里面收集；
2. 若不同的SVA文件中有互斥的assume，则需要配置不同的tcl；tcl和SVA是配套的；
3.如何Merge各个覆盖率文件：

2.5 TCL 关键字分析

2.5.1 Analyze:读取design和property文件，检查语法错误；

2.5.2 Elaborate：指定synthesize和build的设计顶层；

2.5.3 Black-boxing:z 去掉内部逻辑，只保留接口；black-box模块的输出将不受驱动；

目的：为了更好的性能或者周围有不可综合代码；

2.5.4 Stopat(Cutpoint) 切断网的方法，使其不受驱动；

stopat命令可以切断设计中的任何网络或者总线；
Note：stopat切断某个信号时，信号接口上会没有值，没有驱动，单纯使用会改变DUT的逻辑，常常搭配assume来进行固定赋值；

2.5.5 Assume

有时候约束一些管家或者寄存器来作为设置；

2.5.6 clock:使用命令时钟来申明一个信号为时钟

2.5.7 Reset:使用reset命令配置设计初始化

2.6 不用脚本运行

tcl demo；
在tcl中自己指定好相关文件；

3 形式化验证FPV验证介绍（进一步）

这个完全可以在搭建UVM 验证平台之前 花费2天时间进行搭建Formal Verification
Core：形式验证相当于采用穷举法，对约束空间的所有可能进行穷举；形式验证的优点在于不用搭建验证平台，直接写assertion，大大缩短时间；

形式验证：针对设计spec中的状态、功能逻辑等，采用断言区描述设计spec，最后通过断言去check是否与RTL code等价性；

3.1 SVA code

Concurrent assertion:
immdiate assertion:

层次：建立序列sequence–》建立属性property–》断言声明assume assert cover；
Assume：假设某些属性为真，约束某些属性；
Assert: 断言属性结果；
Cover:覆盖属性，衡量覆盖率结果；
label:assert/cover/assume property(xxx);

蕴含运算符；
a |-> b;
a |=> b;
Sequence：
a ##1 b
a ##[2:3] b
a ##[4:$] b
a [*5] //连续5拍拉高；
$past() $rose() $fell(d);

流程：
spec分析–》code SVA–》设置时钟 复位信号；–运行TCL脚本–》设计代码与断言代码映射 工具检查—》要么修改RTL code 要么修正断言—Coverage 分析；

3.2 项目目录结构

project
–properties
-----xxx.sv
-----xxx.sv
–script
----dut.tcl
----sva.tcl
—filelist.f
—parameters.vh
–sim
-----Makefile
–wave
------xxx.fsdb

3.3 Formal VO getup

主要是编写Assumption和Assertion；

3.4 运行结果分析

设计代码《–》属性描述 反例–》波形；
思考点：
模块接口与外部交互的检查；业务数据通路检查；–》设计代码bug复现；

基于Spec文档，采用SVA描述设计属性特征，通过JasperGold工具证明RTL code与Spec等价性
可将对标准协议的断言检查封装为断言属性库，方便不同项目之间的使用