アサーションベース検証

アサーションベース検証(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を広く深くサポートしています。QuestaQuesta Formal VerificationVeloceなどのコア検証ツールですべての標準アサーションライブラリと言語がサポートされているだけでなく、アサーションに直接関係するデバッグやカバレッジなどにもそれぞれ専用のサポートが提供されています。

 

製品

Questa Advanced Simulator

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

Questa Formal Verification

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

Veloce2

Veloce2は、設計プロセスのすべての段階でブロックレベルおよびSoC全体のRTLシミュレーションを高速化します。 詳細

製品情報リクエスト