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

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

對于給定的兩個網(wǎng)表（可以稱為原始網(wǎng)表和修訂網(wǎng)表），假設兩個網(wǎng)表的輸入信號、輸出信號，以及網(wǎng)表中的輸入信號、輸出信號和網(wǎng)表中的寄存器配對，產生多對組合邏輯錐（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)表的邏輯功能是否相同。

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

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

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

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