形式驗證工具（Formal Verification Tool）是通過數(shù)學邏輯的算法來判斷硬件設(shè)計的功能是否正確，通常有等價性檢查（Equivalence Checking）和屬性檢查（Property Checking）兩種方法。

等價性檢查用來檢查兩個數(shù)字集成電路設(shè)計之間的邏輯等價性。在集成電路設(shè)計過程中許多步驟都可能做邏輯修改，例如插入可測性設(shè)計邏輯、時鐘樹綜、工程變更單等，如果用仿真驗證會耗費大量時間而且難以保證驗證的覆蓋率。等價性檢查時通過靜態(tài)和數(shù)學邏輯的算法來比較修改前后邏輯的一致性，理論上可實現(xiàn)全覆蓋驗證。

對于給定的兩個網(wǎng)表（可以稱為原始網(wǎng)表和修訂網(wǎng)表），假設(shè)兩個網(wǎng)表的輸入信號、輸出信號，以及網(wǎng)表中的輸入信號、輸出信號和網(wǎng)表中的寄存器配對，產(chǎn)生多對組合邏輯錐（Combinational Logic Cones）;然后再用二元決策圖（Binary Decision Diagram）、合取范式的可滿足性求解器（SAT So lver）等算法，對每一對組合邏輯錐進行比較。如果每一對里兩個邏輯錐的布爾函數(shù)都是等價的，就能斷定兩個網(wǎng)表的靜態(tài)和時序邏輯功能是相同的。等價性檢查驗證示意圖如圖5-112所示。

當原始網(wǎng)表和修訂網(wǎng)表的寄存器個數(shù)不相同時 ，上述的算法通常會發(fā)現(xiàn)有些配對的組合邏輯錐里的兩個布爾函數(shù)是不等價的。這時就必須用一些檢測時序邏輯等效性（Sequential Equivalence Checking）的算法做進一步分析，從而判定兩個網(wǎng)表的邏輯功能是否相同。

屬性檢查時一種分析電路設(shè)計是否滿足某些給定規(guī)范或斷言（Assertion）的方法。首先用邏輯結(jié)構(gòu)和形式化邏輯描述系統(tǒng)模型和待驗證的屬性，如時序邏輯結(jié)構(gòu)、有限狀態(tài)機和形式邏輯公式等，再通過形式驗證的算法來檢測設(shè)計是否滿足該屬性。屬性檢查技術(shù)又可以分為定理證明（Theorem Proving）和模型檢查（Model Checking）。

定理證明是將設(shè)計和待驗證的屬性用某種形式化邏輯系統(tǒng)的公式表示出來，再根據(jù)該系統(tǒng)的公理、推理規(guī)則以及已經(jīng)證明的定理，推導出表達系統(tǒng)屬性的公式，從而證明設(shè)計滿足該屬性。這種推導的過程通常需要人工參與，并要對系統(tǒng)功能設(shè)計有相當程度的了解。

模型檢查是用時序邏輯結(jié)構(gòu)或有限狀態(tài)機表示待檢驗的設(shè)計。首先用某種時態(tài)邏輯表示設(shè)計應(yīng)該具有的屬性，再通過二元決策圖、合取范式可滿足性求解、自動測試生成（ATPG）等技術(shù)搜尋設(shè)計的狀態(tài)空間，檢測是否在所有可能的狀態(tài)下設(shè)計都滿足這些屬性。如果檢測出設(shè)計不滿足某種屬性時，也能給出反例，方便錯誤的定位。模型檢查算法通常不需要人工參與，但如果設(shè)計可能存在的狀態(tài)空間太大時，會遭遇所謂的狀態(tài)爆炸（State Explosin）問題，導致無法在有限的時間內(nèi)得到最終的結(jié)果。

由于工藝的不斷演進，等價性檢查和屬性檢查的技術(shù)必須不斷地改進才能處理越來越大的設(shè)計規(guī)模。