Questa Formal Assertion Library

 高性能フォーマル解析用に最適化されたアサーションベースの検証IP

Questa Formal Assertion Libraryは、Questa Property Checking (PropCheck)を使用して業界標準プロトコルに準拠している設計かどうかを検証するためのSVA(SystemVerilog Assertion)パッケージとサンプルを提供します。

購入したIPの検証

複雑な標準規格のインタフェースを多用する今日の設計では、IPの相互運用性とシステム動作を正しく検証しなければなりません。IPを修正せずにそのままを使用する場合でも、最終製品を差別化するためにカスタマイズする場合でも、事前には想定できなかった問題がインタフェースを統合したタイミングで発生することがあります。非常に成熟したIPでも同様です。これに加えて、経験豊富な開発者でもIP仕様を誤解したり、数多くのプロトコルパラメータのコンフィギュレーションを誤ったりして、エラーや時間の無駄を招くことさえあります。

Questa Formal Assertion Library  

Questa Formal Assertion Libraryには汎用的な業界標準プロトコルに準拠したSVA(SystemVerilog Assertion)パッケージとサンプルが用意されています。このパッケージとサンプルはQuesta Property Checking (PropCheck)のフォーマルベース検証用に最適化されています。

ソリューション: Questa Formal Assertion Library

Questa Formal Assertion Libraryは、メンター・グラフィックスのノウハウを結集して汎用的な標準インタフェースに対応した再利用可能アサーションをパッケージ化したものです。このライブラリを使用することで検証品質の向上と期間短縮を達成できます。
RTL記述とアサーション記述さえ準備できればすぐにQuesta Property Checking (PropCheck)によるフォーマル検証をスタートできるので、設計者はBFM(Bus Functional Model)、検証コンポーネント、検証IP(VIP)を独自に構築する手間をかけることなく、設計の差別化や付加価値の作り込みに専念できます。

IPが修正されて使われた場合、標準プロトコルをカスタマイズした部分や拡張した部分がプロトコルの基本部分への違反を起こさないことを確認したり、想定外のコーナーケースを発生させたりしないことを網羅的に確認するために、アサーションベースIPを使用したフォーマル検証も必要になります。

Questa Formal Assertion LibraryをQuesta Verification Platformと組み合わせることで、包括的なVIPコンポーネントによって検証準備の時間短縮と早期のカバレッジクロージャを達成できます。
Questaのフォーマル検証ツールを使用すると、プロトコルアサーション一式を使って設計の正しさを網羅的に検証できます。一方、Veloceエミュレーションシステムを使用すると、高性能なシミュレーションを加速させ、スループットを桁違いに向上させます。

特長

  • Questa Formal AMBA Libraryファミリがサポートするプロトコル: AMBA2(APB2、AHB2)、AMBA3(APB3、AXI3)、AMBA4
  • IEEE標準規格のSVA(SystemVerilog Assertion)で記述されたアサーションを高性能なQuesta Formalアプリケーション(Questa PropCheckQuesta AutoCheck)用に最適化
  • 既存のフォーマルベースのカバレッジドリブン検証フローに基づいて、検証結果をQuesta Verification Managementと連動可能

利点

  • 立ち上げ時間の短縮によるTime-to-Marketの改善と標準インタフェースのカバレッジクロージャを早期化
  • カスタマイズしたプロトコルが意図したとおりに元のプロトコルを補完していることをフォーマルに証明

 

製品情報リクエスト