EDA形式化驗證漫談：仿真之外，驗證之內(nèi)

“在未來五年內(nèi)仿真將逐漸被淘汰，僅用于子系統(tǒng)和系統(tǒng)級驗證。與此同時，形式化驗證方法已經(jīng)開始處理一些系統(tǒng)級任務(wù)。隨著技術(shù)發(fā)展，更多Formal相關(guān)的商業(yè)標(biāo)準(zhǔn)化會推出?！?/p>

Intelfellow

M. V. Achutha Kiran Kumar

隨著Formal技術(shù)的發(fā)展，業(yè)內(nèi)已經(jīng)有不少公司有專門的形式化驗證團隊，也培養(yǎng)了一批熱愛Formal，愿意來鉆研這門技術(shù)的EDA人。

仿真方法學(xué)是動態(tài)驗證的一種，是一個“你想到哪里才能驗到哪里”的驗證方式，本質(zhì)上在不斷做加法。你需要先讓自己盡可能多地想到各種場景、耗費大量時間搭建測試環(huán)境，再試圖“碰出BUG”，但是這種方式更擅長發(fā)現(xiàn)設(shè)計“這里有BUG”，但卻很難回答“那里沒有BUG”的問題。

這方面形式化驗證工具有很大的優(yōu)勢。

形式化驗證則被稱為靜態(tài)驗證，是一種基于嚴格的數(shù)學(xué)與算法的驗證方法學(xué)。用戶利用SVA斷言描述清楚需要證明的設(shè)計規(guī)格，通過編譯RTL和基于SVA的斷言語言，建立Formal模型，然后不斷做減法，發(fā)現(xiàn)不符合模型的“反例”。

顯而易見的一個優(yōu)勢是，形式化驗證工具能夠通過建立數(shù)學(xué)模型，實現(xiàn)更敏捷的反向驗證，以類似數(shù)學(xué)定理證明的方式，通過對所有可能的激勵空間進行遍歷，保證邏輯沒有死角，實現(xiàn)驗證的完備化、自動化。

傳統(tǒng)的仿真工具，在進入具體發(fā)現(xiàn)bug階段前，往往需要很長時間為UVM搭建一個完備的驗證平臺（testbench）；而在調(diào)試（Debug）階段，當(dāng)出現(xiàn)UVM error，需要問題定位時，仿真工具一般需要從UVM繁雜的log到rtl再到waveform、信號級別，這也是一個很長的回溯曲線。形式化驗證在這兩個方面，則可以節(jié)省很多時間，尤其是通過直接提供反例波形，可以精準(zhǔn)直指相關(guān)信號進行問題定位。

早期大家可能會擔(dān)心，覺得Formal工具是不是有使用門檻，這種擔(dān)心來源于形式化驗證工具使用過程中，需要基于對設(shè)計的全面理解，才能正確構(gòu)建驗證模型的斷言和約束。

一方面，形式化驗證對驗證工程師而言，確實能夠大大的減輕焦慮，芯華章2021年推出GalaxFV，并且在項目的打磨中，持續(xù)不斷地在豐富應(yīng)用級斷言庫，并對其參數(shù)化、提高可配置性，讓GalaxFV更加容易使用。

另外，隨著設(shè)計規(guī)模增加，工具更加的自動化、智能化，理解設(shè)計會成為工程師的一大優(yōu)勢！用好Formal工具，項目將不再需要靠堆人、堆license、堆時間來提高驗證質(zhì)量。