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

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

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

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

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

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

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

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