Formal verification的优势在哪里？
首先我们应该都有一个共识：
在数学上穷尽分析所有可能的RTL空间是最理想的验证结果，这也是传统的仿真很难做到的事情。
FPV方法的优点包括：
做正确的验证
这句话可能比较哲学哈。
以一个工程师的角度，你是否问了自己很多次：我们应该如何正在验证我们的设计？
理想的方法是从数学上证明它们符合其规格。但不幸的是，由于工具的限制，我们大多基于仿真的方式来进行验证。这是工程中上市时间和技术水平对我们的约束，
随着这些限制的减少，我们应该尽可能地摆脱这些旧的方法（仿真）或者尝试选择FPV方式进行一些验证。
完全覆盖
如果我们将“coverage”定义为我们对设计分析的空间与设计全空间的比值，FV本质上能够提供完全的覆盖。完全的FV对于大规模的设计是不太现实的，但是FV方法仍然能够达到非常多次仿真回归的效果。
最小的场景示例
大多数FV引擎能够产生最小的场景（RTL行为），这些数个周期内的行为可能要在数千个随机仿真环境中才能复现，这使得FV更容易定位问题。
边界场景（Corner Cases）
FV会遍历任何没有约束掉的行为，这意味着FV工具很容易发现有趣的Corner Cases（头脑风暴也很难想到的场景）。对这个场景进行分析，可以检查我们的EDA验证环境是否不够完备，是否在某个地方（激励、参考模型和检查机制）存在着过约。
基于State-Driven和Output-Driven的分析
FV可以cover设计内部的任何状态，设计可以根据这个cover分析产生这个状态的相关设计行为。仿真是激励驱动的，通常覆盖到某个特定的复杂设计场景都会比较困难。
证明永恒的问题（Infinite Behaviors ）
如果使用仿真，你如何能够证明设计永远不会到达某些状态。用FV，数学的推理力量，我们就可以回答这个问题。
Formal Verification能用来做什么？
基于前文所述Formal Verification的优势，可以诞生多个FV的应用场景。
complete coverage，确保所有可能的场景都被覆盖到，以提高验证交付自信，防止出现Intel 奔腾FDIV bug等类型的问题。
bug hunting，当设计规模较大时，可以针对设计特定的风险区域进行更加全面的覆盖测试（注意，前提是无法做到Full proof,不然就没有bug hunting的必要了）
design exploration，利用数学分析可以帮助我们更好地理解RTL行为。
FV FOR COMPLETE COVERAGE
为了进一步了解FV方法，先让我们花点时间来考虑一个简单的验证问题：
验证一个有两个32位输入的加法器。
为了充分验证该设计的所有可能的输入，我们需要仿真264种可能的组合。如果你有一个超快速的仿真器和服务器资源，可以每秒仿真214个周期（已经非常快了），这意味着它将花费你2*40秒（数万年）的时间来检查所有可能的值。
就算验证经理分给你这么久的时间，可能我们这颗蓝色星球也等不起你验完啊。而且，这仅仅只是测试了一拍的设计行为，还没有考虑时序场景。因此，基于完全覆盖这个需求，相比EDA仿真，FV是我们真正需要的。
01 TIP 1.1
当你想要获得设计行为的完全覆盖时，请考虑使用FV作为主要验证方法。
FV for Bug Hunting
对于一些规模比较大的设计，FV完全覆盖是不太可能的。这才有了EDA 仿真技术的用武之地啊~
当设计规模比较大，或者逻辑比较复杂时，无法做到Formal Full proof。在这些情况下，FV不能完全替换仿真。但这不意味，FV已经没有用了，FV仍然能够验证到比仿真方法多很多的设计状态。
因此，作为仿真的补充，FV仍然可以作为一种有价值的验证方法，否则可能会遗漏潜在bug。
01 TIP 1.2
当你有一个具有复杂逻辑的设计，无法做到Formal Proof时，可以考虑将Formal 作为仿真的补充。
FV for Exploring Designs
FV的另一个主要用途是作为探索RTL设计行为的工具。FV工具能够分析所有的设计空间，然后找出一个示例让设计查看特定的设计行为。
这可以看作是逆向仿真：当你不知道什么样的激励能够产生特定的场景，可以让FV跑出这个场景再去分析。例如，你希望覆盖输出32‘hffff_ffff，但是不知道应该输入什么样的激励，这时候FV可以帮到你。
有时候一个特定的输出是多个周期输入耦合作用的结果，可能只有FV能够找出一个精确的输入序列。
换句话说，使用FV用作设计探索时，我们只要指定的是目的地，而仿真需要你指定旅程中的每一个脚印。
01 TIP 1.3
你可以轻松地指定感兴趣的设计状态或输出，然后使用FV帮你找到特定的输入序列。
Formal Verification在真实项目中的应用
上图是SOC设计流程中Formal Verfication的一些应用，主要包括：
基于断言的验证(ABV)
如今断言已经非常广泛地应用到芯片研发流程中了，例如使用SVA来描述设计的属性（properties ）。在某些情况下，仅仅使用属性也可以描述一个设计的全部规格。使用ABV并不意味着正在执行Formal Verification，因为断言也可以在仿真中进行检查。
事实上，在仿真中检查断言是断言的最主要应用。
Formal Property Verification (FPV)
这是指使用formal 工具来证明断言。FPV是一种非常通用的技术，可以进一步发展再细分为许多额外的技术：
2.1 Full Proof FPV。
这是经典的使用FPV来代替仿真,验证RTL是否正确地实现了规格。
2.2 Bug Hunting FPV。
这是指使用FPV来作为仿真的补充，在Formal无法彻底验证设计的情况下。它仍然是一种非常强大的验证手段，发现corner-case bug并覆盖比仿真更多的设计空间。
2.3 Unreachable Coverage Elimination。
如果你最主要的验证方法是仿真时，通常会在项目中会有一些代码覆盖率永远无法达到，需要验证团队弄清楚它们是否是dead code。FPV可以用来达到这个目的，方便代码覆盖率waive。
2.4 Specialized FPV Apps。
这是指适用于特定设计属性的FPV，如验证寄存器、状态机、连接等等，主要目的就是使用FPV提高某个特性的验证效率。
Formal Equivalence Verification (FEV)
这是指使用formal 比较两个模型并确定它们是否等价的技术。比较的模型可能都是高级语言模型、RTL或网表等等。高级语言FEV可以比较C算法模型和Verilog，RTL2RTL、RTL2NETLIST、NETLIST2NETLIST在后端流程（例如ECO时）中用的比较多。
作者：验证哥布林
原文链接：https://mp.weixin.qq.com/s/gH0P9_dmuKdv91oEyI7JbQ
https://mp.weixin.qq.com/s/G_bSoe2-9qsU762noU7s4Q
https://mp.weixin.qq.com/s/xBWoRwKBbv7Z0QWxcGSjKg
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
