Definition

Formal Verification：利用數學分析的方法，通過算法引擎建立模型，對待測設計的狀態空間進行窮盡分析的驗證。

Kinds of Formal Verification

相比于動態仿真Simulation Veficiation，形式驗證屬于Static Verification，不需要手動灌入激勵；通過數學分析的方式，對待測設計進行檢查；

在這里插入圖片描述

形式驗證分為兩大分支：Equivalence Checking等價檢查 和Property Checking屬性檢查 形式驗證初次被EDA工具采用，可以追溯到90年代，被應用于RTL code和gate level code的LEC等價檢查；后來形式驗證開始慢慢發展，衍生出適用于不同場景的各類工具；

Equivalence Checking

Combinational equivalence：用于RTL vs Netlist的檢查，檢查寄存器之間的組合邏輯在綜合前后是否一致，如Formality，Conformal。Sequential Equivalence: 用于RTL vs RTL的檢查，基于cycle的精確度；適用于對原有block級RTL做了非邏輯修改，如Clock/power gating，對修改后的RTL進行等價檢查。Transaction Equivalence：用于C/C++ model VS RTL的檢查，基于transaction的精確度；常用于數據通路的算法類設計。

Property Checking

屬性檢查基于PSL/SVA Assertion Languages，通過對property的assume,cover,assert語句分析，建立golden模型。FPV(Formal Property Verification)需要用戶直接書寫property；從FPV衍生出各類APP，適用于不同場景，可以根據相關配置，自動生成對應的property。

除了上述兩類，CDC的檢查也屬于static verification；例如Spyglass會對跨時鐘域設計做structural 結構上的檢查，檢查跨時鐘域的信號是否經過同步器處理；一般來講，formal verification屬于static verification;

Simulation VS Formal

Simulation屬于Dynamic Verification，Formal屬于Static Verification；兩者是相互補充的驗證手段，各有優缺點，在合適的場景采用合適的驗證手段，達到最佳的ROI。

在這里插入圖片描述

Simulation是time-based的，仿真器依據消耗時間的事件推進仿真的進行，激勵需要用戶施加；Simulation雖然可以隨機化發送激勵，但是對于corner case的遍歷需要花費大量時間；Simulation適用于大規模的設計，仿真的時間深度可以輕松達到上萬個cycle；

Formal是state-space based的，依據算法探索所有可能的狀態空間，不需要平臺搭建和輸入激勵，便于快速啟動驗證；Formal適用于小模塊的驗證，隨著設計復雜度和cycle深度的增加，formal會占用大量資源，難以收斂；

Formal適用于40,000 寄存器以內的模塊驗證（這個數據已經被刷新）；隨著設計復雜度的增加，state space explosion，狀態空間激增；一個設計包含n個dff，有2n種配置，m個input有2m種組合；該設計可能的狀態達到2(n+m)個；對于一個10 input，10 dff的設計，為220=1,048,576。

回到開頭所說的，Simulation和Formal是相互補充的；模塊中的assertion語句既可以在Formal中使用，也可以在Simulation中使用；Formal產生的覆蓋率也可以merge到Simulation的覆蓋率中；設計人員可以通過Formal免于平臺的搭建，快速地跑通IP中的一些模塊，再hand-off給驗證人員使用Simulation sign-off（Shift-Left）；Simulation中的corner scenario，可以通過Bug hunting FPV補充驗證；

Formal do better

不同的驗證策略適合不同的驗證場景；Emulation適用于整個Chip級的驗證，加速仿真速度；UVM-Simulation適用于復雜寄存器配置的傳輸packet的IP驗證，便于提取transaction和隨機化驗證；Formal（FPV）適合相對較小的模塊，便于收斂；Formal適合controllable的模塊，例如FSMs；Formal適合observable的模塊，便于assertion的書寫，如AXI bus；串行bus則不適合使用formal。開源項目Opentitan中使用FPV的驗證模塊[2]。

適合Formal的常見模塊如下：

?Arbiter、Scheduler

?FIFO 、FSMs

?Interrupt controller、DMA controller、Memory controller

?Power manager unit、Clock programing unit

?Bus、Bus bridge、Bus Fabric (CrossBar NoC etc)

?Cache，Cache-Coherent Protocols modeling and verification

?Data transport

?Pinmux, Clock Controller, Reset Controller

The growth of Formal

Formal Property Verification相關的工具也有十幾年歷史了，但由于其限制，Formal Tool并沒有被用戶廣泛使用。但最近這些年，一些因素推動了formal的高速發展：

1. 之前繁多的語言（Vera，'e'，摩托羅拉的CBV和英特爾的ForSpec）整合為SystemVerilog Assertion，并加入IEEE 1800協議，成為標準化的Assertion Languages。工程師在Simulation中廣泛使用SVA，節省了在Formal上的學習成本。

2. 隨著工藝節點的縮小，流程成本大幅提高；對于corner scenario下可能會隱藏的bug，工程師更傾向Fromal這類exhaustive的驗證手段。

3. Formal可以很好的匹配Simulation；同一家EDA的Formal和Simulation工具相互打通，Formal產生coverage可以和Simulation的coverage相互merge，Formal產生的波形可以在Simulaiton上復現，Formal和Simulaiton相同的GUI Debug工具等。

4. 各類Formal APPs的推出，使得Formal更容易掌握和部署。

5. 隨著企業服務器性能的提升和Formal算法的發展，可以處理更復雜的設計規模。

6. 一些基于C/C++ model的包含大量運算單元的硬件產品，如AI/ML，GPU的需要爆發，推動了Formal Data Path Validation；

7. Automotive Chip需求激增及其高可靠性的要求，Formal提供safety fault analysis的功能；

8. 芯片對Security的要求越來越高，需要窮盡分析所有訪問路徑，適合采用Formal；

9. 移動端芯片對于Lower Power的重視；PMU模塊適合formal驗證；

10.采用敏捷開發的芯片團隊，對于"shift left"的追求，采用formal快速進行模塊驗證及早發現bug;

Deepchip

Deepchip上一個forma系列的專訪，全面的介紹了formal：

?Jim Hogan on how "this is not your father's formal verification"[3]

?Where Formal ABV whomps HDL simulation for chip verification[4]

?9 major and 23 minor Formal ABV tool metrics - plus their gotchas[5]

?16 Formal Apps that make Formal easy for us non-Formal engineers[6]

?Hogan on Cadence, Mentor, OneSpin, Real Intent, Synopsys formal[7]

審核編輯：劉清