フォーマル検証

出典: くみこみックス

フォーマル検証（フォーマルけんしょう） 【Formal Verification】

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

【出典】（株）アルティマ 技術統括部 一同，下馬場 朋禄，山際 伸一，横溝 憲治；システム開発者のためのFPGA用語集，Design Wave Magazine 2008年12月号 別冊付録，CQ出版社，2008年12月．