概述

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

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

對(duì)于DFT工程師來(lái)說(shuō)，要完成的形式驗(yàn)證有2種：

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

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

Why Formal Verify

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

DFT工程師運(yùn)用工具將DFT測(cè)試邏輯插入到設(shè)計(jì)中，不能改變?cè)茧娐返墓δ埽栽谕瓿蒁FT設(shè)計(jì)后要驗(yàn)證電路是否等價(jià)于原始設(shè)計(jì)的電路。

Formal Verify的分類

1、等價(jià)性檢查

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

2、形式模型檢查

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

3、定理證明

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

Formal Verify的流程

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

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

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

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

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

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

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

create_container pre_dft

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

create_container post_dft

read_verilog -f ./scripts/imp_filelist(已插DFT測(cè)試邏輯的設(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à)。