Magellannskk_pdf.gif

ハイブリッドRTLフォーマル検証ツール

概要

Magellanは、発見が困難なコーナーケースのバグを迅速に検出することにより、機能検証の期間を短縮し高品質なデザインを実現する、ハイブリッドRTLフォーマル検証ツールです。Magellan独自のハイブリッド・アーキテクチャは、最新のフォーマル検証エンジンとVCSのシミュレーション・エンジンの長所を組み合わせて、大規模で複雑なデザインのプロパティを検証します。
主な利点
  • コーナーケースの機能バグを検出することによりデザインの品質を向上
  • 検証サイクルの早期に機能バグを検出することにより検証コストを削減
  • ダイナミック検証環境とフォーマル検証環境の間でアサーションを再利用することにより検証効率を向上
主な特長
  • ハイブリッド・アーキテクチャによる大容量フォーマル検証
  • ユーザー定義のプロパティのフォーマル検証
  • 自動抽出プロパティのフォーマル検証
  • false-negativeエラーの排除
  • アサーションの階層検証のサポート


図1:Magellanによるプロパティ検証

大規模デザインのバグ検出

Magellanは、デザインの奥深いステート状態にまで到達するVCSのシミュレーション・エンジンを使ってハイブリッドRTLフォーマル検証を実行し、指定されたプロパティをデザインが満たしているかどうかを複数のフォーマル検証エンジンを用いて検証します。これにより、発見が困難なコーナーケース・バグの検出が可能になります。従来のフォーマル検証ツールは、バグ検出にフォーマル検証エンジンのみを使用していたため、非常に小規模なデザインでは有効でした。これに対して、MagellanはVCSのシミュレーション・エンジンを使用して大規模なデザインの細部まで迅速に到達し、フォーマル解析を実行してデザイン中のバグを検出します。VCSのシミュレーション・エンジンとMagellanのフォーマル検証エンジンの自動的な連携により、Magellanは「大規模」なデザインを効率的に処理できます。



図2:Magellanのハイブリッド･アーキテクチャ




表1:自動抽出プロパティの一覧


false-negativeエラーの排除

false-negativeエラーは、デザインの実際の動作条件では発生しない、仕様と異なるデザイン動作をフォーマル検証ツールがレポートしたときに発生します。たとえば、従来のフォーマル検証ツールでは、デザインの実動作と異なる状態でデザインを解析し、バグとしてレポートすることがありました。Magellanはこうしたfalse-negativeエラーを排除します。Magellanのフォーマル・エンジンによって検出された違反を、違反をレポートする前に内蔵のVCSエンジンで自動的に検証することにより、実際の動作環境で再現性のあるバグかどうかを確認できます。このため、エンジニアが手作業でfalse-negativeエラーを検証する必要がなくなり、検証効率をさらに向上させることができます。

プロパティのフォーマル検証
Magellanは、所定のデザインのユーザー定義のプロパティまたは自動抽出プロパティをフォーマル検証します。RTLのほかに、デザインのアサーションと制約を指定することができます。Magellanのフォーマル解析により、以下のいずれかの結果が生成されます。
  • Proven（証明）
    指定されたアサーションは、制約に基づくいかなる入力でも守られることが保証されます。
  • Falsified（反証）
    入力が制約に基づいていても、デザインの動作が指定されたアサーションに違反する可能性があることを意味します。その場合、Magellanは、エンジニアによるシミュレーションと検証が可能なデバッグ・トレースを作成します。
  • Inconclusive（不確定）
    プロパティがprovenでもfalsifiedでもない場合、ダイナミック・シミュレーションでモニタとして使用できます。また、一定の時間枠でtrueまたはfalseになるかどうかのフォーマル検証も行えます。

 


図3:Magellanでブロックレベル検証に使用される仮定/制約



図4:チップレベルのモニタとしてブロックレベル検証で用いた仮定/制約を再利用


先進のDesign-for-Verification手法

Magellanは、シノプシスのDiscoveryプラットフォームがサポートしているDesign-for-Verification（DFV）手法を強化します。Magellanで使用されるプロパティと制約は、シノプシスのVerilog HDLシミュレータVCSやテストベンチ生成ツールVeraにより、ダイナミック検証環境でモニタとして再利用することができます。また、Magellanでデザインブロックを検証するために記述された制約を、以降のブロックを検証するためのアサーションとして使用することもできます。これにより、ブロックの検証時に作成された制約がさらに検証され、デザインに対して真であることが保証されます。
Discoveryベリフィケーション・　プラットフォーム
シノプシスのDiscoveryベリフィケーション・プラットフォームは、Verilog HDL/VHDL言語混在、ミックスド・シグナル、システムレベル検証、アサーション、検証用IP群、コード・カバレッジ解析、機能カバレッジ解析、テストベンチ生成そしてフォーマル検証を実現する検証ツール群を、高速かつ高い検証効率で活用可能にする統合検証環境です。Discoveryベリフィケーション・プラットフォームは、複雑なSoC設計のためのVerilog HDL、VHDL、Verilog HDL/VHDL混在、SystemC、およびミックスドシグナル・シミュレーションをサポートします。Discoveryベリフィケーション・プラットフォームは、SystemVerilogおよびシノプシスのDFV手法とともに、要求されたプロジェクト期間内での初回製造での成功に貢献することで、検証効率の向上を支援します。
言語サポート
Magellanは、Verilog HDLまたはVHDLで記述されたRTLデザインの検証に使用できます。プロパティと制約はOpenVeraアサーション、Verilog HDLまたはVHDLで記述できるので、非常に柔軟性があります。またMagellanでは、Open Verification Libraryの既定義のチェックを使用することもできます。さらにMagellanは、最新のSystemVerilogに対応するよう開発されています。