Formal Verify形式验证的流程概述

概述

Formal Verify，即形式验证，主要思想是通过使用数学证明的方式来验证一个修改后的设计和它原始的设计，在功能上是否等价。

用于比较的设计文件可以是一个RTL级的设计和它的门级网表，或者综合后的门级网表和做完布局布线及优化之后的门级网表。常见的工具是synopsys公司的Formality。

对于DFT工程师来说，要完成的形式验证有2种：

第一，验证插入DFT测试逻辑之后的设计文件与未插入DFT测试逻辑的原始设计文件之间是否等价；

第二，验证综合后插入扫描链的门级网表与未插入扫描链的门级网表之间是否等价。

Why Formal Verify

做形式验证是为了确认修改后的设计电路与原始设计电路是等价的。不管是人为的修改还是工具处理后的电路不一定能保证等价性，工具也是人做出来的，也有可能会出错，所以要确认。

DFT工程师运用工具将DFT测试逻辑插入到设计中，不能改变原始电路的功能，所以在完成DFT设计后要验证电路是否等价于原始设计的电路。

Formal Verify****的分类

1、等价性检查

用于比较设计的两种实现是否一致，可分为组合等价性检查和时序等价性检查。利用数学技术来验证参考设计与改动后的设计等价，主要目的是在一个设计经过变换之后，穷举地检验变换前后的功能一致性，即证明设计的变换没有产生功能的变化。

2、形式模型检查

是一种检测设计是否具有所需属性的方法，如安全性、活性和公平性。模型检验所针对的对象是同步时序设计。系统的设计spec用时序状态逻辑公式来描述。而通过对有限状态系统的所有可能的状态空间遍历来证明设计是符合规范的，增强设计者的信心；或者是通过提供违反spec的反例，以帮助设计者来发现早期设计的错误。反例给出的方式是从系统的初始状态出发到“坏”的状态的路径。系统的状态空间能够用有效的抽象符号算法来隐含地描述。

3、定理证明

是形式验证技术中最高的，它需要设计行为的形式化描述，通过严格的数学证明，比较HDL描述的设计和系统的形式化描述在所有可能输入下是否一致。这种验证方法需要非常深厚的数学功底，而且不能完全自动化，所以应用案例较少。

Formal Verify的流程

1、准备HDL文件和fm_verify.tcl脚本

对于DFT工程师，需要准备好原始设计的RTL-level的HDL文件、插入DFT测试逻辑之后RTL-level的HDL 文件和fm_verify.tcl运行脚本，进行RTL的Formal Verify；

准备好综合后的门级网表文件、插入扫描链之后门级网表 文件和fm_verify.tcl运行脚本，进行门级网表的Formal Verify。

2、设置design_name和读取库文件

set_top top, 设置顶层为top。

read_db/project/${USER}/library/db/*.db,用read_db读取.db库文件。

3、用read_verilog命令读入设计

create_container pre_dft

read_verilog -f ./scripts/ref_filelist (未插DFT测试逻辑的设计)

create_container post_dft

read_verilog -f ./scripts/imp_filelist(已插DFT测试逻辑的设计)

读入reference design和implement design

current_design top 设置当前设计名称为top

4、设置环境

读取设计后，需要设置formal verification环境。比如插入dft以后，做function验证时，不需要考虑scan mode/test mode，或者人为创建的port，需要给这些port设置一个常量告诉工具不去检查。

5、Match

检查 reference design 和 Implemention design 的比较点是否匹配。

6、Verify

验证功能是否一致，电路是否等价。

总结

本文主要介绍了Formal Verify的概念、分类、进行Formal Verify的原因以及Formal Verify的具体流程。