Formal Verification：形式驗(yàn)證的分類、發(fā)展、適用場景

Definition

Formal Verification：利用數(shù)學(xué)分析的方法，通過算法引擎建立模型，對待測設(shè)計(jì)的狀態(tài)空間進(jìn)行窮盡分析的驗(yàn)證。

Kinds of Formal Verification

相比于動(dòng)態(tài)仿真Simulation Veficiation，形式驗(yàn)證屬于Static Verification，不需要手動(dòng)灌入激勵(lì)；通過數(shù)學(xué)分析的方式，對待測設(shè)計(jì)進(jìn)行檢查；

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

Equivalence Checking

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

Property Checking

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

除了上述兩類，CDC的檢查也屬于static verification；例如Spyglass會(huì)對跨時(shí)鐘域設(shè)計(jì)做structural 結(jié)構(gòu)上的檢查，檢查跨時(shí)鐘域的信號是否經(jīng)過同步器處理；一般來講，formal verification屬于static verification;

Simulation VS Formal

Simulation屬于Dynamic Verification，F(xiàn)ormal屬于Static Verification；兩者是相互補(bǔ)充的驗(yàn)證手段，各有優(yōu)缺點(diǎn)，在合適的場景采用合適的驗(yàn)證手段，達(dá)到最佳的ROI。

Simulation是time-based的，仿真器依據(jù)消耗時(shí)間的事件推進(jìn)仿真的進(jìn)行，激勵(lì)需要用戶施加；Simulation雖然可以隨機(jī)化發(fā)送激勵(lì)，但是對于corner case的遍歷需要花費(fèi)大量時(shí)間；Simulation適用于大規(guī)模的設(shè)計(jì)，仿真的時(shí)間深度可以輕松達(dá)到上萬個(gè)cycle；

Formal是state-space based的，依據(jù)算法探索所有可能的狀態(tài)空間，不需要平臺(tái)搭建和輸入激勵(lì)，便于快速啟動(dòng)驗(yàn)證；Formal適用于小模塊的驗(yàn)證，隨著設(shè)計(jì)復(fù)雜度和cycle深度的增加，formal會(huì)占用大量資源，難以收斂；

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

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

Formal do better

不同的驗(yàn)證策略適合不同的驗(yàn)證場景；Emulation適用于整個(gè)Chip級的驗(yàn)證，加速仿真速度；UVM-Simulation適用于復(fù)雜寄存器配置的傳輸packet的IP驗(yàn)證，便于提取transaction和隨機(jī)化驗(yàn)證；Formal（FPV）適合相對較小的模塊，便于收斂；Formal適合controllable的模塊，例如FSMs；Formal適合observable的模塊，便于assertion的書寫，如AXI bus；串行bus則不適合使用formal。開源項(xiàng)目Opentitan中使用FPV的驗(yàn)證模塊^[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相關(guān)的工具也有十幾年歷史了，但由于其限制，F(xiàn)ormal Tool并沒有被用戶廣泛使用。但最近這些年，一些因素推動(dòng)了formal的高速發(fā)展：

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

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

3. 3. Formal可以很好的匹配Simulation；同一家EDA的Formal和Simulation工具相互打通，F(xiàn)ormal產(chǎn)生coverage可以和Simulation的coverage相互merge，F(xiàn)ormal產(chǎn)生的波形可以在Simulaiton上復(fù)現(xiàn)，F(xiàn)ormal和Simulaiton相同的GUI Debug工具等。

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

5. 5. 隨著企業(yè)服務(wù)器性能的提升和Formal算法的發(fā)展，可以處理更復(fù)雜的設(shè)計(jì)規(guī)模。

6. 6. 一些基于C/C++ model的包含大量運(yùn)算單元的硬件產(chǎn)品，如AI/ML，GPU的需要爆發(fā)，推動(dòng)了Formal Data Path Validation；

7. 7. Automotive Chip需求激增及其高可靠性的要求，F(xiàn)ormal提供safety fault analysis的功能；

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

9. 9. 移動(dòng)端芯片對于Lower Power的重視；PMU模塊適合formal驗(yàn)證；

10. 10.采用敏捷開發(fā)的芯片團(tuán)隊(duì)，對于"shift left"的追求，采用formal快速進(jìn)行模塊驗(yàn)證及早發(fā)現(xiàn)bug;