独OneSpin、フォーマル検証ツール「360 MV」製品ファミリーを拡張

2009年1月19日、フォーマル検証ツールを手掛ける独OneSpin Solutionsは、フォーマル検証の統合環境「360 MV」製品ファミリーの拡張を発表した。

OneSpinの「360 MV」製品ファミリーは、日本上陸当初は2つの製品で構成されていたが、現在は下記の5つの連携する製品で構成される包括的なフォーマル検証環境。少ないプロパティ記述で高速な検証を実行できる点やプロパティを作成するメソドロジを用意している点が特徴で、プロパティの再利用性が高い高度なフォーマル検証を簡単な手順で実行できるツールとして欧州市場では強固な顧客を確保している。

発表によると、今回の製品拡張でステップバイステップの構造化されたアサーションベース検証アプローチが導入され、ユーザーは専門知識とプロジェクトのニーズに適したレベルに応じてツールを利用可能に。すなわち、検証エキスパートに限らずフォーマル検証の初心者でもアサーションベース検証で効果を出せる環境を用意した。

具体的には、3段階の「標準」フォーマルABVと、オペレーションをベースとしたOneSpinの改良ABV手法の3段階のエントリーレベルを用意しており、設計初期段階のコードクリーンアップのための自動チェックから、最高の検証品質を保証する検証まで広範囲にフォーマル検証をカバー。新たなデバッガも用意され、より高品質な検証をより効率的に実現できるようになった。

同新製品ファミリーは、今週開催のEDSFair2009にて初披露される予定。

■「360 MV」製品ファミリー　ラインナップ

?360 MV Inspect™ （自動チェック）
コードが最初に利用可能となった段階で すぐにRTLエラーを検出でき、以降のデバッグ工数を削減できます。数千のチェックを数分で実行し、フォーマル検証の経験やアサーション言語の知識を必要としません。

?360 MV Check™ （インプリメンテーション意図の検証）
マイクロアーキテクチャまたはインプリメンテーションの側面を表したアサーションを使って、設計者はテストベンチが利用可能となる数週間または数ヶ月前にインプリメンテーションのバグを見つけ出すことができ、早期の品質向上と以降のデバッグ工数削減を可能にします。

?360 MV Verify™ （機能仕様と設計に含まれるオペレーション検証）
業界最高のキャパシティおよびパフォーマンスと、設計のオペレーションに対する独自の体系的な検証により、深く、複雑なエラーをシミュレーションや他のフォーマルツールよりも格段に効率的に見つけだします。 また、新しい証明ベースのデバッガにより、複雑なSVAに対して自動的にエラー箇所を特定します。360 MV Verifyは、高カバレッジのモジュール／サブシステムレベルテストベンチに対する必要性を削減、または解消し、OneSpin独自の、オペレーションベースのフォーマルABVに対するエントリポイントとしての役割を果たします。 

?360 MV Assure™ （自動ギャップ検出を使った検証）
まだ検証されていない入力シナリオを自動的に特定し、設計に含まれるオペレーションの体系的な検証を強化します。デバッグおよび診断環境により、これらの検証ギャップをクローズするSystemVerilogアサーションの開発を助け、仕様／インプリメンテーションの徹底的な協調検証を確実にします。

?360 MV Certify™ （ギャップフリー検証）
OneSpinの旗艦製品であり今日他のどの検証アプローチでも保証できない検証品質を提供します。検証プランニング、検証の実行、自動ギャップ検知を統合した閉ループプロセスであるOneSpinのGapFreeVerification™ により、可能な限り最高の検証品質を達成します。360 MV CertifyはギャップのないSystemVerilogアサーションの開発を支援します。仕様に準拠した設計の完全な機能のリファレンスモデルを構築し、RTLコードがリファレンスモデルと機能的に等価であることを証明します。

※OneSpin Solutions社