フォーマル検証の仕組み

まず初めに、アラームを発生するための条件を回路内部にアサーションで定義します。
FIFOのオーバーフローやステートマシンのデッドロックなどの基本的な検証項目は、ツールが回路を分析し、
自動でアサーションを生成します。
その他の重要な仕様は設計者や検証者がアサーションで定義します。

フォーマル検証ツールは “論理を理解できる” ので、回路の論理をバックトレースしながら、条件に該当する論理が起こり得るかを検証します。

例えば、図１ の CM4 のピン B が “H” になると違反（不具合になる）だとアサーションで定義します。
フォーマル検証ツールは論理を理解できるので、CM4 のピン B が “H” になるには、CM3 の A ピンが “H”、C ピンが “L” になる必要があると判断できます。
更に、そのためにはCM1のピンAが“L”、CM2のピンBが“L”になる必要があると判断できます。
入力ピンまで論理が辿り着いたので、このパターンのテストベンチで不具合が起こることが分かります。

逆に、CM1 のピン A と CM2 のピン B が “L” になる条件が無いのなら、この不具合は起こり得ないと証明できます。

フォーマル検証はシミュレーションや実機検証のように、全ての状態（アサーションを満たす）を検証する “完全証明”以外に、
誤動作（アサーションを違反する）を検証する“反証”を行うことが出来ます。

誤動作の方が正常動作よりも組み合わせ数が少ないので、誤動作を調べる“反証”の方が“完全証明”よりも高速に検証できます。

シミュレーションで使うテストベンチが全ての内部状態の組み合わせを網羅していることを証明することは困難ですが
フォーマル検証なら、アサーションで定義した現象が“起こらない”ことを簡単に証明できます。

フォーマル検証の特長

・テストパターンは不要 ⇒ 設計初期から設計者が自ら検証できる
・論理シミュレーションの実行は不要
・フォーマル検証は論理シミュレーションよりも解析が早い
・“起こらないこと”を証明できる

フォーマル検証の弱点

・段数が多くなると入力ピンまでのパスが複雑になる⇒出力に近い側のアサーション解析には時間がかかる

論理シミュレーションは出力に近い側の不具合が見つかりやすいので、シミュレーションを使った検証とフォーマル検証を併用すると検証の穴を小さくできます。
実機検証は想定外の使い方による不具合に弱いので、フォーマル検証を実機検証と組み合わせても効果的です。

その他に、フォーマル検証ツールはリントチェックであるデッドコード検出などのRTL検証やカバレッジの高いテストベンチを自動で生成する機能があります。 論理を理解できるので普通のリントチェックよりも高度な検証ができます。