SOC V2.0的Formal是什么？

这里的Formal是formality/LEC 吗？不是。那这里的Formal是什么？

SOC V2.0 里的Formal是形式验证。

形式验证不同于仿真验证，它是通过数学上完备地证明或验证电路的实现方法是否确实实现了电路设计所描述的功能。

形式验证方法分为等价性检查(equivalence checking)如Formality，LEC等和属性检查(Property checking)如Jasper gold，VC Formal 等。

我们这里讲的形式验证特指属性的检查(Property checking)。

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

另外一种场景是当信号从设计的端口输入，信号流的走向会根据不同设定或者状态选择走向不同的路径。

如上图所示，当信号流可选择的路径很多时，通过动态仿真也是很难覆盖到所有路径的。

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

在处芯积律SOC V2的项目里面，提供了一个用Formal 验证PIN MUX 的案例。

通过实际例子让大家感受 Formal 环境长什么样？Formal是怎么验证的。

除了 Formal ，SOC V2 项目还有什么？

No1. 有DMA，ISP，PINMUX 这些模块

审核编辑：刘清