formal形式验证原理

formal原理：

在超大规模asic设计中，仿真代码需要花费大量的时间。在确定功能正确后，在后续每一步的流程中是通过等价对比来保证正确性的，此处的等价对比就是所谓的形式验证。

formal验证思想是对于两个设计reference design和implementation design，基于逻辑锥(logic cones)的原理进行等价比较，对逻辑锥输入相同的激励，然后对比较点(compare points)的数据进行一致性对比，如下图所示：

http://s7/mw690/002pcoHFzy7hbnia09E86&690
图一 formal等价性比对原理
http://s10/mw690/002pcoHFzy7hbnhUFv3d9&690
图二 逻辑锥示意图

逻辑锥：

逻辑锥是根据比较点得到的，来源于：

u  primary outputs.

u  sequential elements.

u  black box input pins.

u  nets driven by multiple drivers, where at one driver is a port or black box.

逻辑锥是在match的时候两个设计形成匹配的，匹配的方法来自于：

1.       exact-name matching( name-based matching ).

2.       name filtering( name-based matching ).

3.       topological equivalence ( non-name-based matching).

4.       signature analysis (non-name-based matching).

5.       compare point matching based on net names ( name-based matching).

formal执行流程：

formal的执行一般顺序是启动软件、设置参数、读入设计、然后进行比对，流程图如下所示：

 http://s12/mw690/002pcoHFzy7hbnr09lh5b&690
图三 八步法formal执行流程

http://s13/mw690/002pcoHFzy7hbnu5SYQac&690
图四 formal迭代执行流程

整个flow中formal的作用：

整个asic流程中验证通过后的RTL代码作为功能稳定的golden代码，后续需要插入mbist、综合网表、插入DFT扫描链、后端place、插入时钟树、后端route，每一步流程都有可能修改逻辑功能，为了保证功能不能变化都需要做formal验证，所以在整个flow流程中formal的位置如下：

http://s4/mw690/002pcoHFzy7hbo93ocP33&690
图五 flow中formal的作用

formal优缺点：

优点：因为是穷举的方法进行比对，所以相对于一般的仿真不需要测试向量、能完整覆盖全部测试空间、验证时间短；

缺点：不能发现代码中的功能错误和时序错误，规模太大的话验证时间更大（所以在大规模设计中进行harden模块划分）。

常用工具：

Synopsys公司的Formality；

Candence公司的Conformal。