アサーションベース検証

アサーションベース検証（ABV）は、設計の意図を確認するためのアサーションを挿入し、シミュレーション、フォーマル検証、エミュレーションのいずれかの方法によって、設計意図が正しく実装されているかどうかを検証する手法です。

簡単な例として、回路内のブロックにFIFOを実装する場合を考えてみます。ABV手法では、設計者が設計意図（この場合はFIFOのオーバーフローもアンダーフローも発生しないこと）を確認するためのアサーションを定義し、シミュレーション、フォーマル検証、エミュレーションのいずれかの方法によってFIFOが正しく実装されているかどうかを検証します。

アサーションをサポートした言語やツールは広く出回っているため、多くの設計者や検証エンジニアがABVを導入して設計品質や検証生産性の向上を図っています。また、アサーションはデバッグ工程にも大きな利点があることが知られるようになっています。

メンター・グラフィックスの包括的なABVフローでは、シミュレーション、フォーマル検証、エミュレーション、FPGAベースのプロトタイピングなどでアサーション・ライブラリやユーザ定義アサーションを利用でき、収集したカバレッジ・データはQuestaのUCDB（Unified Coverage DataBase）というカバレッジ・データベースに保存されます。

ABV手法は段階的な導入が可能なため、既存の検証フローにも容易に採用できます。特に、アサーション・ライブラリを使用すれば、どのようなプロジェクトにも簡単にABVを取り入れることができます。QuestaおよびQuesta Formal Verificaionには充実したアサーション・ライブラリが用意されているため、高付加価値のアサーションを手軽に挿入して、ただちに効果が得られるので、最初のプロジェクトから高いROIを達成できます。

利点

  • アサーションが回路（またはテストベンチ）を能動的に監視し、機能の正しさを保証
  • アサーションは設計のエラーを原因付近で検出できるため、観測性が大幅に向上し、デバッグ時間の短縮に貢献
  • SVA（SystemVerilogの一部）やPSLなどのアサーション言語は標準化されているため、現在ではABV手法は幅広いツールでサポートされており、Verilog、SystemVerilog、VHDLベースの設計で利用可能
  • メンター・グラフィックスのQuestaやQuesta Formal Verificaionにはどちらも充実したアサーション・ライブラリが用意されており、このライブラリを使用することによってABVの手軽な導入が可能
  • アサーションは、シミュレーション、フォーマル検証、エミュレーションで利用できるため、高いROIを達成可能

メンター・グラフィックスによるABVのサポート

メンター・グラフィックスの機能検証ソリューションは、ABVを広く深くサポートしています。Questa、Questa Formal Verificaion、Veloceなどのコア検証ツールでは、標準のアサーション・ライブラリと言語がすべてサポートされているだけでなく、アサーションに直接関係するデバッグやカバレッジなどにもそれぞれ専用のサポートが提供されます。

 

データシート

ツールボックス

製品

Questa

メンター・グラフィックスが提供する先進の検証環境Questaは、検証フローの品質、生産性、予測性を改善する唯一の統合検証プラットフォームです。

Questa Formal Verification

Questa Formal Verificaiソリューションは業界トップクラスのキャパシティとパフォーマンスを誇り、発見が極めて困難なバグも確実に検出します。

Veloce

組込システムおよびSoC設計の検証を処理する高性能、高精度、ハイ・キャパシティのハードウェア支援検証ソリューションです。