Questa Property Generation(PropGen)

シミュレーション、フォーマル検証、ハードウェア支援検証における
アサーションベース検証を自動化

Questa Property Generation (PropGen)は、RTL記述とテストベンチから可読性の優れたSVA(SystemVerilog Assertion)プロパティを自動で生成してアサーションベース検証を自動化するアプリケーションです。形式的仕様記述言語やプロパティ言語に馴染みのないエンジニアであっても、わずかな時間でIPを評価できます。IPのRTL記述と生成されたSVAプロパティを使用して、IPに潜む想定外の問題を特定します。また、SVAプロパティをSoC統合フローに直接取り込んで、仕様の不整合を見つけることもできます。

アサーションベース検証(ABV): あなたの代わりにアサーションを生成

アサーションベース検証(Assertion Based Verification: ABV)の利点は広く知れ渡っています。設計意図を伝えることができる実行可能な仕様書であり、問題の原因となる場所を直ちに特定でき高速のデバッグが可能です。また、ハードウェアに起因する問題をデバッグする際の可観測性が優れているといったメリットもあります。その一方で、アサーションのプロパティを手作業で記述し、管理するには専門知識が必要であり、時間もかかるため、ABVは非常に強力な手動でありながら、導入に二の足を踏むエンジニアも少なくありません。

Questa Property Generation  

Questa PropGenは、RTL記述とテストベンチから可読性の優れたSVA(SystemVerilog Assertion)プロパティを自動生成することで、アサーションベースの検証を自動化します。シミュレーション、フォーマル解析、ハードウェア支援検証の各種プラットフォームでアサーションを使用して、仕様と一致しないバグとカバレッジホールを特定します。

ソリューション: Questa Property Generation(PropGen)

Questa Property Generation(PropGen)は、RTL記述、SystemVerilogテストベンチ、生成した波形から自動的にSVAプロパティを生成するアプリケーションです。可読性の高いプロパティを使用することで設計/検証エンジニアは以下を実行できます。

  • 統合直後にアサーションが発火したSoC設計におけるIPの誤使用を素早く検出
  • カバレッジホールを特定して早期のカバレッジクロージャを達成
  • ユーザの意図したとおりに動作しないプロパティを観察し、仕様と異なるRTL記述を特定

特長

  • RTL記述、テストベンチ、波形から自動的に高品質のプロパティを作成
  • ランタイムエンジンから独立しているため、ランタイムシミュレーション、フォーマル検証ツール、アクセラレータ、エミュレーションのライセンスが不要
  • 設計意図を抽出可能
  • リグレッションスイートのカバレッジホールを特定
  • アサーションを用いてドキュメント化、設計レビュー、シミュレーション、エミュレーション、フォーマルモデルチェックに活用
  • Questa Advanced Simulator、Questaフォーマル検証エンジン、PropCheck、Veloceハードウェアアクセラレータ/エミュレータすべてと統合

利点

  • SVA言語の知識を必要とせずに、短時間に多数の貴重なプロパティを作成することができ、面倒でミスを誘発しやすい作業を削減可能
  • プロパティにより想定外の振る舞いを検出して、RTLが仕様どおりになっていない可能性を示唆
  • カバレッジホールを特定して早期のカバレッジクロージャを達成
  • 統合直後にアサーションが発火したSoC設計に含まれたIPの誤使用を素早く検出

 

製品情報リクエスト