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 这些模块

审核编辑：刘清