“在未來五年內仿真將逐漸被淘汰，僅用于子系統和系統級驗證。與此同時，形式化驗證方法已經開始處理一些系統級任務。隨著技術發展，更多Formal相關的商業標準化會推出。”

Intelfellow

M. V. Achutha Kiran Kumar

隨著Formal技術的發展，業內已經有不少公司有專門的形式化驗證團隊，也培養了一批熱愛Formal，愿意來鉆研這門技術的EDA人。

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

這方面形式化驗證工具有很大的優勢。

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

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

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

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

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

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