FormalityとFormality Ultra 

DC Ultraのための等価検証 

概要
Formality®はフォーマルで静的な検証技術を用いて、2つの異なるバージョンの設計が機能的に等価か否かを確認する等価検証(EC)ソリューションです。

今日の設計の規模と複雑度に加え、タイミング、面積、消費電力とスケジュールの目標に応えるという課題のためには、最新、最先端の合成最適化が検証可能であることが必要です。

FormalityはDC Ultraの合成を直接サポートし、最高の、かつ完全に検証可能な結果品質を提供します。

Formalityは電源オン/電源オフ状態の検証、多電圧、多電源およびクロックゲート設計をサポートします。

Formalityの使いやすいフローベースのグラフィカル・ユーザ・インターフェースと自動設定モードがあれば、経験の浅いユーザでも、検証を最短のスケジュールで成功に終わらせることが可能です。

PDFデータシートのダウンロード(PDF)
主な特長
  • DC Ultraと最高の友 - DC Ultraのデフォルトの最適化を全てサポート
  • フローベースの直感的なグラフィカル・ユーザ・インターフェイス
  • 電源オン/電源オフ状態を考慮した低消費電力回路の検証
  • 設定情報が間違っていたり漏れていたりすることによる擬似エラーを減らす自動設定モード
  • パフォーマンスを上げる内蔵の分散処理
  • DC Ultra最適化前後の検証成功率を向上させる自動ガイダンス
  • ESPテクノロジを併用し、フルカスタム、またメモリ設計の検証をサポート

最も包括的な等価検証ソリューション
DC Ultraはレイアウト後のタイミング、面積、消費電力との高い相関性を達成するためにトポグラフィカル・テクノロジを用い、リタイミングやフェイズの反転、論理展開など先端の合成技術を提供しますが、Formalityは、DC Ultraにより合成されたこのような設計をより優れた完成度に導きます。Formalityはまた、配線混雑度を予測し緩和するために用いられるDC Graphicalと完全な互換性があります。設計者はもはや、等価検証をパスするためにDC Ultraの強力な合成の質を妥協する必要はありません。DC UltraとFormalityを併用したとき、最高の、しかも検証可能な結果品質が生まれます。

Figure 1: Formality equivalence checking solution.
図1:等価検証ソリューションFormality

Formalityの使いやすさ

自動設定モード
Formalityの自動設定モードは、設定情報が間違っていたり漏れていたりすることによる擬似エラーを減らすことにより、検証を簡素化します。自動設定モードは、ネーミングスタイル、unused pins、テスト用インプット、クロックゲーティングなど、DC Ultraで作られた仮定に対応する設定情報をFormalityの中から適用します。RTLやネットリスト、ライブラリなど重要なファイルは、自動的に示されます。自動設定情報はすべてサマリーレポートにリストされます。

自動ガイダンス
FormalityはDC Ultraにより生成されるガイド付き設定ファイルを使うことにより、合成最適化の一役を担うことができます。ガイド付き設定は、ネーム変更、レジスターの最適化、増幅器構造その他多くの合成中に起こりうる変化を含みます。これら”correct-by-construction”の情報があるので、マッチングと検証の際に最も効率的なアルゴリズムを用いることができ、パフォーマンスが向上、やり直しなく一度で作業が完了できます。 Formalityのガイド付き設定は、ログファイル構文解析に頼ったツールでは予測できなかった部分を予測する、標準のドキュメント化されたフォーマットです。

独立した検証
ガイド付き設定フローの各アスペクトは、直接または間接的に検証され、すべての内容はASCIIファイルの形でアクセスでき、綿密に調べることが可能です。

グラフィカル・ユーザ・インターフェース
Formalityは、フローベースのグラフィカル・ユーザ・インターフェースを採用することによって、「out-of-the-box usability=特別な知識/操作なしでの使いやすさ」を設計者に提供します。リファレンス設計と実行結果の設計を同時に表示することが可能です。コーン・プルーニングの自動化で、リファレンス設計と検証対象設計の間の違いのみを示すことができ、見やすくなります。

