機能等価性検証ツール

概要

Formalityは、フォーマル検証技術を用いて2つの異なるバージョンのセルベース・デザインを比較し、それらが機能的に等価か否かを確認する論理等価性検証ソリューションです。Formalityは、すべての主要言語、ASICおよびFPGAアプリケーション、そして設計最適化手法をサポートしており、最も包括的な検証ソリューションを提供します。その高い完成度、開発期間短縮能力、および使い易さにより、Formalityは最先端の設計フローに欠くことのできない検証ツールです。

主な特長

• ASIC、FPGAに対し最も完全かつ最先端の数学的検証ソリューションを提供
• 分散処理によりCPU単体の処理能力を拡大
• 自動セットアップファイルの使用により、エラーを起しやすい手作業でのセットアップ作業を低減
• 等価性検証工程をわかりやすくガイドすることにより、すべての設計者の生産性を向上
• 実績のある業界最高クラスの検証容量により、現在のハードウェア環境への投資効果を最大限に発揮

　

等価性検証は成功の条件

パフォーマンスとカバレッジに制限があるため、超大規模回路のダイナミック検証は現実的ではありません。等価性検証は、テストベクタを使用せずに大規模回路を迅速かつ完全に検証するスタティック解析の一種です。スタティック解析は高性能で低リスクなため、等価性検証は急速に普及し、すべての設計工程に不可欠となっています。

図1：Formalityはシノプシスのフルチップ機能等価性検証ソリューションの主要ツールです

検証課題

不十分なカバレッジ
設計の技術と手法は急速に進化しつづけています。FPGAプロトタイピングが幅広く採用され、エンド・アプリケーションではさらに高度な演算機能が必要となっています。設計技術が等価性検証能力の限界を超えている場合、最終的なゲートレベルのネットリストがRTLと等価であることが実証できません。その結果、テープアウトが遅れることになります。

長時間に及ぶ検証工程
現在では、4千万ゲート規模の回路の検証も珍しくありません。このような回路規模では、シングルCPUでの検証では厳しい開発スケジュールを満たすことはできません。

非直感性
1ゲート当たりの機能性を高めることにより、チップのサイズを縮小し、コストを削減することができます。そのためには、以前にも増してデザインの最適化が行なわれるようになっています。等価性検証ツールには、これらの最適化から発生する変更点を認識させるためのセットアップが必要です。その結果、セットアップが検証過程の大部分を占めるようになっています。

コスト管理
検証容量は、企業が既存の32ビット・システムを最大限利用しながらコストの管理に努めている点から、依然として最も重要な問題となっています。企業はコストを抑えるため既存の32ビット・システムを最大限利用しており、検証容量は依然として最も重要な問題となっています。

最も包括的な検証ソリューション

FPGAプロトタイピング
FormalityとDesign Compiler FPGA（DC FPGA）は、FPGAを用いたプロトタイプ設計において業界で最も完全な検証を提供します。これにより、トップクラスのFPGAデバイスをASICとして実現する際に、RTLの機能が確実に維持できていることを確認できます。

高度な演算機能
数学的立証を実行するFormalityの革新的な検証エンジンは、最速の数学的検証性能を実現し、先進の合成ツールの新しいダイナミック・アーキテクチャに容易に対応します。加算器ツリーの再配分、リソース共有、演算子のマージなどの最適化は、Formalityにより簡単に検証することができます。

Formalityの使いやすさ

自動セットアップ
Formalityは、インプリメンテーションの際生成されるセットアップ・スクリプトの使用により、デザインの最適化を自動的に考慮することができます。このスクリプトには、名前の変更、レジスタの相違、および乗算器のアーキテクチャのセットアップ・コマンドが含まれており、手作業を要することなく完全かつ最高の性能を提供します。構造的に正しいセットアップにより、エラーの発生しやすい手作業でのセットアップのデバッグに費やされるイタレーションが軽減されます。すべての情報は独立して検証され、TCLフォーマットで作成されます。

