VC Formal

機能と利点

• アサーションベースのプロパティ検証（FPV）: SystemVerilog Assertion (SVA）プロパティを検証するためのフォーマル証明ベースの技術で、シミュレーション環境が用意される前の、考えられるすべての設計活動にわたって正しい操作が行われていることを保証します。高度のアサーション可視化、プロパティ走査検索、グループ化およびフィルタリング機能により、簡素で一貫した形で結果を表示できます。

• 自動抽出されたプロパティのチェック（AEP）: 専用のテストを使用することなく、境界外配列、算術オーバーフロー、X割り当て、値設定/再設定の同時実行、フルケース、パラレルケースの解析、マルチ・ドライバーや競合しているバスおよびフローティング・バスのチェックを実行する自動機能解析。

• フォーマルなカバレッジ解析（FCA）: シミュレーション・フローを完了するため、VC Formalはカバレッジ目標に到達しなかった箇所を発見、また実際に到達不可能だったことを証明し、その箇所をその後の解析から排除して、人手による工数を大幅に節減できます。

• SoCレベルの接続性チェック（CC）: SoCレベルでの接続性の検証。統合を簡易化する柔軟な入力形式。値のアノテーション、スケマティック・ビュー、ソース・コード走査検索を含む強力なデバッグ機能と解析レポートが解析を高速化します。接続性が切断されている場合の根本原因を自動的に解析し、デバッグ時間を大幅に短縮できます。

• シーケンシャル等価性チェック（SEQ）: これにより、レジスタ・リタイミング、パワー最適化のためのクロック・ゲートの挿入、またマイクロアーキテクチャの変更などの前後に設計を比較できます。

• フォーマル・ナビゲータ（NAV）: Unified Verdi GUIでは、アサーションやテストベンチを使用、もしくは使用せずにRTL設計のみでwhat-if解析とデバッグを行えます。

• レジスタ検証（FRV）: 「読み取り専用」、「読み取り/書き込み」または「値のリセット」などの各属性の構成レジスタの動作をフォーマル検証でき、ダイレクト・テストの必要がありません。

• Certitudeと統合されたFormal Testbench Analyzer（FTA）: Testbench Quality Assuranceは、フォーマル環境の品質を評価する独自の機能を持っています。Testbench Quality Assuranceと VC Formalはネイティブ統合されているため、フォーマル・サインオフの一環として、意味のあるプロパティ・カバレッジ測定値を提供でき、欠損または不正なプロパティや制約などの弱点を特定します。ネイティブ統合により、スタンドアロンの故障インジェクション方法に比較してパフォーマンスが5～10倍速くなります。

• セキュリティ検証（FSV）: セキュアなデータがセキュアでない宛先に到達しないことをフォーマル検証し、セキュアでないデータがセキュアな宛先を上書き（または到達）しないというデータ整合性を確認できます。

• アサーションIP（AIP）: 標準バス・プロトコルの検証のための高パフォーマンスおよび最適化されたアサーションIPで、シノプシスのVC FormalソリューションとVCSシミュレーションで使用可能です。

• 高度のデバッグおよび双方向性: スケマティックのバリュー・アノテーション、オンザフライ・アサーション、制約編集、証明状況フィードバック、および影響解析など、Unified Verdi GUIベースのRTL上で構築された高度のデバッグ・インターフェイスおよび波形可視化ソリューションを利用して、ユーザーは可視性と制御性を向上できます。

• フォーマル・スコアボード: データ・パス設計のデータの整合を徹底的に検証します。データが損失、並び替え、破壊、複製されることなくデザイン内を伝達されることを確認します。

• フォーマル・カバレッジ: 高度のテクノロジにより、プロパティ検証のサインオフを達成するためのフォーマル・メトリクスおよびメソドロジーが可能になります。