形式等效性檢查

通常是在集成電路設計中，通過一些數學方法（如二元決策圖、布爾可滿足性問題），來對不同電路之間進行形式驗證，比較它們在行為上是否等效。 ^[1] 

在計算機硬件（特別是集成電路）和軟件系統的設計過程中，形式驗證的含義是根據某個或某些形式規範或屬性，使用數學的方法證明其正確性或非正確性。

軟件測試無法證明系統不存在缺陷，也不能證明它匹配一定的屬性。只有形式化驗證過程可以證明一個系統不存在某個缺陷或匹配某個或某些屬性。系統無法被證明或測試為無缺陷，這是因為不可能形式地規定什麼是“沒有缺陷”。所有可以做的，就是證明一個系統沒有任何可以想到的缺陷，並且滿足所有的使系統匹配功能要求的和有用的屬性。

在集成電路設計中，形式驗證是一種集成電路設計的驗證方法，它的主要思想是通過使用形式證明的方式來驗證一個設計的功能是否正確。形式驗證可以分為三大類：等價性檢查（Equivalence Checking）、形式模型檢查（Formal Model Checking，也被稱作特性檢查）和定理證明（Theory Prover）。

等價性檢查的驗證用於驗證寄存器傳輸級設計與門級網表之間、門級網表與門級網表之間是否一致。在進行掃描鏈重排、時鐘樹綜合等過程中，都可以用等價性檢查保證網表的一致性。等價性檢查已經融入集成電路標準設計流程中。等價性檢查在檢查ECO時非常有用。例如，設計者在修改門級網表時，由於手誤，錯將一個或門寫成或非門，等價性檢查工具通過比較寄存器傳輸級設計與門級網表，可以很容易地發現這種錯誤。

模型檢查用時態邏輯來描述規範，通過有效的搜索方法來檢查給定的系統是否滿足規範。模型檢查是目前研究的熱點，但其驗證的電路規模受限制這一問題還沒有得到很好的解決。

定理證明把系統與規範都表示成數學邏輯公式，從公理出發尋求描述。定理證明驗證的電路模型不受限制，但需要用户的人工干預和較多的背景知識。 ^[2] 

電子設計自動化（英語：Electronic design automation，縮寫：EDA）是指利用計算機輔助設計（CAD）軟件，來完成超大規模集成電路（VLSI）芯片的功能設計、綜合、驗證、物理設計（包括佈局、佈線、版圖、設計規則檢查等）等流程的設計方式。

現今數字電路非常模組化（參見集成電路設計、設計收斂、設計流程 (EDA)），產線最前端將設計流程標準化，把設計流程區分為許多“細胞”（cells），而暫不考慮技術，接着細胞則以特定的集成電路技術實現邏輯或其他電子功能。製造商通常會提供組件庫（libraries of components），以及符合標準模擬工具的模擬模型給生產流程。模擬 EDA 工具較不模組化，因為它需要更多的功能，零件間需要更多的互動，而零件一般説較不理想。

在電子產業中，由於半導體產業的規模日益擴大，EDA 扮演越來越重要的角色。使用這項技術的廠商多是從事半導體器件製造的代工製造商，以及使用 EDA 模擬軟件以評估生產情況的設計服務公司。EDA 工具也應用在現場可編程邏輯門陣列的程序設計上。 ^[1]