設計の正しさを数学的な手法で静的に解析する検証技術の総称です.形式的検証とも呼ばれます.フォーマル検証には,検証対象となる設計の論理機能がリファレンスとなる設計の論理機能と等価であるかどうかをチェックする等価性検証(Equivalent Checking)と,検証対象の論理機能が与えられた仕様記述の条件(プロパティ)を満たしているかどうかをチェックするプロパティ検証(PropertyChecking)があります.例えば等価性検証では,RTL 記述と論理合成後のゲート・レベルネットリストを比較し,論理的に等価であるかどうかを確認します.現在のLSI 設計では設計期間よりも検証期間の方が長くなっています.等価性検証を利用すれば,ゲート・レベルシミュレーションで検証する場合よりも論理検証にかかる期間を大幅に短縮できます.