By definition, formal verification is the use of tools that mathematically analyze the space of possible behaviors of a design, rather than computing results for particular values.

形式验证在IC flow有两种常用的看起来相差甚多的领域：

• 模型检查（model checking）：检查RTL是否满足设计规范，典型产品如JasperGold
• 等价性检查（equivalence checking）：检查两个design是否等价，可以是RTL和RTL之间、RTL和netlist之间或者两个netlist之间，典型产品如Synopsys的formality和Cadence的Conformal LEC

既然都是形式验证的范畴，那必然会有一些共性的东西。它们的背后都有一系列数学工具在支撑，比如binary decision diagrams。从理解角度，不严格地考虑，二者都是力求遍历所有可能的输入，来检查对应的输出是否满足目标。当然，实际实现上不可能简单实用穷举，EDA工具都有很多数学模型可以使用，以解决各类问题。比如对于一个加法器，如何进行model checking和equivalence checking？如果穷举那效率太低了，我们可以根据design使用诸如AIG（and-inv graph）等手段把function抽取出来，和model或其他design进行比较。

其实formality和Conformal LEC只涵盖了等价性检查的一方面（CEC），equivalence checking还有一种更强大的手段：SEC，只是这个手段在IC flow中并未普及。这方面的工具有Cadence旗下的JasperGold SEC和和Mentor的SEC工具Questa SLEC。

RTL的function的形式验证除了model checking，还有一种手段是定理证明（Theorem proving），对纯计算逻辑会比较有用。

1. Model checking

Formal verification, in contrast to testing, uses rigorous mathematical reasoning to show that a design meets all or parts of its specification.

提到形式验证的model checking，绕不开和传统的仿真验证方式的比较。仿真验证依靠施加各种类型的激励，以尽量高的覆盖我们想验证的逻辑功能。这种方法自然coverage很难达到100%，而形式验证理论上是可以达到100% coverage的。

那model是怎么来的呢？model是根据design specification写出来的，具体形式可以是用形如SVA表达的ssertion集合（当然还有其他的表达工具）。

本质上讲，model checking的工具使用各种数学手段来试图证明你的design能完全match你写的assertion，如果不能，那么就是找到bug了。当然了，根据specification写出assertion也是一个挑战。

Model checking在IC flow中是对simulation方式的一个补充，使用的流行度无法和基于UVM的simulation相比。

2. Theorem proving

Theorem proving也是一种验证RTL功能和model是否match的手段。顾名思义，它使用的是推导的方法。不像model checking是工具自动给的激励来和assertion匹配，定理证明则是用纯数学方法了。它们之间有一点是共通的，就是都是和根据design specification写的model来比，model checking用assertion表达model，而theorem proving则是用某种中间语言来表达。

用来进行theorem proving最有名的工具语言算是ACL2了。

ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. "ACL2" denotes "A Computational Logic for Applicative Common Lisp".

Intel和AMD都拿ACL2来验证他们的浮点数乘法器。验证过程是类似这样的：

Theorem proving使用的范围比较窄，所以在IC flow中并不常见。

3. Equivalence checking

顾名思义，等价性检查就是看两个design是否等价。像我们常用的Synopsys的formality或者Cadence的Conformal LEC使用的是给定参考状态（拥有match步骤）的combinational equivalence checking（CEC），针对的是同一个design的不同实现阶段。还有可以针对内部状态不match情况下的等价性检查，比如经过retimed, pipeline重排后的design。

3.1 Combinational equivalence checking

等价性检查（Equivalence checking）可以用在IC流程的各个阶段。

除了上图提到的使用场景外，RTL和RTL进行比对也是一项很有用的功能。比如我们对一个模块优化timing，又不想重新跑regression，我们可以比对优化前后的RTL是否等价来进行验证。

我们知道，equivalence checking工具如formality有个步骤叫match，用于match两个design里的参考点，这些参考点和STA里使用的类似，为flip-flop和IO，然后再进行verify。这是很容易理解的，工具把整个等价性检查工具拆分为一系列两个参考点之间的组合逻辑的等价性验证，可以让整个工作高效完成。当然，这只是简单的易于理解的说法，实际上里面会有很多的加速手段。

CEC在IC flow中是标配，即是工程师口中狭义的形式验证，没有听说过不用的。

3.2 SEC与形式验证的统一

实际上formal equivalence checking工具不止于此。上面说到的conception其实称为combinational equivalence checking (CEC)，还有一种是sequential equivalence checking (SEC)。SEC可以对两个时序逻辑设计进行比对，它可能使用BDD等symbolic算法来对设计的状态空间进行表述，这也就演变为了model checking问题，所以SEC通常会使用更高抽象层级的reference model，这个思想和验证RTL功能的model checking和theorem proving就有明显的共通之处了。

JasperGold SEC工具就是做这个工作的。当然SEC主要就是针对RTL对RTL了。我们可以把SEC工具看做model checking的一个特例，这里model不是assertion，而是另一个design，甚至可以是一个周期精确的model，从这点看是不是很像theorem proving实现的功能呢？

可以想象SEC的计算复杂度很高，在不可实现的实现我们通常可以寻求bounded equivalence checking（BEC）的帮助，我们把vector sequence的长度作一个限制，去证明在这个长度以内两个design是等价的。

BEC作为SEC的一个实现手段，自然也可以用于RTL function的model checking。SEC在IC flow中并未普及，IC flow中通常的使用场景都可以用CEC解决。

4. 小结

我们可以看到各种formal verification 手段殊途同归到design implementation和reference model（不管是assertion， RTL ，netlist还是电路的其他中间形式表达）的比对上。

从各种形式验证手段背后思想、算法的角度来看，不管model checking、theorem proving还是equivalence checking它们之间其实还是一致的，很多concept和algorithm可以共享。