让你无法拒绝Formal验证的4个理由

在讨论Formal验证相比传统动态仿真验证的优势之前，让我们先确认一个共识：

动态仿真、硬件加速或者其他的一些验证流程只能“证伪”，而不能“证明”。真正完备的验证应该对设计进行严谨地数学分析，从原理上对进行证明。

后者就是我们所说的形式验证（Formal Verification，FV）。（

Note0：这里的形式验证，主要指的是模型验证，而非大多数人所知的等价性验证。

Note1：Formal也有很多缺点，所以现在Formal还不如动态仿真验证普及。具体是哪些缺点需要各位自行体会了，Formal和动态仿真相结合才能发挥出验证人员最大的潜力。

Formal验证的优势包括：

•解决真正的验证问题：对于面向实际工程问题的验证人员，验证方面的数学分析也许太过理论和不切合实际。但是如果你尝试问下自己：我们究竟该如何验证或者说保证设计的正确性？大多数人还是会说，理想情况只能在数学上验证设计符合规格，而不是使用随机激励覆盖那些人为提取的测试点。不幸的是，由于当前EDA工具的缺憾，我们还是主要采纳后者的验证方式。相信随着工具的升级，我们会越来越多地采纳形式验证对RTL，甚至更High level的设计进行验证，以降低在后期验证发现BUG带来的DEBUG成本。

•完全覆盖：覆盖率（coverage）是指已经验证通过的测试点占全部测试点的比例，本质上FV会提供完全的覆盖（如果你的功能覆盖率文件没有写错的话）。这些需要覆盖的测试点在动态仿真上我们可能需要进行等价，只收集其中的一部分，并且要花费数十倍于FV的时间成本。由于设计规模和工具算力的限制，对chip level进行Formal验证几乎是不可能的，但是在符合规格的输入约束条件下，可以对某些关键模块进行block level的Formal验证，这相当于对该模块进行“指数级”的动态仿真，能够提高验证的完备性和验证交付信心。

•设计行为最小示例：大多数FV引擎都能够生成设计行为的最小示例。如果Formal验证失败，会展示出发生BUG的数个周期内的设计行为，但是在典型的随机动态仿真环境中可能需要追溯到数千个周期前才能定位到问题所在（如果问题所在处没有断言），从而使得Formal验证的调试和问题定位非常容易。

•边界（Corner）场景：在FV的引擎中，工具会遍历用户尚未禁止的所有场景，这意味着形式验证能够发现很多用户都不会识别出来的边界场景。而在动态仿真中，验证工程师需要输入有限的激励，这会导致这些边界场景无法得到完备的验证，即发生漏测。究其根本，是因为动态仿真只指定有限的合理约束，而Formal验证只需要验证人员指定有限的错误约束。相比前者，后者更容易做到。