OneSpin、業界初となるフォーマルアサーションベース検証カバレッジ解析と計測のための 自動化されたメトリックドリブン検証ソリューションを発表
Quantify MDVはフォーマル検証の進捗と品質からあらゆる不確実性を解消
2011年5月23日、ドイツ ミュンヘンおよび東京発 − 革新的なフォーマル アサーションベース解析ソリューションを提供するEDAベンダー OneSpin Solutions は本日、業界初のフォーマル・メトリックドリブン検証（MDV）ソリューションQuantify MDVを発表しました。この製品はRTL（Register Transfer Level）設計に対するフォーマル検証の進捗と品質を自動的かつ包括的に解析し、計測するものです。OneSpin 360® MV の旗艦製品ファミリーを強化するこの画期的な ツールは、プロジェクト全体に渡り正確なフィードバックを提供し、検証エンジニアは次の3つの重要な問いに対して定量的かつ正確な答を得られるようになります：
- アサーションの品質は？
- 制約の品質は？
- 検証プランはどの程度進んでいるか？
Quantify MDVはフォーマル検証がどの程度進んでいるかをエンジニアとプロジェクトマネージャが正確に判断するために必要な、包括的な指標を提供します。 これにより、経験による推測ではなく、正確な計測結果に基づいてプロジェクトの残り工数を評価することが可能になります。Quantify MDVは現在提供中であり、OneSpinは2011年6月5-10日、カリフォルニア州サンディエゴで開催される2011 Design Automation Conferenceにて同製品のデモンストレーションを行います。
見当や当て推量が不必要に
Quantify MDVはRTLとアサーションを設計空間全体に渡り包括的に解析および追跡することによりフォーマル検証の進捗に関する不確実性を取り除きます。RTLコードの検証済み、未検証を識別し、検証の穴を埋めるためにどこにアサーションを挿入すれば良いか、エンジニアは一目で確認することができます。また、制約を解析することにより過剰な制約を特定できるため、過剰制約を検出するためにアサーションをシミュレートする必要がありません。また冗長なコードおよび検証コード、カバー不可能なデッドコードも特定します。さらにQuantify MDVのフォーマル検証指標をテストベンチ指標に統合することにより検証全体の進捗を完全に可視化することが可能です。
OneSpinの社長兼CEO、Peter Feistは次のように語っています。「Quantify MDV以前には、検証の進捗状況を正確に定量化するフォーマル検証指標がありませんでした。アサーション密度のような直接的指標データは検証の進捗や品質を表したものとは言えません。設計のどの程度がカバーされているかについてはエンジニアに推測するしかありません。Quantify MDVにより、推測の必要はなくなります。また、フォーマル指標をテストベンチカバレッジと統合することにより、検証全体に完全な透明性がもたらされます。OneSpinの新しいソリューションは簡単なキー入力だけで習得の手間もなく実用的な指標をエンジニアおよびプロジェクトマネージャに提供するものであり、これまでフォーマル検証手法がメインストリームに普及する上での大きな障害であった問題を解決しています。」
Quantify MDVはRTLサブブロックの早期検証から、ブロック全体およびブロック間の接続検証、ブロック設計のハンドオフまで、プロジェクトのどの段階でも使うことができます。またエンジニアは任意の段階で精度とランタイムのトレードオフを行うことができます。たとえば、早期の段階では未検証のRTLコードを素早く見つけ、プロジェクトがサインオフに近づいた段階ではより精度の高い検証を行うことも可能です。
Quantify MDVは、フォーマル検証指標データをHTMLフォーマットおよびUCDB（Unified Coverage Database）フォーマットで出力することができ、 検証チーム全体のMDVフローにフォーマル検証を統合可能にします。検証エンジニアはフォーマル検証とテストベンチ検証の進捗指標の両方を、統合されたレポートで同時に確認することが可能です。また、Quantify MDVの出力を他のデータベース フォーマットにあわせてプログラミングすることにより、幅広い検証フローで利用することが可能になります。
「自動化されたQuantify MDVは、検証チームのすべてのメンバーが使いこなせます。」Feistはこのように付け加えます。「推測が排除され、不確実性が解消されることにより工数の短縮とより優れた検証指標の取得が可能になります。このツールを使うのに数学の専門知識や特殊な技術は必要なく、誰もが検証の進捗と品質を正確に評価できます。」
Quantify MDVは業界をリードするアサーション標準、SystemVerilog Assertions (SVA)を構造化されたアサーションおよびオペレーションベースのアサーションの両方でサポートしています。エンジニアは OneSpinのTiming Diagram Assertion Library (TiDAL) を使うことにより機能タイミングダイアグラムをオペレーショナル SVAに変換することができます。 設計言語のサポートにはSystemVerilog、Verilog、VHDLが含まれます。
価格と提供時期
Quantify MDVは標準360 MV製品ラインの一部として提供されており、360 MVの1年間ライセンスの価格は$25,000からとなります。
360 MVについて
OneSpinの 360 MV製品ファミリーは、RTL設計のための最も包括的なフォーマル アサーションベース検証（ABV）ソリューションです。360 MVは機能RTL検証に対する業界で最も革新的かつ重要な製品として主要な業界誌とその読者により過去5年間で4回の選出を受けました。360 MVは完全に自動化されたRTLチェックから、パワフルなアサーションベース検証、OneSpinの特許技術である最高品質のgap-free検証まで、フォーマル検証の初心者、経験豊富なユーザー、エキスパートまでが使える、最も幅広いABVアプリケーションをカバーしています。 詳細な情報はhttp://www.onespin-solutions.comをご覧ください。
OneSpin Solutionsについて EDA（Electronics Design Automation）ベンダーOneSpin Solutionsは、複雑なASICおよびFPGA設計の機能検証を容易化し、検証工数を短縮するための、受賞歴のある最もキャパシティの高いフォーマル検証ソリューションを提供しています。OneSpinの360 MVソリューションは特許取得済みのフォーマルカバレッジ解析によりかつてない検証カバレッジと生産性を実現します。詳細な情報はhttp://www.onespin-solutions.com/をご覧になるかinfo@onespin-solutions.comまで電子メールでお問い合わせください。