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

圖1 數字電路設計驗證的分類（包括Formal驗證和仿真功能驗證）

實際上形式驗證是為了驗證RTL代碼與綜合后的門級網表之間的邏輯等價性。功能是否等價，與時序無關。與動態仿真 Simulation Veficiation 相比，形式驗證屬于 Static Verification ，不需要手動灌入激勵；只需要通過數學分析的方式，對待測設計進行檢查。

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

Equivalence Checking

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

Property Checking

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

實際上前端設計使用Spyglass工具對跨時鐘域設計的structure結構的CDC檢查，檢查異步時鐘寄存器在跨時鐘域時，信號有沒有進行同步處理也屬于靜態驗證的一種。

S家的Formality的流程(Reference 參照網表/RTL; Implementation 實施網表)

圖2 Formal工具的GUI界面

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

環境配置

Guidance

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

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

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

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

Setup

設置常量

Match

也是Formal最重要的一個環節，驗證Reference與Implementation的邏輯是否一致.match>run matching

通常Implemetation的point要多于Reference，小編出現過Reference的umatch point反而更多的情況，后來定位發現是部分logic在Reference中刪除了，這也是得來的Formal經驗！！

Verify

也是Formal最重要的一個環節，驗證Reference與Implementation的功能是否一致.這一步驟將吐出failing_point和abort_point，即相同激勵輸入，信號不同的點，都會被當成功能不一致的點輸出到rpt內

Debug

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

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

審核編輯：湯梓紅