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等等，被应用在RTL Code 和 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可以观察到，在参照网表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 (not equivalent)是否通过，再分析没过的原因。
好啦，到这里今天这期Formal形式验证全流程以及flow代码环境讲解就讲到这里啦，小编在 这里留下个小问题，如果在fm环境内要吃UPF（为了Implemetation netlist)，需要进行哪些代码 操作呢？知道的小伙伴可以后台留言哦。
我是处芯积律，感谢大家阅读！！
作者： 处芯积律
文章来源： 处芯积律
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏。
迎添加极术小姐姐微信（id:aijishu20)加入技术交流群，请备注研究方向。