直感的な環境
Formalityは、フロー・ベース環境を採用することによって「out-of-the-box usability=特別な知識/操作なしでの使いやすさ」を提供します。経験豊かなエンジニアの思考方法に合わせて構築された環境で作業をすることで、すべての設計および検証エンジニアはシノプシスが有する業界最高レベルのノウハウを活用することができます。

インクリメンタル手法
設計のやり直しを最小限に抑えるため、一致処理と検証がインクリメンタルに実行されます。

インクリメンタルな一致処理では、さまざまな処理技術を用いて繰り返し処理を実行することにより、処理条件との一致を検証することができます。

インクリメンタルな検証では、迅速に検証を一度実行した後、解決されなかった点の検証を続行すると同時に、結果の解析を開始することができます。

図2：Formalityのフロー・ベース手法は、経験豊かなエンジニアのように 等価性検証工程をわかりやすくガイドします

Hier-IQテクノロジ
革新的な技術であるHier-IQテクノロジは、フラット検証の使いやすい操作性に加えて、階層検証のパフォーマンスのメリットを兼ね備えています。Hier-IQテクノロジは、マーケットをリードするFormalityの機能向上に大きく貢献しました。

デバッグ機能
通常、実際の設計問題が単純なゲートの置き換えで解決できることはありません。複雑なインプリメンテーション・エラーを迅速に分離するには、高度なデバッグ機能が必要です。Formalityの革新的な機能は、このような設計の不一致の検出、分離、および解決を支援します。

エラー候補は、エラーの原因の可能性があるネットを表示します。これにより、論理をトレースし直して問題を分離する作業をよりインテリジェントに行えます。

回路図トリミングは、エラーに関係ない論理を回路図ビューから削除します。これにより、関連情報だけに焦点を当てることができます。

パターン表示は、すべてのエラー入力パターンをスプレッドシート型のフォーマットで表示し、設計者はこの中から自分の設計に適用したいパターンを選択できます。これにより、最も容易にデバッグできるパターンを選択することが可能です。

階層スクリプトの生成は、セットアップを増やすことなくサブブロックを調べる方法を提供します。この機能は、問題個所の分離と修正部分の検証に最適です。

ソース・ブラウジングは、RTLおよびネットリストのソース・ファイルを開き、選択されたインスタンスを表示します。これにより、HDL中のエラー個所まで誘導してくれるため、デバッグの労力が軽減されます。

アノテーションされたエラー解析は、デバッグ作業中の手作業による確認と計算を減らし、設計のトレースバックの速度を向上させます。

図3：Formalityのアノテーションされたエラー解析では、デバッグ時に指示が与えられます。

投資効果を最大限に発揮

分散検証
Formalityは、シングルCPU上でも優れた検証性能を発揮できますが、分散処理環境下ではその検証性能を累乗的に高めることができます。例えば、4つのプロセッサを同時に使用して検証を行うことにより、検証時間を4分の1にまで短縮します。

超大規模回路の場合は、Formality の分散検証により、64ビットのプラットフォームを利用してローメモリのコンポーネントを32ビットシステムに割り当てることができます。分散検証のパフォーマンス利点により、高価な64ビットシステムは他の重要な作業に当てることができます。

正確な結果
Formalityは、シミュレータと同様の方法でRTLを解釈します。この方法が最も確かだからです。合成の方法を用いた場合、設計のエラーを検出できない確率が高くなります。シノプシスが目標としているのは、テープ・アウト結果が初回のシリコン・テスト時に設計者の意図した通りに機能することを保証することです。

入力フォーマット

以下に示すフォーマットの任意の組み合わせをサポートしています。

SystemVerilog 3.0*
Verilog-2001
Verilog-95
VHDL-93
VHDL-87
EDIF
Synopsys DB、DDCおよびMDB
SPICE（Formality-ESP）
*SystemVerilogは変換ユーティリティを通してサポートされています。

プラットフォーム・サポート

Sun Solaris（32および64ビット）
HP-UX（32および64ビット）
IBM AIX（32および64ビット）
Linux Red HatおよびEnterprise
- x86（32ビット）
- Opteron（64ビット）
- IPF（64ビット）

Formalityは、主要ASIC/FPGAフローをすべてサポートしています。