Questa Property Checking(PropCheck)

 

シミュレーション環境が整備される前の網羅的な検証

Questa Formal Verificationは設計統合前のブロックレベルのデバッグに使用できるため、シミュレーション環境が整う前に潜在的なエラーを検出するのに役立ちます。Questa Advanced Simulatorと同じ言語パーサーを使用し、UCDBとも統合されているので、迅速なバグの検出、RTLの機能仕様への整合、バグ修正が他への悪影響を及ぼさないことの確認、早期のカバレッジクロージャを実現できる完璧なツールです。

検証の完全性

どれほど完成度の高い制約付きランダムテストベンチでも、設計のステート空間を完璧に網羅することはできません。DUTは小規模であってもシミュレーションベースの検証だけでは不十分です。シミュレーション用テストベンチの構築には何週間もかかるので、その間にIPに複雑なバグが入り込む恐れすらあります。このため、古い仕様または仕様の誤解に基づいたバグであるか、設計ミスによるバグかにかかわらず、バグの検出が遅ければ遅いほど、バグを検出してから修正し、ほかに悪影響を与えることなくバグを正しく修正されたことを確認するのにより多くのコストがかかります。

Questa Property Checking(PropCheck)  

Questa Property Checking(PropCheck)を使用すると、意図した動作と入力信号の制約を規定するプロパティをいくつか記述するだけで、テストベンチを使わずにRTLを徹底的に検証できます。見慣れた波形インタフェースで信号パターンの正否が明示され、カバレッジの進捗レポートはAccellera標準であるUCDB形式で出力されます。

ソリューション:Questa PropCheck

Questa Property Checking(PropCheck)は一般的なアサーションベースのフォーマル検証を使用して、設計が特定の機能要求を満たしていることを検証するツールです。PSL(Property Specification Language)とSystemVerilogアサーション(SVA)、オブジェクト検証言語(OVL)をサポートし、マルチクロックアサーションにも対応しており、超大規模な設計でも多数のアサーションを使用して簡単に検証できます。また、初期ステートから到達可能なすべての設計ステートを規定したアサーションに基づき、予想と実際の振る舞いを比較解析します。

Questa PropCheckは論理の幅優先でステート空間全体を探索し、逆にシミュレーションでは論理の深さ優先で探索します。このため、バグ検出用のスティミュラスがなくても、潜在する設計エラーをすべて発見できます。これにより、検証済みの設計には、あらゆる正当な入力シナリオに対して、一切バグがないことを保証できます。同時に、このアプローチは到達不可能なカバレッジポイントを識別するため、カバレッジクロージャ達成までの時間を短縮します。

世界水準のハイキャパシティで高スループットの複数のエンジンが内蔵されており、それぞれのエンジンの強みを生かしてリアルタイムな連携が可能です。これにより、早期に検証を完結させることができます。Questa Advanced Simulatorと同じ言語パーサーを使用し、UCDBとも統合されているので、迅速なバグの検出、RTLの機能仕様への整合、バグ修正が他への悪栄養を及ぼさないことの確認、早期のカバレッジクロージャを実現できる完璧なツールです。

特長

  • アサーションベースのフォーマル検証によりテストベンチなしで徹底した検証が可能
  • 複数のフォーマルエンジンが連携動作して最大キャパシティとハイパフォーマンスを達成
  • Questa Advanced Simulatorとの統合により、アサーションで検出したエラーを容易にデバッグ
  • IEEE標準のUCDBとの統合/結果のレポートにより、フォーマル解析の結果をQuesta Verification Management経由でメインのデータベースに取込むことで、進捗や成功の度合いを電子的にコミュニケーションすることが可能
  • SVA/PSL/OVLのプロパティ、VerilogあるいはVHDLで記述されたDUTをサポート

Benefits

  • 早期のデバッグ: シミュレーション環境の整う前にブロックレベルで検証可能
  • 徹底した検証: 可能なすべてのシナリオを網羅した解析
  • カバレッジクロージャ: フォーマル解析の結果を同じツール環境内でトラック。解析結果は一元化された検証トラッキングツールにエクスポート可能
  • ポストシリコンデバッグ: 修正結果を検証するために検出された問題を再現
製品情報リクエスト