概述

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的具體流程。