形式验证（Formal Verification）会越来越有用

新的应用推动了对复杂芯片的需求，在这些应用中，复杂的交互和安全风险很难用其他的仿真工具验证。

随着芯片被用于很多关键的应用，芯片内部的交互数量也在增加，形式验证在芯片研发流程中的角色也越来越多。

低功耗设计已经存在了很长时间，之前主要是被移动端芯片采用。现在，我们看到AI/ML加速器中非常关注能效。因此，现在对于每个人来说，无论他们在做什么，低功耗设计都是一个大问题，可以使用形式验证解决其中的一些问题。

如果你正在做时钟门控，我们可以在有和没有时钟门控的情况下进行分析，并明确地告诉你功能是否等价。根据用户要求，还可以通过UPF文件考虑电源意图。

Formal 能够进入这些非常具体的领域，不需要执行全部的仿真回归就可以把这些具体问题解决得一干二净。这才是Formal的真正价值。

Formal在这里是完备的，在上面这个例子中可以完备地保证低功耗不会对功能造成错误。

测试计划中都会有各种各样测试项，其中一些你可以通过形式验证来完备地验证。随着验证空间越来越大，Formal的重要性越能够凸显。

简言之，过去功能较少、仿真可以基本保证覆盖，在今天的许多应用中仿真的效率不可接受的。

高级工艺节点 SoC 和异构封装导致的设计复杂度不断增加，验证需求往往会呈指数级增长。验证工作做了非常多的工作来证明某些特性是正确的，最费时间的就是各种质量活动评审。当我们审视整个IC验证的研发流程，尽管验证作为一个岗位持续了数十年之久，但它并没有跟上复杂性的增加，而这正是形式验证成为重要角色的原因。

验证工作中的很多特性都很难用仿真方法来证明，这反过来又导致了对Formal需求的激增。这是Formal的优势所在，由于其完备性证明的性质，形式验证可以最终证明设计是正确的、安全的或值得信赖的。

如果一颗芯片用在了自动驾驶上，你怎么能够证明你的芯片是安全的？如果Formal能够作为某种认证手段会怎么样？客户会不会更愿意采纳你的IP呢？

在过去十年中，形式验证的应用惊人增长。目前，对于绝大多数顶级半导体公司来说，它是验证武器库中不可或缺的工具。

一个很好的例子是连接性检查，如果使用Simulation，可能需要一步一步地遍历所有连接，这可能需要相当长的仿真时间 。要想提高生产力，我们需要Formal验证，释放出仿真周期，从而在这些仿真周期内做更有价值的事情。

现在的验证思路是基于 IP 的分而治之验证，首先彻底验证 IP 或子系统，然后检查是否正确集成。对于基于 IP 的验证，形式验证已经扩展到对许多（但不是所有）类型的 IP 进行sign off，但状态空间仍然是一个问题。例如，复杂的串行协议对于形式验证仍然具有挑战性 - 时序深度通常太高。

一些形式化技术可以扩展到芯片级，但仅限于一些有限的验证点——大型数字 SoC 的完全Formal signoff仍然太具有挑战性。

每个设计都可以有一个Formal 应用的验证解决方案，尤其是以算术为主的设计此时，传统的仿真方法基本上不可能验证完备。

从理论上，你如何验证设计中不存在什么，例如设计不存在木马，这通常是通过仿真无法解决的验证问题，因为仿真只能证伪，不能够证明。但是Formal真的可以！

但Formal技术也造成了人才短缺，因为在这领域，只有极少数人精通断言和Formal验证工具。很多大厂都已经在实际项目中使用了Formal验证工具并且从Formal验证中收益。更多的是，行业内中有一些人想要了解Formal，但是缺少指引。

Emulation vs. formal vs. simulation

验证流程中主要是Emulation 和Simulation 。有些东西非常适合Formal验证，但不太适合Simulation，反之有些数模混合或者异步设计适合Simulation，而不适合Formal验证。

仿真和Formal验证技术是相辅相成的。在覆盖率方面，通过仿真，你可以很容易地达到80%、85%甚至90%的覆盖率，然后你就会很快达到曲线上的一个另外的95%收敛瓶颈。根据signoff的标准，另外 5% 左右，你可以做再怎么多的随机化，也仍然无法达到这些标准。

这 5% 恰好是Formal验证的甜点，因为 5% 是仿真难以达到的地方，可能是边界场景，也可能是dead code。这个时候，传统的验证流程就会安排一些有经验的工程师介入进行代码review:“我们一直认为这是无法覆盖到的或者风险不大，可以验证交付。” 真的么？？？

上面这种手动干预是不太合适的，低效率的，这个时候可以使用仿真和Formal验证技术，互补验证。

仿真完成基本的验证，由Formal验证完成最后一公里，类似的应用可以有连接性、死锁、安全、低功耗、算法验证和等价性比较验证等等。

Formal的局限性 与所有 EDA 工具一样，Formal工具也有一些局限性。相比完整的SoC，Formal更适合在模块上运行。当涉及到冗长的时序序列时，Formal会面临挑战。

就目前而言，有些验证任务Formal做得很好，有些仿真做得很好。我们永远不会看到Formal完全消除仿真的时候。 就像EDA工具做完综合后以及做完PR后，一直努力避免门级仿真，仅利用等价性比对，但是很多场景还是无法避免。

但是，我们看到Formal验证的应用正在以更快的速度增长。