概述

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

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

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

第一，驗(yàn)證插入DFT測試邏輯之后的設(shè)計(jì)文件與未插入DFT測試邏輯的原始設(shè)計(jì)文件之間是否等價(jià)；

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

Why Formal Verify

做形式驗(yàn)證是為了確認(rèn)修改后的設(shè)計(jì)電路與原始設(shè)計(jì)電路是等價(jià)的。不管是人為的修改還是工具處理后的電路不一定能保證等價(jià)性，工具也是人做出來的，也有可能會出錯(cuò)，所以要確認(rèn)。

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

Formal Verify****的分類

1、等價(jià)性檢查

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

2、形式模型檢查

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

3、定理證明

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

Formal Verify的流程

1、準(zhǔn)備HDL文件和fm_verify.tcl腳本

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

準(zhǔn)備好綜合后的門級網(wǎng)表文件、插入掃描鏈之后門級網(wǎng)表 文件和fm_verify.tcl運(yùn)行腳本，進(jìn)行門級網(wǎng)表的Formal Verify。

2、設(shè)置design_name和讀取庫文件

set_top top, 設(shè)置頂層為top。

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

3、用read_verilog命令讀入設(shè)計(jì)

create_container pre_dft

read_verilog -f ./scripts/ref_filelist (未插DFT測試邏輯的設(shè)計(jì))

create_container post_dft

read_verilog -f ./scripts/imp_filelist(已插DFT測試邏輯的設(shè)計(jì))

讀入reference design和implement design

current_design top 設(shè)置當(dāng)前設(shè)計(jì)名稱為top

4、設(shè)置環(huán)境

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

5、Match

檢查 reference design 和 Implemention design 的比較點(diǎn)是否匹配。

6、Verify

驗(yàn)證功能是否一致，電路是否等價(jià)。

總結(jié)

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