一、形式验证

形式验证是什么？什么时候做形式验证？这两个问题算是形式验证的核心问题。第一个问题有关于形式验证的理论，第二个问题有关形式验证的实际应用。

形式验证是为了验证RTL代码与门级网表之间的逻辑等价性。通常在综合的流程中会插入扫描链（关于可测性设计将在后续文章中进行介绍），这样综合出的结果的逻辑关系可能会与RTL代码的等效逻辑不一致；在版图流程中，通常会做时钟树综合，将会在网表中插入BUFF和反向器，这就可能会造成逻辑的不等价。如果在这两种情况下，都采用重新进行一番验证的方式来验证门级网表的正确性，那么将会带来大量的时间消耗，项目流程会被拉长，这对于IC设计来说是不能承受的高成本，因此，采用逻辑等价性验证的方式来验证综合之后、版图导出的门级网表是否与经过验证的RTL代码的逻辑功能完全等价。这样就使得综合之后的门级网表在节省时间的前提下，得到完全的功能验证。

形式验证流程主要是在综合插入扫描链之后，版图时钟树综合之后进行。

二、工具

形式验证工具有很多中，常用的有Formality，conformal(cadence公司)，本章节将采用Formality。

三、示例

利用上一章节（综合）产生的门级网表文件，以及原始RTL代码文件，本示例给出一个简单的教程。

所需文件，如下图所示，其中，UART_XMTR_m.v为综合产生的网表文件：

启动formality图像化界面，启动命令：formality

步骤1，Ref载入参考文件RTL代码，“verilog... > 选中files框下的文件 > loadfile > 3.Set Top Design选项卡 > 2.Choose a design 下UART_XMTR > Set top”

步骤2，载入综合库，“2.Read DB Libraries > DB.. 选择综合库/home/Lance/synopsys/model/018SC7/SM00LB501-FE-00000-r0p0-00rel0/aci/sc-m/synopsys/tt_1v8_25c.db > LoadFiles”

步骤3，Impl载入待验证门级网表，流程与步骤1一致，注意选项卡的选择，如下图，

步骤4，4.Match，5，Verify, “Run matching > ok,”“verify > OK”

步骤6，查看formality运行的终端信息，看到Verifiction SUCCEEDED,表明验证成功，如果不成功，那就要慢慢找原因了。回到6.debug中，可以看到failling points栏是空的，没有不匹配的地方。

以上就是formality验证的一般流程，由于这个流程没有在综合的时候插入扫描链，所以验证之后没有不匹配点，也就没有debug的必要。但是，在实际应用中，一定会存在不匹配点，这个时候就需要仔细的debug了。