談?wù)凢ormal驗(yàn)證中的Equivalence Checking

Lec形式驗(yàn)證想必ICer們都很熟悉，尤其是中后端的IC工程師，在正常邏輯綜合生成網(wǎng)表過后或DFT插入mbist等可測試邏輯綜合后，需要對綜合后產(chǎn)生的網(wǎng)表與綜合前的RTL代碼進(jìn)行等效邏輯Lec驗(yàn)證，目的是為了保證綜合過程沒有映射map錯(cuò)，邏輯正確。后端工程師同時(shí)還需要在APR的place，cts等階段手動(dòng)ec后，ecoRt手動(dòng)ec后，將綜合后的網(wǎng)表與PostRoute ec后的網(wǎng)表進(jìn)行Lec驗(yàn)證。

圖1 數(shù)字電路設(shè)計(jì)驗(yàn)證的分類（包括Formal驗(yàn)證和仿真功能驗(yàn)證）

實(shí)際上形式驗(yàn)證是為了驗(yàn)證RTL代碼與綜合后的門級網(wǎng)表之間的邏輯等價(jià)性。功能是否等價(jià)，與時(shí)序無關(guān)。與動(dòng)態(tài)仿真 Simulation Veficiation 相比，形式驗(yàn)證屬于 Static Verification ，不需要手動(dòng)灌入激勵(lì)；只需要通過數(shù)學(xué)分析的方式，對待測設(shè)計(jì)進(jìn)行檢查。

形式驗(yàn)證由兩類靜態(tài)檢查組成：Equivalence Checking 等價(jià)檢查 和 Property Checking 屬性檢查，形式驗(yàn)證現(xiàn)在通常通過EDA工具進(jìn)行驗(yàn)證，業(yè)內(nèi)通常用S家的Formality，C家的Conformal進(jìn)行Lec形式驗(yàn)證，國內(nèi)也有多家企業(yè)在進(jìn)行Formal驗(yàn)證工具的開發(fā)如奇捷科技的EasyECO等等，被應(yīng)用在RTLCode 和 gate level code的LEC等價(jià)檢查。

Equivalence Checking

Combinational equuvalence :用于綜合過后RTL與Netlist之間的檢查，檢查寄存器之間的組合邏輯在綜合前后是否一致，比如常見的Lec驗(yàn)證工具：Formality，Conformal。sequential Equivalence ：用于RTL代碼階段的Check，基于cycle的精確度；在module層面上對時(shí)鐘&時(shí)鐘樹路徑上的gating代碼手動(dòng)ec后的RTL進(jìn)行等價(jià)檢查。Transaction Equivalence :用于C/C++ model 與 RTL代碼之間進(jìn)行檢查，基于transaction的精確度；用于通路的算法類設(shè)計(jì)。

Property Checking

屬性檢查是基于PSL、SVA等斷言語言的，需要通過對屬性的assume,cover,assert等語句進(jìn)行分析，進(jìn)行建立golden模型。FPV（Formal Property Verifacation)需要用戶直接書寫property;從FPV衍生出各類APP，適用于不同場景，可以通過配置相關(guān)配置，自動(dòng)生成對應(yīng)的property。

實(shí)際上前端設(shè)計(jì)使用Spyglass工具對跨時(shí)鐘域設(shè)計(jì)的structure結(jié)構(gòu)的CDC檢查，檢查異步時(shí)鐘寄存器在跨時(shí)鐘域時(shí)，信號有沒有進(jìn)行同步處理也屬于靜態(tài)驗(yàn)證的一種。

S家的Formality的流程(Reference 參照網(wǎng)表/RTL; Implementation 實(shí)施網(wǎng)表)

圖2 Formal工具的GUI界面

由圖2可以觀察到，在參照網(wǎng)表implemetation下方，有從0.Guide到60.debug的Formal驗(yàn)證流程，通常Formal的驗(yàn)證流程為Guidance > Reference>implemetation>setup>Match>Verify（有時(shí)候setup順序可以改變）,再到最后的Debug，聽上去是不是十分復(fù)雜，但是其實(shí)不然，讓小編結(jié)合FM官方的環(huán)境來給你一一介紹：

環(huán)境配置

Guidance

這一步通常是用來添加DC綜合完后，報(bào)出來的.svf文件，通常是些邏輯優(yōu)化記錄和一些約束條件。

Reference（這里舉例是綜合后的，所以Reference吃的是RTL HDL，如果是APR后，那么吃的就是綜合后的網(wǎng)表）

讀入rtl設(shè)計(jì)文件，從吃對應(yīng)teachlibrary的DB文件（S家的lib文件都是.db格式）開始，再吃Reference參照的設(shè)計(jì)文件Verilog、VHDL等等，如果有UPF，則還要吃UPF，如果沒有則設(shè)置頂層文件。

這一步比較簡單，主要就是read 需要對比的網(wǎng)表 read design file > verlilog >load files吃完netlist后再set top

Setup

設(shè)置常量

Match

也是Formal最重要的一個(gè)環(huán)節(jié)，驗(yàn)證Reference與Implementation的邏輯是否一致.match>run matching

通常Implemetation的point要多于Reference，小編出現(xiàn)過Reference的umatch point反而更多的情況，后來定位發(fā)現(xiàn)是部分logic在Reference中刪除了，這也是得來的Formal經(jīng)驗(yàn)??！

Verify

也是Formal最重要的一個(gè)環(huán)節(jié)，驗(yàn)證Reference與Implementation的功能是否一致.這一步驟將吐出failing_point和abort_point，即相同激勵(lì)輸入，信號不同的點(diǎn)，都會(huì)被當(dāng)成功能不一致的點(diǎn)輸出到rpt內(nèi)

Debug

可以通過GUI界面一個(gè)一個(gè)時(shí)序錐來對照追問題port,，也可以通過前面verify和match的報(bào)告來進(jìn)行debug，最后跑完，打印出結(jié)果，可以看到Passing (equivalent)和Failing (notequivalent)是否通過，再分析沒過的原因。

好啦，到這里今天這期Formal形式驗(yàn)證全流程以及flow代碼環(huán)境講解就講到這里啦，小編在這里留下個(gè)小問題，如果在fm環(huán)境內(nèi)要吃UPF（為了Implemetation netlist)，需要進(jìn)行哪些代碼操作呢？知道的小伙伴可以后臺留言哦。

審核編輯：湯梓紅