フォーマル検証は、シミュレーションとは異なるアプローチでチップの動作を検証します。フォーマル検証では、スティミュラスではなくアサーション（詳しくはアサーションベース検証手法を参照）を使用するため、テストベンチを作成する必要がありません。そして高度な数学的解析技術を利用して、設計の動作に関するこれらのアサーションの真偽を証明します。多くの場合、アサーションが真であることはフォーマル検証によって形式的に証明できるので、これによって設計が正しく動作することを検証することができます。

0-In Formal Verificationソリューションは業界トップクラスのキャパシティと性能を誇り、発見が極めて困難なバグも確実に検出します。豊富なモニタとアサーションを含む充実したアサーション・ライブラリを備え、各種シミュレーション環境にも緊密に統合できる最先端フォーマル検証ツールの0-In Formal Verificationは、全体的な検証品質を高め、極めて発見の困難な致命的バグの検出を可能にします。

0-In Formal Verificationではテストベンチが不要なため、RTLコードが利用可能になった時点ですぐに利用できます。通常、アサーションは豊富なアサーション・ライブラリから追加するか、エンジニアがSystemVerilogまたはPSLを用いて記述します。これらのアサーションによって、設計のプロパティやRTLブロックのインタフェースに対する制約条件を指定します。設計者は、充実したデバッグ環境を利用して設計のプロパティを証明したり、0-In Formal Verificationによって検出された機能上の問題の根本原因を見つけることができます。

フォーマル検証はシミュレーションを補完するものです。メンター・グラフィックスのソリューションではフォーマル検証とシミュレーションの結果はどちらもUCDB（Unified Coverage Database）に記録され、このデータベースを通じて豊富な検証管理機能を利用できます。