什么是形式验证(Formal验证)？Formal是怎么实现的呢？

最近看到行业群里面经常有人问什么是形式验证，今天的文章和大家介绍下形式验证(Formal verification)。

相信很多人已经接触过验证。如我前面有篇文章所写验证分为IP验证，FPGA验证，SOC验证和CPU验证，这其中大部分是采用动态仿真(dynamic simulation)实现，即通过给定设计(design)端口测试激励，结合时间消耗判断设计的输出结果是否符合预期。动态仿真又分为定向测试和随机测试。现在很多公司用的UVM验证方法学便是建立在动态仿真的基础上的。

形式验证不同于仿真验证，它是通过数学上完备地证明或验证电路的实现方法是否确实实现了电路设计所描述的功能。形式验证方法分为等价性检查(equivalence checking)如Formality，LEC等和属性检查(Property checking)如Jasper gold，VC Formal 等。我们这里讲的形式验证特指属性的检查(Property checking)。

如上图所示，在一个简单的加法设计中，我们采用动态仿真的方式去验证上述运算是类似一种丢飞镖的过程，想要验到所有的场景要运行2的64次方即18446744073709551616次，这只是简单的加法运算，如果再加入其它稍微复杂的逻辑，想用动态仿真的方式打完所有情况是非常困难的。

另外一种场景是当信号从设计的端口输入，信号流的走向会根据不同设定或者状态选择走向不同的路径。如上图所示，当信号流可选择的路径很多时，通过动态仿真也是很难覆盖到所有路径的。

上述两个问题用Formal就可以很好的解决掉。

除了功能验证上的使用，Formal也可以被用在coverage的收集上。在设计里面有不少代码是无法执行到的。如果用动态仿真去找这些点，一般的做法是跑大量的回归测试（regression），收集coverage，然后针对没打到的coverage hole找designer去review。整个过程走下来会花费不少人力。而用formal可以比较轻松高效的找到其中的一些点。

介绍了这么多，那么Formal是怎么实现的呢？用Formal验证需要输入设计(design)，约束(constraint)和待验证的property。这里的设计一般是指RTL，约束指的是assumption，clock，reset等，propert是指assertion。

下面是一个简单的例子，当设计如下

我们可以通过下面描述来验证该段逻辑,先验证req_valid 为高时，dataout等于datain；

再验证req_valid 为低时，dataout等于0。

Formal适合所有验证场景吗？当然不是，因为formal是通过数学运算去完成完备性验证，在一些简单的逻辑如arbiter，muxes，FSM，Control logic上比较适合用formal去验证，但是对一些复杂的场景，比如涉及到大量的memory，复杂的总线传输，多模块协助工作等场景都不太适合用Formal。

审核编辑：刘清