形式的検証とは、設計、仕様とも数学的モデルで表現し数学的推論により正しさを検証する、シミュレーションを実行しない静的検証手法です。
形式的検証には、等価性検証とプロパティ検証があります。
プロパティ検証では、「基準時間の事象と、同サイクル或いは有限サイクル（固定）の事象との間の論理関係」が全ての時間にわたって成立することを証明します。

時間が一意に決まらないシーケンス動作は記述できないことに注意が必要です。 例えば、「Aが成立後、いつかBが成立する」等 無限の時間は扱えません。

形式的検証で全ての機能を検証することは現実的ではありませんが、例えばランダム検証と組み合わせることで、検証時間を短縮し機能カバレッジを上げることができます。
内蔵された乗算器を形式検証により 証明済みとすることで、加算器への入力信号のデータパターンをカバレッジ収集対象外にでき、また、ランダム検証の未カバー領域を排除することで、シミュレーション時間を短縮することができます。
ＯＫＩネットワークＬＳＩがご提供する最新の検証技術を是非ご活用ください。