谈谈Formal验证中的Equivalence Checking

Lec形式验证想必ICer们都很熟悉，尤其是中后端的IC工程师，在正常逻辑综合生成网表过后或DFT插入mbist等可测试逻辑综合后，需要对综合后产生的网表与综合前的RTL代码进行等效逻辑Lec验证，目的是为了保证综合过程没有映射map错，逻辑正确。后端工程师同时还需要在APR的place，cts等阶段手动ec后，ecoRt手动ec后，将综合后的网表与PostRoute ec后的网表进行Lec验证。

图1 数字电路设计验证的分类（包括Formal验证和仿真功能验证）

实际上形式验证是为了验证RTL代码与综合后的门级网表之间的逻辑等价性。功能是否等价，与时序无关。与动态仿真 Simulation Veficiation 相比，形式验证属于 Static Verification ，不需要手动灌入激励；只需要通过数学分析的方式，对待测设计进行检查。

形式验证由两类静态检查组成：Equivalence Checking 等价检查 和 Property Checking 属性检查，形式验证现在通常通过EDA工具进行验证，业内通常用S家的Formality，C家的Conformal进行Lec形式验证，国内也有多家企业在进行Formal验证工具的开发如奇捷科技的EasyECO等等，被应用在RTLCode 和 gate level code的LEC等价检查。

Equivalence Checking

Combinational equuvalence :用于综合过后RTL与Netlist之间的检查，检查寄存器之间的组合逻辑在综合前后是否一致，比如常见的Lec验证工具：Formality，Conformal。sequential Equivalence ：用于RTL代码阶段的Check，基于cycle的精确度；在module层面上对时钟&时钟树路径上的gating代码手动ec后的RTL进行等价检查。Transaction Equivalence :用于C/C++ model 与 RTL代码之间进行检查，基于transaction的精确度；用于通路的算法类设计。

Property Checking

属性检查是基于PSL、SVA等断言语言的，需要通过对属性的assume,cover,assert等语句进行分析，进行建立golden模型。FPV（Formal Property Verifacation)需要用户直接书写property;从FPV衍生出各类APP，适用于不同场景，可以通过配置相关配置，自动生成对应的property。

实际上前端设计使用Spyglass工具对跨时钟域设计的structure结构的CDC检查，检查异步时钟寄存器在跨时钟域时，信号有没有进行同步处理也属于静态验证的一种。

S家的Formality的流程(Reference 参照网表/RTL; Implementation 实施网表)

图2 Formal工具的GUI界面

由图2可以观察到，在参照网表implemetation下方，有从0.Guide到60.debug的Formal验证流程，通常Formal的验证流程为Guidance > Reference>implemetation>setup>Match>Verify（有时候setup顺序可以改变）,再到最后的Debug，听上去是不是十分复杂，但是其实不然，让小编结合FM官方的环境来给你一一介绍：

环境配置

Guidance 

这一步通常是用来添加DC综合完后，报出来的.svf文件，通常是些逻辑优化记录和一些约束条件。

Reference（这里举例是综合后的，所以Reference吃的是RTL HDL，如果是APR后，那么吃的就是综合后的网表）

读入rtl设计文件，从吃对应teachlibrary的DB文件（S家的lib文件都是.db格式）开始，再吃Reference参照的设计文件Verilog、VHDL等等，如果有UPF，则还要吃UPF，如果没有则设置顶层文件。

这一步比较简单，主要就是read 需要对比的网表 read design file > verlilog >load files吃完netlist后再set top

Setup

设置常量

Match

也是Formal最重要的一个环节，验证Reference与Implementation的逻辑是否一致.match>run matching

通常Implemetation的point要多于Reference，小编出现过Reference的umatch point反而更多的情况，后来定位发现是部分logic在Reference中删除了，这也是得来的Formal经验！！

Verify

也是Formal最重要的一个环节，验证Reference与Implementation的功能是否一致.这一步骤将吐出failing_point和abort_point，即相同激励输入，信号不同的点，都会被当成功能不一致的点输出到rpt内

Debug

可以通过GUI界面一个一个时序锥来对照追问题port,，也可以通过前面verify和match的报告来进行debug，最后跑完，打印出结果，可以看到Passing (equivalent)和Failing (notequivalent)是否通过，再分析没过的原因。

好啦，到这里今天这期Formal形式验证全流程以及flow代码环境讲解就讲到这里啦，小编在这里留下个小问题，如果在fm环境内要吃UPF（为了Implemetation netlist)，需要进行哪些代码操作呢？知道的小伙伴可以后台留言哦。

审核编辑：汤梓红