形式化驗證是一種驗證方法，而實際應用方向主要有兩方面，一是綜合前后的等價性檢查，二是RTL設計的功能驗證。
本文所講的是形式化驗證方法在RTL設計功能驗證方向的應用。
芯片驗證的兩個方法，一個是模擬仿真驗證，另一個是形式化驗證。
模擬仿真驗證是目前最主流的驗證方法，主要是以 UVM 為代表的驗證方法學，特點就是搭建模擬仿真環境，通過隨機化激勵進行模擬仿真，reference module作為驗證標準進行結果數據的check，以收集覆蓋率的方式作為驗證進度的參考，當代碼覆蓋率和功能點覆蓋率達到100%時，做到sign off。
由此看來，模擬仿真的優點就是基本不受設計復雜度的影響，而缺點就是驗證環境搭建較復雜，測試激勵手動添加，收集覆蓋率周期較長，尤其是Corner場景的覆蓋很讓人頭疼。
形式化驗證從某層面看似乎讓人省心。形式化方法簡單的說就是用數學工具進行定義、開發和驗證，它會對設計電路進行數學建模，然后窮舉系統運行過程中電路所能達到的所有狀態，以斷言的形式完成設計電路的功能驗證和規則檢查（也可以通過reference model的形式，做結果數據的check）。
聽起來似乎完美，但是這要依賴強大的運算系統和EDA工具，否則會發生狀態爆炸問題，長時間無法得出證明結果。以目前的形式化驗證工具來看，還不足以吃進一個超復雜的設計電路，來完全替代模擬仿真的驗證方法。
所以，在芯片的驗證中，隨機仿真驗證和形式化驗證往往是相輔相成，一個更適合系統級功能驗證，一個更適合模塊級的功能驗證。除此之外，還有FPGA的硬件加速測試，這三種驗證手段可謂是三位一體，相輔相成。
個人認為，形式化驗證是基于嚴格的數學算法和模型，根據設計功能提取電路規則的屬性描述，并窮舉系統運行過程中電路所能達到的所有狀態，自動進行數學分析和證明。驗證過程如下：
以上的形式化驗證過程就像做一道數學證明題，用數學方法證明該命題是否成立，而這個證明過程是驗證工具完成的，工程師不需要關心。
目前，業界主流的形式化驗證工具主要有Cadence的 JasperGold 和 Synposys 的 VC-Formal。
形式化驗證使用的是 SVA (SystemVerilog Assertion) 語言，屬于SV的一部分，下面對SVA基本的使用語法進行說明。
SVA的語法主要分為三種使用類型：assume、assert、cover。
使用的基本規則為，先描述一個property，然后為property設置為assume或assert或cover，命名時習慣性將property名字添加“P_”前綴，將assume名字添加“ASM_”前綴，將assert名字添加“AST_”前綴，將cover名字添加“COV_”前綴。注：建議所有屬性帶時鐘沿觸發條件。
Assum即假定之意，也就是假定某些信號符合某規則特性，最常見的就是給輸入信號添加約束，下面對assume語法的使用做簡單介紹：
property P_property_name;
@(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
ASM_property_name: assume property (P_property_name);
ASM_property_name: assume property (@(posedge clk) (condition==1'b1) -> (result==1'b1));
Assert即斷言之意，也就是認為某些信號符合某規則特性，出現反例則報錯，最常見的就是給關鍵信號依據特定屬性設置斷言，來進行特性檢查，下面對assert語法的使用做簡單介紹：
property P_property_name;
@(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
AST_property_name: assert property (P_property_name);
AST_property_name: assert property (@(posedge clk) (condition==1'b1) -> (result==1'b1));
cover即覆蓋之意，也就是對某些信號的某規則特性進行采樣，反饋是否覆蓋該特性，下面對cover語法的使用做簡單介紹：
property P_property_name;
@(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
COV_property_name: cover property (P_property_name);
COV_property_name: cov property (@(posedge clk) (condition==1'b1) -> (result==1'b1));
本文使用的形式化驗證工具是JasperGold，其常用的使用方法有兩種類型，
這里只對FPV進行介紹，也就是 Formal Property Verifycation。
set FPV_ROOT /FPV_project_path
set DES_PATH $FPV_ROOT/source/design
set PRO_PATH $FPV_ROOT/source/property
set_capture_elaborated_design on
check_cov –init –exclude_bind_hierarchies –enable_prove_based_proff_core
analyze -v2k –f $DES_PATH/design.flist
analyze –sva –f $PRO_PATH/property.flist
elaborate –top top_module_name
clock clock_signal_name
reset reset_signal_name
set_prove_time_limit 24h
prove -all
report –summary –force –result –file “report/FPV_project_name.rpt”
啟動驗證環境很簡單，驗證流程主要依靠啟動腳本的設置，而驗證環境的啟動只需在終端敲下啟動命令即可，如下：
jg FPV_project_name.tcl
當然不是！
換句話說，形式化驗證不能驗證完全，雖然不能做到sign off，但是可以將前期暴露的語法bug和設計bug進行修復，最終驗證不完全，無非表明我不一定是對的，但也沒找到我的錯誤，說明設計代碼已經達到一定成熟度。
復雜的設計驗證時間通常較長，不容易完成驗證，但是，依據設計的特性，也是可以通過一些手段完成驗證，下面以典型設計舉例。
此設計有以下幾個特點：
以上方法還未在實際工程中使用過，待后續總結
