Questa Formal Verification

シミュレーションベースのRTL設計検証を補完

Questa Formal Verificationは、設計上考えられるすべての動作を解析し、潜在するエラー状態を検出することで、シミュレーションベースのRTL設計検証を補完します。この徹底した解析により、重要な制御ブロックがどんな場合にも正しく動作することを保証し、シミュレーションで見落とされた可能性のある設計エラーを確実に検出します。

 

Questa Formal Verificationは、設計の完了後すぐに使用できるため、統合前にブロックをデバッグし、シミュレーションテスト環境が使用可能になるよりかなり前に、潜在するエラーを検出できます。共通言語のフロントエンドをQuesta Simulatorと共有しており、Unified Coverage Database(UCDB)とも統合されているので、バグ検出、エラー修正、カバレッジクロージャの達成を加速化する完璧なツールです。

概要

Questa Formal Verificationの動作方法

Questa Formal Verificationは、設計の動作を解析し、初期ステートから到達する可能性のあるすべての設計ステートを特定します。この解析では、横型方式でステートスペース全体を探索し、逆にシミュレーションでは縦型方式を使用します。
そのため、Questa Formal Verificationは、バグを検出するためのスティミュラスを必要とせず、潜在する設計エラーを発見できます。これにより、検証済みの設計には、すべての正当な入力シナリオで一切バグがないことを保証します。同時に、このアプローチは到達不可能なカバレッジポイントを識別するため、カバレッジクロージャ達成までの時間を短縮します。

自動プッシュボタンエラー検出

Questa Formal Verificationは、共通する多数の設計エラーを自動チェックする使いやすい機能を提供しています。設計者は、Questa Formal Verificationを使用して、簡単に新しいコードをチェックし、浮いたバスまたは多重駆動バス、組み合わせ回路のループ、数学的エラー、初期化などの機能的な問題を検出できます。新しいコードを設計に統合する前に、これらのエラーを検出し修正できるため、検出が困難なバグがより大規模なシステムに入り込んでしまうのを防ぎ、それ以降の工程での検証に要する時間を短縮できます。これらのチェックは、到達可能なステートスペースの正確な解析に基づいており、検出されたエラーは実際のエラーです。通常の単純なリントチェッカで生成される信憑性の低い結果とは異なります。

アサーションベースのフォーマル検証

また、Questa Formal Verificationは、設計が特定の機能要件を満たしていることを保証することを目的とした、汎用的なアサーションベースのフォーマル検証をサポートしています。マルチクロックアサーションを含め、PSL、SVA、OVLをサポートするQuesta Formal Verificationは、非常に大規模な設計でも多数のアサーションを使用して簡単に検証できます。複数のハイキャパシティなフォーマルエンジンが連携動作して、検証をより短時間で完了します。Questa Formal Verificationは、アサーションの失敗をより容易にデバッグするために、Questa Simulatorに統合されます。

製品情報リクエスト