VC Formal 

次世代フォーマル検証 

概要
SoCデザインの複雑化が続く中、検証とデバッグを短期間で完了し、全体的なスケジュールを圧縮してスケジュールの予測性を高めるには、これまでとは違った新しい検証手法が必要です。次世代フォーマル検証ツールのVC Formalは、現在の最も複雑なSoCデザインの検証に対応する容量、速度、柔軟性を備えているほか、優れた解析、フィルタ、デバッグ手法も採用しており、短時間でルートコーズ解析が行えます。さらに、シミュレーション環境が完成する前の早期段階でVC Formalを利用すれば、全体的なスケジュールの短縮も可能です(図1)。

VC Formal データシート

VC Formal

検証の課題と最新のフォーマル検証
複雑なチップおよびシステムの検証は非常に困難なタスクであり、検証期間の短縮、予測性の向上、デバッグの迅速化につながる手法がエンジニアとマネージャの双方から強く求められています。この問題を解決する1つの方法として、設計サイクルのなるべく早い段階でバグを発見するというアプローチがあります。バグを早い段階で特定できれば、バグの選別、デバッグ、修正にかかる労力と時間とコストを抑えられます。そこで問題となるのが、シミュレーションでは見つけにくいバグ、つまり事前に想定するのが非常に困難なコーナーケースのシナリオで発生するバグをどのようにして見つけるかという点です。この問題を解決するのが形式(フォーマル)検証手法です。形式検証手法では、ユーザーがシナリオを考えてバグをトリガしなくてもバグを見つけることができます。そして、業界をリードするデバッグ・ツールおよびメソドロジと組み合わせることにより、フォーマル検証本来の威力を存分に引き出すことができます。

形式検証手法は、単独またはシミュレーションと組み合わせてデザインを解析できます。プロジェクトのスケジュール終盤、あるいは実チップの製造後にデザインの不具合が見つかると、非常に長時間かつ困難なデバッグを強いられ、変更には膨大なコストがかりますが、形式検証手法ならこうしたバグも早期段階で見つけることができます。設計サイクルの早い段階で形式検証手法を適用すると、機能の正しさや完全性といったRTLの問題を、シミュレーション・テスト環境の完成を待たずにいち早く見つけることができます。

VC Formal for next-generation formal verification

新しいフォーマル検証アプリケーションを追加し、SoCのコネクティビティの正しさと完全性を検証し、RTLデザインの2つのバージョンを比較して不一致部分を切り出すことができます。

シミュレーション環境が完成したら、フォーマル検証手法とシミュレーションを組み合わせてさらに解析を実行することで、例えばカバレッジ目標の設定が妥当かどうかなども検証でき、結果品質が向上します。

設計および検証プロセスの適切な時点でフォーマル検証手法を適用することにより、通常ならプロジェクトの終盤にならないと見つからない発見の困難なバグさえも、プロジェクトの非常に早い段階で発見できるようになります。この結果、デザインの品質が向上し、全体的なスケジュールも短縮され、予測性が向上します。

VC Formal
VC Formalは容量と処理性能を高めたフォーマル検証ソリューションで、クラス最高のアルゴリズム、メソドロジ、データベース、ユーザー・インターフェイスを備えています。このソリューションは、現在の最も困難な検証タスクに対応できるよう、まったくゼロから設計されており、現在の市場で最新かつ最高のフォーマル検証エンジンを搭載しています。

主な機能と利点

  • アサーション・ベース検証
    SVAで記述したプロパティまたはアサーションを証明によって形式的に検証。シミュレーション環境が完成する前でも、想定されるデザインのすべてのアクティビティに対して動作を確認できます。高度なアサーション可視化、およびプロパティのブラウズ、グループ化、フィルタリング機能により、検証結果にも簡単かつ簡潔にアクセスできます。
  • 先進のデバッグ
    回路図への値のアノテーションによるコネクティビティ・チェックなど、業界標準のVerdiベースのRTLおよび波形表示ソリューションをベースにした先進のデバッグ・インターフェイス(図2)。

