FormalVerification(一)形式验证的分类、发展、适用场景

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的🔗验证模块(https://reports.opentitan.org/hw/top_earlgrey/formal/summary.html)。

适合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

Data transport

The growth of Formal

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

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

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

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

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

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

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

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

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

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

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

欢迎加入formal验证讨论群 （小朋友请勿加，formal目前不适合小朋友）

如二维码失效，请加微信：riscv-linux