メンター・グラフィックスの0-In Formal v3.0、
フォーマル検証に新たなレベルの自動化を実現

2010年06月09日

メンター・グラフィックス・コーポレーション(本社: 米国オレゴン州、以下メンター・グラフィックス)は、複雑なIC設計に対する業界で最も先進的なフォーマル検証ソリューションである0-In® Formal v3.0を発表しました。0-In Formal v3.0では自動化による使いやすさの強化、Questa®検証プラットフォームのUCDB(Unified Coverage Database)との統合およびカバレッジの「到達性」チェックによるカバレッジ・クロージャのさらなる高速化、検証エンジンの改良による性能およびキャパシティの強化などが行われています。

フォーマル検証は、今日の複雑なIC設計において、機能検証上の膨大な課題に対処するために必要なテクノロジの1つです。0-In Formalを用いることにより、ユーザはシミュレーションを開始する前に多数のバグを特定、修正できます。これにより、より早い段階で、必要な動作のカバレッジ達成にシミュレーションを集中させることが可能になります。一度に特定のシナリオを1種類だけテストするシミュレーションとは異なり、0-In Formalではあらゆるシナリオを並行検証し、一切のエラーが発生し得ないことを徹底的に確認します。検証に対する労力を最大限にしたとしても、シリコンで設計エラーが確認される場合もあります。0-In Formalでは、HDLモデル内で即座にエラーを特定し、エラーの修正により設計が正常に動作することを迅速に検証することで、このようなエラーの診断および修正を加速します。

0-In Formal v3.0では、Questaとのより緊密な統合を通して、混在言語設計のサポート強化も行われています。共通のユーザ・インタフェースとフロントエンドを用いることにより、Questaと0-In Formalの両方で同一のコンパイル・フローが利用できます。またQuestaと0-In Formalの両方でUCDBへの書き込みが可能で、バックエンドも共通化されています。Questaのフロントエンドとの統合は、PSLおよびSVAのアサーション言語機能だけでなく、VHDLおよびSystemVerilogの設計および検証言語機能のサポートも強化するものです。加えて、0-In Formalのオートチェックでは、ユーザがアサーションを記述することなく、多数の一般的なエラーを自動検出することが可能です。

0-In Formalでは、例えば「いかなるステートからでも最終的にはリセット・ステートに到達する」というような「liveness」プロパティの追加により、より多くの種類の動作が確認できるようになりました。

さらに、到達不可能なカバレッジの自動識別およびUCDBとの統合により、カバレッジ計算から到達不可能なカバレッジ・ポイントを自動除外し、カバレッジ・クロージャをより迅速に達成できるようにもなりました。

使い勝手の向上としては、フォーマル検証結果の可視化およびデバッグ機能のサポート強化や、新しく強化された検証エンジンによる性能とキャパシティの向上により、複雑な設計をより高速かつ完璧に検証できるようになったことが挙げられます。

「メンター・グラフィックスは、0-In Formal v3.0において、いくつかの特筆すべき機能強化を行いました。コンパイルは非常に高速で、AMDではすべてのプロパティの証明が可能となりました。この新しいリリースではラッチの解析についても、クロックとデータが混在している場合でさえ、非常に効率的に行えました。」AMD、MTS設計エンジニア、Dr. Shaun Feng氏は上記のように述べています。

「フォーマル検証のエキスパートは、業界をリードするメンター・グラフィックスの証明エンジンの性能強化とlivenessプロパティのサポートを評価されると思います。アサーション・プロパティを記述する必要性を排除し検証チェックを自動化することにより、メンター・グラフィックスのフォーマル検証テクノロジの性能を、フォーマル検証のエキスパートだけでなく、すべての検証エンジニアの手に渡すことが可能となります。」メンター・グラフィックス、Design Verification Technology Division、General Manager、John Lenyoは上記のように述べています。

Questa機能検証プラットフォーム
Questa機能検証プラットフォームは、優れた性能と大規模設計への対応を両立し、業界で最も包括的な検証機能を提供します。最新の高性能コンストレインツ・ソルバ、幅広いファンクショナル・カバレッジのサポート、UCDB(Unified Coverage Database)などを特長とするQuestaは、ABV(アサーションベース検証)、テストベンチ・オートメーション、CDV(カバレッジドリブン検証)をネイティブにサポートします。消費電力を考慮した機能検証により、RTL環境内で低消費電力設計の機能検証を行うことも可能です。Questaは柔軟なOVM 2.0により最先端の機能を幅広く提供し、あらゆる設計/検証フローに対して他に類のない言語と機能のサポートを提供します。

メンター・グラフィックスについて
メンター・グラフィックスは、EDA(Electronic Design Automation)のテクノロジ・リーダーとして、高性能な電子機器を短期間でよりコスト効率よく開発するためのハードウェアおよびソフトウェアのソ リューションを提供しています。ますます複雑化する基板およびチップ設計の世界でエンジニアが直面する様々な設計上の課題を克服するための革新的な製品お よびソリューションを提供します。メンター・グラフィックスは業界で最も幅広いクラス最高の製品ポートフォリオを有し、EDAベンダとして唯一組込みソフ トウェア・ソリューションを持っている企業です。メンター・グラフィックスについての詳しい情報はhttp://www.mentorg.co.jpを ご覧ください。

Mentor GraphicsはMentor Graphics Corporationの登録商標です。その他記載されている製品名および会社名は各社の商標または登録商標です。

 

機能検証について

 

本件に関するお問合わせ

メンター・グラフィックス・ジャパン株式会社
コーポレート・マーケティング部
E-mail: mktg_mgj@mentor.com