形式验证：分类、发展与适用场景

形式验证：分类、发展与适用场景

引用

CSDN

1.

https://m.blog.csdn.net/2501_90225825/article/details/145195802

形式验证（Formal Verification）是芯片设计和验证领域的重要技术手段，与传统的动态仿真（Simulation）相比，具有独特的优势和适用场景。本文将详细介绍形式验证的分类、发展历史及其在芯片设计中的应用。

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

形式验证分为两大分支：

• 等价检查（Equivalence Checking）
• 属性检查（Property Checking）

形式验证初次被EDA工具采用，可以追溯到90年代，被应用于RTL代码和门级代码的逻辑等价检查（LEC）。后来，形式验证开始慢慢发展，衍生出适用于不同场景的各类工具。

等价检查

等价检查主要包含以下几种类型：

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

属性检查

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

除了上述两类，CDC的检查也属于静态验证；例如Spyglass会对跨时钟域设计做结构性检查，检查跨时钟域的信号是否经过同步器处理；一般来讲，形式验证属于静态验证。

Simulation VS Formal

• Simulation属于动态验证，Formal属于静态验证；两者是相互补充的验证手段，各有优缺点，在合适的场景采用合适的验证手段，达到最佳的ROI。
• Simulation是time-based的，仿真器依据消耗时间的事件推进仿真的进行，激励需要用户施加；Simulation虽然可以随机化发送激励，但是对于corner case的遍历需要花费大量时间；Simulation适用于大规模的设计，仿真的时间深度可以轻松达到上万个cycle；
• Formal是state-space based的，依据算法探索所有可能的状态空间，不需要平台搭建和输入激励，便于快速启动验证；Formal适用于小模块的验证，随着设计复杂度和cycle深度的增加，formal会占用大量资源，难以收敛；
• Formal适用于40,000 寄存器以内的模块验证（这个数据已经被刷新）；随着设计复杂度的增加，状态空间激增；一个设计包含n个dff，有2^n种配置，m个input有2^m种组合；该设计可能的状态达到2^(n+m)个；对于一个10 input，10 dff的设计，为2^20=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的🔗验证模块。

适合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
• System Deadlock

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;