概述

Formal Verify，即形式驗證，主要思想是通過使用數(shù)學證明的方式來驗證一個修改后的設計和它原始的設計，在功能上是否等價。

用于比較的設計文件可以是一個RTL級的設計和它的門級網(wǎng)表，或者綜合后的門級網(wǎng)表和做完布局布線及優(yōu)化之后的門級網(wǎng)表。常見的工具是synopsys公司的Formality。

對于DFT工程師來說，要完成的形式驗證有2種：

第一，驗證插入DFT測試邏輯之后的設計文件與未插入DFT測試邏輯的原始設計文件之間是否等價；

第二，驗證綜合后插入掃描鏈的門級網(wǎng)表與未插入掃描鏈的門級網(wǎng)表之間是否等價。

Why Formal Verify

做形式驗證是為了確認修改后的設計電路與原始設計電路是等價的。不管是人為的修改還是工具處理后的電路不一定能保證等價性，工具也是人做出來的，也有可能會出錯，所以要確認。

DFT工程師運用工具將DFT測試邏輯插入到設計中，不能改變原始電路的功能，所以在完成DFT設計后要驗證電路是否等價于原始設計的電路。

Formal Verify****的分類

1、等價性檢查

用于比較設計的兩種實現(xiàn)是否一致，可分為組合等價性檢查和時序等價性檢查。利用數(shù)學技術來驗證參考設計與改動后的設計等價，主要目的是在一個設計經(jīng)過變換之后，窮舉地檢驗變換前后的功能一致性，即證明設計的變換沒有產(chǎn)生功能的變化。

2、形式模型檢查

是一種檢測設計是否具有所需屬性的方法，如安全性、活性和公平性。模型檢驗所針對的對象是同步時序設計。系統(tǒng)的設計spec用時序狀態(tài)邏輯公式來描述。而通過對有限狀態(tài)系統(tǒng)的所有可能的狀態(tài)空間遍歷來證明設計是符合規(guī)范的，增強設計者的信心；或者是通過提供違反spec的反例，以幫助設計者來發(fā)現(xiàn)早期設計的錯誤。反例給出的方式是從系統(tǒng)的初始狀態(tài)出發(fā)到“壞”的狀態(tài)的路徑。系統(tǒng)的狀態(tài)空間能夠用有效的抽象符號算法來隱含地描述。

3、定理證明

是形式驗證技術中最高的，它需要設計行為的形式化描述，通過嚴格的數(shù)學證明，比較HDL描述的設計和系統(tǒng)的形式化描述在所有可能輸入下是否一致。這種驗證方法需要非常深厚的數(shù)學功底，而且不能完全自動化，所以應用案例較少。

Formal Verify的流程

1、準備HDL文件和fm_verify.tcl腳本

對于DFT工程師，需要準備好原始設計的RTL-level的HDL文件、插入DFT測試邏輯之后RTL-level的HDL 文件和fm_verify.tcl運行腳本，進行RTL的Formal Verify；

準備好綜合后的門級網(wǎng)表文件、插入掃描鏈之后門級網(wǎng)表 文件和fm_verify.tcl運行腳本，進行門級網(wǎng)表的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、設置環(huán)境

讀取設計后，需要設置formal verification環(huán)境。比如插入dft以后，做function驗證時，不需要考慮scan mode/test mode，或者人為創(chuàng)建的port，需要給這些port設置一個常量告訴工具不去檢查。

5、Match

檢查 reference design 和 Implemention design 的比較點是否匹配。

6、Verify

驗證功能是否一致，電路是否等價。

總結

本文主要介紹了Formal Verify的概念、分類、進行Formal Verify的原因以及Formal Verify的具體流程。