Formal Verification：形式验证的分类、发展、适用场景

Definition

Formal Verification：利用数学分析的方法，通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。

Kinds of Formal Verification

相比于动态仿真Simulation Veficiation，形式验证属于Static Verification，不需要手动灌入激励；通过数学分析的方式，对待测设计进行检查；

在这里插入图片描述

形式验证分为两大分支：Equivalence Checking等价检查 和Property Checking属性检查 形式验证初次被EDA工具采用，可以追溯到90年代，被应用于RTL code和gate level code的LEC等价检查；后来形式验证开始慢慢发展，衍生出适用于不同场景的各类工具；

Equivalence Checking

Combinational equivalence：用于RTL vs Netlist的检查，检查寄存器之间的组合逻辑在综合前后是否一致，如Formality，Conformal。Sequential Equivalence: 用于RTL vs RTL的检查，基于cycle的精确度；适用于对原有block级RTL做了非逻辑修改，如Clock/power gating，对修改后的RTL进行等价检查。Transaction Equivalence：用于C/C++ model VS RTL的检查，基于transaction的精确度；常用于数据通路的算法类设计。

Property Checking

属性检查基于PSL/SVA Assertion Languages，通过对property的assume,cover,assert语句分析，建立golden模型。FPV(Formal Property Verification)需要用户直接书写property；从FPV衍生出各类APP，适用于不同场景，可以根据相关配置，自动生成对应的property。

除了上述两类，CDC的检查也属于static verification；例如Spyglass会对跨时钟域设计做structural 结构上的检查，检查跨时钟域的信号是否经过同步器处理；一般来讲，formal verification属于static verification;

Simulation VS Formal

Simulation属于Dynamic Verification，Formal属于Static Verification；两者是相互补充的验证手段，各有优缺点，在合适的场景采用合适的验证手段，达到最佳的ROI。

在这里插入图片描述

Simulation是time-based的，仿真器依据消耗时间的事件推进仿真的进行，激励需要用户施加；Simulation虽然可以随机化发送激励，但是对于corner case的遍历需要花费大量时间；Simulation适用于大规模的设计，仿真的时间深度可以轻松达到上万个cycle；

Formal是state-space based的，依据算法探索所有可能的状态空间，不需要平台搭建和输入激励，便于快速启动验证；Formal适用于小模块的验证，随着设计复杂度和cycle深度的增加，formal会占用大量资源，难以收敛；

Formal适用于40,000 寄存器以内的模块验证（这个数据已经被刷新）；随着设计复杂度的增加，state space explosion，状态空间激增；一个设计包含n个dff，有2n种配置，m个input有2m种组合；该设计可能的状态达到2(n+m)个；对于一个10 input，10 dff的设计，为220=1,048,576。

回到开头所说的，Simulation和Formal是相互补充的；模块中的assertion语句既可以在Formal中使用，也可以在Simulation中使用；Formal产生的覆盖率也可以merge到Simulation的覆盖率中；设计人员可以通过Formal免于平台的搭建，快速地跑通IP中的一些模块，再hand-off给验证人员使用Simulation sign-off（Shift-Left）；Simulation中的corner scenario，可以通过Bug hunting FPV补充验证；

Formal do better

不同的验证策略适合不同的验证场景；Emulation适用于整个Chip级的验证，加速仿真速度；UVM-Simulation适用于复杂寄存器配置的传输packet的IP验证，便于提取transaction和随机化验证；Formal（FPV）适合相对较小的模块，便于收敛；Formal适合controllable的模块，例如FSMs；Formal适合observable的模块，便于assertion的书写，如AXI bus；串行bus则不适合使用formal。开源项目Opentitan中使用FPV的验证模块^[2]。

适合Formal的常见模块如下：

• •Arbiter、Scheduler

• •FIFO 、FSMs

• •Interrupt controller、DMA controller、Memory controller

• •Power manager unit、Clock programing unit

• •Bus、Bus bridge、Bus Fabric (CrossBar NoC etc)

• •Cache，Cache-Coherent Protocols modeling and verification

• •Data transport

• •Pinmux, Clock Controller, Reset Controller

The growth of Formal

Formal Property Verification相关的工具也有十几年历史了，但由于其限制，Formal Tool并没有被用户广泛使用。但最近这些年，一些因素推动了formal的高速发展：

1. 1. 之前繁多的语言（Vera，'e'，摩托罗拉的CBV和英特尔的ForSpec）整合为SystemVerilog Assertion，并加入IEEE 1800协议，成为标准化的Assertion Languages。工程师在Simulation中广泛使用SVA，节省了在Formal上的学习成本。

2. 2. 随着工艺节点的缩小，流程成本大幅提高；对于corner scenario下可能会隐藏的bug，工程师更倾向Fromal这类exhaustive的验证手段。

3. 3. Formal可以很好的匹配Simulation；同一家EDA的Formal和Simulation工具相互打通，Formal产生coverage可以和Simulation的coverage相互merge，Formal产生的波形可以在Simulaiton上复现，Formal和Simulaiton相同的GUI Debug工具等。

4. 4. 各类Formal APPs的推出，使得Formal更容易掌握和部署。

5. 5. 随着企业服务器性能的提升和Formal算法的发展，可以处理更复杂的设计规模。

6. 6. 一些基于C/C++ model的包含大量运算单元的硬件产品，如AI/ML，GPU的需要爆发，推动了Formal Data Path Validation；

7. 7. Automotive Chip需求激增及其高可靠性的要求，Formal提供safety fault analysis的功能；

8. 8. 芯片对Security的要求越来越高，需要穷尽分析所有访问路径，适合采用Formal；

9. 9. 移动端芯片对于Lower Power的重视；PMU模块适合formal验证；

10. 10.采用敏捷开发的芯片团队，对于"shift left"的追求，采用formal快速进行模块验证及早发现bug;

审核编辑 ：李倩