アサーションベース検証

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

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

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

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

ABV手法は、段階的な導入が可能なため、大半の既存の検証フローに容易に導入できます。特に、アサーション・ライブラリを使用すれば、どのようなプロジェクトにも簡単にABVを取り入れることができます。QuestaおよびQuesta Formal Verification製品には豊富なアプリケーション・ライブラリが用意されているため、価値の高いアサーションを設計に取り入れて、即座に効果が得られるので、最初のプロジェクトから高いROIを達成できます。

利点

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

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

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

よりスケーラブルな検証メソドロジ

 

データシート

ツールボックス

製品

Questa Advanced Simulator

Questa Advanced Simulatorは、高性能でハイ・キャパシティなシミュレーションと統一された最先端のデバッグ機能を組み合わせることで、Verilog、SystemVerilog、VHDL、SystemC、PSL、UPFのもっとも完全に近いネイティブなサポートを提供します。

Questa Formal Verification

Questa Formal Verificationツールは、設計について考えられるすべての動作を分析し潜在するエラー状態を検出することで、シミュレーションベースのRTL設計検証を補完します。

Veloce

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