Advanced debug interface

  • 対話型操作
    アサーションと制約条件のリアルタイム編集、証明進捗フィードバック、円錐状影響圏を使った解析などの機能を用意し、すぐれたビジビリティと操作性を提供します(図3)。
  • Interactivity

  • SoCレベルのコネクティビティ・チェック
    フルチップSoCレベルでコネクティビティをチェック。柔軟な入力フォーマットにより、フロー統合も容易です。値のアノテーション、回路図ビュー、ソースコード・ブラウザ、解析レポートなど、強力なデバッグ機能により、解析が短時間で完了します。接続に問題のある部分は自動で根本的原因の解析が行われるため、デバッグ時間が大幅に短縮します(図4)。
  • Connectivity checking

  • シーケンシャル等価性チェック
    パワー・ゲーティング挿入後や、マイクロアーキテクチャの変更後でも、デザインを比較できます(図5)。
  • フォーマル・カバレッジ解析
    シミュレーション・フローを補完する形で、フォーマル検証技術がカバレッジの目標と対象ポイントの現実性を検証、証明し、非現実的なポイントがあればその後の解析から省くことができます。これにより、多大な労力を節約できます。
  • Sequential equivalency checking

  • Certitudeとの統合
    Certitude™ は、フォーマル検証環境の評価に役立つ貴重な情報を提供します。VC FormalとCertitudeを統合すると、フォーマルIPサインオフの一部としてフォーマル検証環境におけるプロパティ・カバレッジ測定値といった重要な情報が得られ、プロパティや制約条件の不足や誤りといったフォーマル検証環境の弱点を見つけることができます(図6)。
  • Integration with Synopsys' Certitude functional qualification system

  • フォーマル・スコアボード
    データパス・デザインのデータ保全性を網羅的に検証。デザインを通過する間、データの消失、順序変更、破損、重複が発生しないことを確認します。

類例のない特長

  • 業界をリードするパフォーマンスと容量

    パフォーマンスと容量が5倍以上向上し、大規模なデザインでも効率よく実行可能。

  • 導入から利用までが簡単

    シノプシスのインプリメンテーション・ツールとの親和性が高いモデルとコマンドを採用。VC FormalのスクリプトはDesign CompilerのTCLスクリプトとほぼ共通であり、主なコマンドは共通です。

  • 実行制御

    グリッド表示、一時停止/再開、保存/復元などの機能を利用できます。

  • 回路図への値のアノテーションやルートコーズ解析などの優れたコネクティビティ・チェック機能

    接続されていないネットのデバッグなど、大幅に改良された最先端のデバッグ。

  • エンジンの解析と制御

    実行中のエンジンの動作をリアルタイムに検査・制御でき、きわめて困難な形式的問題もより確実に収束します。

まとめ
デザイン検証の効率を改善するため、高度な形式(フォーマル)検証手法の採用が急速に広がっています。VC FormalはSoCコネクティビティ・チェック、不定値Xの伝播、フォーマル・カバレッジ解析、シーケンシャル等価性チェックなどの検証タスクを自動化しており、これまでよりもはるかに容易にフォーマル検証手法を導入できます。また、スクリプト環境とセットアップが共通化されているため、以前に作成したスクリプトにいくつかの新しいコマンドを追加するか、GUI画面でマウスをクリックするだけで新しいフォーマル検証アプリケーションを追加、起動できます。業界標準のVCS®シミュレーションおよびVerdiデバッグ・ソリューションと統合すれば、フォーマル検証本来の威力を存分に引き出すことができます。

設計および検証プロセスの適切な時点で次世代フォーマル検証を適用することにより、発見の難しいバグも検証スケジュールの非常に早い段階で捉えることができ、デザインの品質向上、全体的なスケジュールの短縮、予測性の向上につながります。

シノプシスの製品、サポート・サービス、トレーニングの詳細は、シノプシスのウェブサイトwww.synopsys.com/japanをご参照ください。



NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideosTraining Courses