Figure 2
図2:自動コーン・プルーニングにより、デバッグの際に回路図を見やすくする

Hier-IQ™ テクノロジ
シノプシスがパテントを持つ Hier-IQテクノロジは、フラット検証の使いやすい操作性に加えて、階層検証によるパフォーマンスの利点を兼ね備えています。

Error-ID テクノロジ
Error-IDは、二つの設計の間で実際に機能の違いを引き起こしているロジックを特定します。複数の違いが存在するときは、Error-IDは複数のロジックの違いを探し出し、レポートします。Error-IDはまた、任意の機能の違いを修正をする際に置き換えることのできる、代替的なロジックを示します。このような柔軟性により設計者は、最も実現しやすい変更を選ぶことができます。

Failing pattern ウィンドウ
全ての間違ったインプット・パターンを、見慣れたスプレッドシート形式のフォーマットで見ることができます。Failing pattern ウィンドウは、検証エラーの原因や不適切な設定を示唆する傾向を迅速に特定するのに最適な手法です。

Figure 3
図3: Failing patternウィンドウの可視的検査により、問題のある箇所が容易に特定されます。

消費電力を考慮した検証
FormalityはPower Compilerと完全に互換性があり、電源オン/電源オフの状態、多電圧、多電源、クロックゲーティングを検証します。レファレンス設計の消費電力が上がると、Formalityは機能を検証します。もし検証対象設計の消費電力の上がり方が違っていると、エラーポイントが示されます。Formalityは、リファレンス設計の消費電力が下がると対象設計の消費電力が下がるかを機能的に検証し、もし対象設計の消費電力が想定通り下がらない部分があれば、その機能的な状態を検出します。消費電力の状態は、Power State Table (PST)に定義されます。パワーの設計意図は、IEEE 1801 Unified Power Format (UPF)によりFormalityに提供されます。

Figure 4
図4:回路図画面により、電力のコネクティビティが見やすくデバッグしやすい

設計完了までの時間を短縮

分散処理
Formalityのパフォーマンスは、分散処理でさらに加速されます。ツールに内臓されたこの機能により、4つのプロセッサを同時に使用して、検証時間を減らすことができます。

時間短縮の他の機能
FormalityのHierarchical Scripting機能は、設定を追加する必要なくサブブロックを調査する手法で、問題点を特定したり、修正を確認するのに最適です。

ソース・ブラウザがRTLとネットリスト・ソース・ファイルを開き、任意のインスタンスの発生をハイライトします。これにより、RTLとゲートレベル設計という二つのバージョンを関連づけることが容易になります。

Error Region Correlationは、Error-IDで発見された一方の設計のエラーに関連するロジックを、もう一方の設計内に視覚的に特定する機能です。また、Command Line Editing機能により、Formalityのコマンドラインから作業する際、履歴やコマンド・テキストエディターの一般的なコマンドを活用することができます。

ECOの検証とインプリメンテーション
Formalityは、二つの設計が機能的に相関するために変更されなければならないロジックの場所を特定することによって、機能的なECOの検証および実行を助けることができます。さらにFormalityは、ECOが意図しない機能的影響を生んでいないことを保障することができます。

トランジスタ・レベルの検証
FormalityとESPを組み合わせることによって、カスタム回路、組み込みメモリ、複雑なI/Oの高速な検証が可能です。ESPのテクノロジは既存のSPICEモデルとRTL動作モデルを直接読み込むので、マッピングや翻訳で制限を加える結果になりません。

入力フォーマット
  • Synopsys DC, DDC, Milkyway
  • IEEE 1800 SystemVerilog
  • Verilog-95, Verilog-2001
  • VHDL-87, VHDL-93
  • IEEE 1801 Unified Power Format (UPF)
ガイド付き設定のフォーマット
  • Synopsys V-SDC
  • Formality Guide Files (SVF)
プラットフォーム・サポート
  • SPARC Solaris
  • IBM AIX
  • Linux Suse, Red Hat and Enterprise