Datasheet VC Formal 次世代フォーマル検証 概要 検証の課題と最新のフォーマル検証 SoC デザインの複雑化が続く中、検証 複雑なチップおよびシステムの検証は非常に困難なタスクであり、検証 とデバッグを短期間で完了し、全体的な 期間の短縮、予測性の向上、デバッグの迅速化につながる手法がエンジ スケジュールを圧縮してスケジュールの ニアとマネージャの双方から強く求められています。この問題を解決 予測性を高めるには、これまでとは違った する 1 つの方法として、設計サイクルのなるべく早い段階でバグを 新しい 検 証 手 法 が 必 要 で す。 次 世 代 発見するというアプローチがあります。バグを早い段階で特定できれば、 フォーマル検証ツールの VC Formal は、 バグの選別、デバッグ、修正にかかる労力と時間とコストを抑えられます。 現 在 の 最 も 複 雑 な SoC デ ザ イ ン の そこで問題となるのが、シミュレーションでは見つけにくいバグ、つまり 検証に対応する容量、速度、柔軟性を 事前に想定するのが非常に困難なコーナーケースのシナリオで発生 備えているほか、優れた解析、フィルタ、 するバグをどのようにして見つけるかという点です。この問題を解決する デバッグ手法も採用しており、短時間で のが形式（フォーマル）検証手法です。形式検証手法では、ユーザー ルートコーズ解析が行えます。さらに、 がシナリオを考えてバグをトリガしなくてもバグを見つけることができ シミュレーション環境が完成する前の ます。そして、業界をリードするデバッグ・ツールおよびメソドロジと 早期段階で VC Formal を利用すれば、 組み合わせることにより、フォーマル検証本来の威力を存分に引き出す 全体的なスケジュールの短縮も可能です ことができます。 （図 1）。 VC Formal デザイン VCスタティック/フォーマル・テクノロジ Formal LP CDC Lint インテリジェントな解析、レポート、デバッグ機能 RTL ユーザー 定義 アサーション （最高の精度、誤検出の少ないレポート、統一されたデバッグ環境） データベースとエンジンを刷新 （パフォーマンスと容量が3∼5倍に向上） ユーザー 定義制約 条件 プロパティの 証明に成功 VC Formal プロパティ/ カバレッジ レポート 限定的証明 プロパティの 証明に失敗 エンジン HW推論、言語サポート、TCLスクリプト （DC、PrimeTime、VCS共通の環境を拡張） シミュレーション用 アサーション VC Formalでのデバッグ （回路図パス ブラウズを含む） 図1：VC Formalによる次世代フォーマル検証 VC Formal 次世代フォーマル検証 1 形式検 証手法は、単独またはシミュレーションと組み なります。この結果、デザインの品質が向上し、全体的 合わせてデザインを解析できます。プロジェクトのスケ なスケジュールも短縮され、予測性が向上します。 ジュール終盤、あるいは実チップの製造後にデザインの 不具合が見つかると、非常に長時間かつ困難なデバッグ VC Formal を強いられ、変更には膨大なコストがかりますが、形式 VC Formal は容量と処理性能を高めたフォーマル検証 検証手法ならこうしたバグも早期段階で見つけることが ソリューションで、クラス最高のアルゴリズム、メソ できます。設計サイクルの早い段階で形式検証手法を ドロジ、データベース、ユーザー・インターフェイス 適用すると、機能の正しさや完全性といった RTL の問題 を備えています。このソリューションは、現在の最も を、シミュレーション・テスト環境の完成を待たずにいち 困難な検証タスクに対応できるよう、まったくゼロから 早く見つけることができます。 設計されており、現在の市場で最新かつ最高のフォー シミュレーション環境が完成したら、形式検証手法と シミュレーションを組み合わせてさらに解析を実行す ることで、結果品質が向上します。SoC のコネクティ ビティの正しさと完全性を検証し、デザインの 2 つの マル検証エンジンを搭載しています。 主な機能と利点 ▶ アサーション・ベース検証 バージョン同士、あるいはデザインとその高位 C/C++ SVA/PSLで記述したプロパティまたはアサーションを モデルを比較して不一致部分を切り出すなどの手法を 証明によって形式的に検証。シミュレーション環境が 使用します。 完成する前でも、想定されるデザインのすべてのアク 設計および検証プロセスの適切な時点で形式検証手法 を適用することにより、通常ならプロジェクトの終盤 にならないと見つからない発見の困難なバグさえも、 プロジェクトの非常に早い段階で発見できるように ティビティに対して動作を確認できます。高度なアサー ション可視化、およびプロパティのブラウズ、グループ 化、フィルタリング機能により、検 証 結果にも簡単 かつ簡潔にアクセスできます。 VC Formalコネクティビティ・チェック デザイン RTL ユーザー 定義 アサーション プロパティ/ カバレッジ レポート VC Formal エンジン 接続あり ユーザー 定義制約 条件 接続なし VC Formal でデバッグ 図2：先進のデバッグ・インターフェイス 図4：コネクティビティ・チェック リセット・シーケンス 制約条件 エンジン制御 エンジン・サマリ 実行 ステータス ゴールデンRTL 変更後のRTL VC Formal シーケンシャル等価性チェック VC Formalエンジン COI 解析 図3：対話型操作 2 デバッグ カウンタの例 結果 レポート 図5：シーケンシャル等価性チェック VC Formal 次世代フォーマル検証 プロパティ+ 制約条件 RTL Certitude （フォルトを挿入） 少なくとも1つの 証明に失敗 RTL VC Formal （証明） すべての証明に成功 フォーマル 検証環境の抜け 図6：シノプシスの検証品質確認システムCertitudeとの統合 ▶ 先進のデバッグ 回路図への値のアノテーションによるコネクティビ ティ・チェックなど、業界標準の RTL および波形表示 ソ リ ュ ー シ ョ ン を ベ ー ス に し た 先 進 の デ バ ッ グ・ インターフェイス（図 2）。 ▶ 対話型操作 アサーションと制約条件のリアルタイム編集、インクリ メンタルなビルドと解計算、証明進捗フィードバックなど ▶ 制約条件の不足や誤りといったフォーマル検証環境の 弱点を見つけることができます（図 6）。 ▶ フォーマル・スコアボード データパス・デザインのデータ保全性を網羅的に検証。 デザインを通 過する間、データの消失、順 序 変 更、 破損、重複が発生しないことを確認します。 の 機 能 を 用 意。 再 起 動しなくて も VC Formal の 独自の価値 動作を即座に理解、制御できます（図 3）。 ▶ 業界をリードするパフォーマンスと容量 SoC レベルのコネクティビティ・チェック フルチップ SoC レベルでコネクティビティをチェック。 柔軟な入 力フォーマットにより、フロー統合も容易 です。値のアノテーション、回路図ビュー、ソースコー ド・ブ ラウザ、解 析レポートなど、強 力なデバッグ 機能により、解析が短時間で完了します。接続に問 題のある部分は自動でル ートコーズ解 析が 行われる ため、デバッグ時間が大幅に短縮します（図 4）。 ▶ シーケンシャル等価性チェック 従 来に比べ大 幅に強 化された 次 世代の 等 価 性 チェック・エンジンにより、これまでの一般的なフォー マル検証では扱えなかったブロックやデザインも比較 が 可能となりました。パワー・ゲーティング挿入後 や合成リタイミング後でもデザインを比較できます （図 5）。 ▶ 測定値といった重要な情報が得られ、プロパティや Certitude との統合 Certitude は、フォーマル検 証環境の評価に役 立つ 貴 重な情 報を提 供します。VC Formal と Certitude を統合すると、フォーマル IP サインオフの一部として フォーマル検証環境におけるプロパティ・カバレッジ VC Formal 次世代フォーマル検証 –– パフォーマンスと容量が 5 倍以上向上し、大規模 なデザインでも効率よく実行可能。 ▶ 導入から利用までが簡単 –– シノプシスのインプリメンテーション・ツール との親和性が高いモデルとコマンドを採用。VC Formal のスクリプトは Design Compiler の TCL スクリプトとほぼ共通です。 ▶ 実行制御 –– グリッド表示、一時停止 / 再開、保存 / 復元などの 機能を利用できます。 ▶ 回路図への値のアノテーションやルートコーズ 解析などの優れたコネクティビティ・チェック 機能 –– 接続されていないネットのデバッグなど、大幅に 改良された最先端のデバッグ。 ▶ エンジンの解析と制御 –– 実行中のエンジンの動作をリアルタイムに検査・ 制御でき、きわめて困難な形式的問題もより確実 に収束します。 3 まとめ 設計および検証プロセスの適切な時点で次世代フォー デザイン検証の効率を改善するため、高度なフォーマル 検証手法の採用が急速に広がっています。VC Formal は SoC コネクティビティ・チェック、不定値 X の伝播、 マル検証を適用することにより、発見の難しいバグ も検証スケジュールの非常に早い段階で捉えること ができ、デザインの品質向上、全体的なスケジュール シーケンシャル等価性チェックなどの検証タスクを の短縮、予測性の向上につながります。 自動化しており、これまでよりもはるかに容易にフォー シノプシスの製品、サポート・サービス、トレーニングの マル検証手法を導入できます。また、スクリプト環境 詳細は、シノプシスのウェブサイト とセットアップが共通化されているため、以前に作成 www.synopsys.com/japan したスクリプトにいくつかの新しいコマンドを追加 をご参照ください。 するか、GUI 画面でマウスをクリックするだけで新しい フォーマル検証アプリケーションを追加、起動でき ます。業界標準の VCS シミュレーションおよび Verdi デバッグ・ソリューションと統合すれば、フォーマル 検証本来の威力を存分に引き出すことができます。 日本シノプシス合同会社 〒158-0094 東京都世田谷区玉川2-21-1 二子玉川ライズ オフィス 〒531-0072 大阪府大阪市北区豊崎3-19-3 ピアスタワー13F TEL.03-6746-3500 (代) FAX.03-6746-3535 TEL.06-6359-8139(代) FAX.06-6359-8149 © Synopsys, Inc. All rights reserved.Synopsysは、米国およびその他の国におけるSynopsys, Inc.の商標です。 シノプシスの商標一覧は、http://www.synopsys.com/Company/Pages/Trademarks.aspx をご参照ください。その他の名称は、各社の商標または登録商標です。 05/14.RP.CS4318.
© Copyright 2024 ExpyDoc
