OneSpinがフォーマル検証のカバレッジ解析/計測の新製品「Quantify MDV」を発表

2011年5月23日、フォーマル検証ツールを手掛ける独OneSpin Solutionは、フォーマル検証のカバレッジ解析および計測のための新製品「Quantify MDV」を発表した。

OneSpinの発表によると新製品「Quantify MDV」は、その名の通り、MDV（メトリックドリブン検証）の定量化を実現するもので、OneSpin曰く「業界初のフォーマル・メトリックドリブン検証ソリューション」となるもの。

同製品は、同社が提供しているRTL機能検証のためのフォーマル検証ツール「OneSpin 360 MV」のユーザー及び検証のマネージャーに向けて用意されたもので、「OneSpin 360 MV」によるフォーマル検証の進捗および品質を自動的に解析・計測し、検証マネジメントに関する判断材料を定量化したデータで示してくれる。

例えば、RTLコードの未検証部分の解析、それをカバーするためのアサーションの挿入箇所の示唆、制約の検証による過剰制約の検出、冗長コード、検証コード、デッドコードの特定などの解析が可能で、それら指標をHTMLフォーマットまたはMentorが開発してAccelleraに寄贈したカバレッジ・データ仕様UCDB（Unified Coverage Database）フォーマットで出力することが可能。フォーマル検証の指標をテストベンチ指標に統合すれば検証プロジェクト全体の進捗を可視化することもできる。

また、「Quantify MDV」は、SVA（SystemVerilog Assertions）を構造化されたアサーションおよびオペレーションベースのアサーションの両方でサポートしており、ユーザーは、OneSpinのTiming Diagram Assertion Library (TiDAL) を使うことにより、機能タイミング・ダイアグラムをオペレーショナル SVAに変換することが可能。RTLサブ・ブロックの早期検証から、ブロック全体およびブロック間の接続検証、ブロック設計のハンドオフまで、プロジェクトのどの段階でも使うことができため、検証エンジニアおよびマネージャーは、検証の進行過程で適宜正確な計測結果に基づくプロジェクトの評価を行なう事ができるようになる。

※新製品「Quantify MDV」は、第48回DACにて同社ブースで展示予定。価格は年間ライセンスでUS$25000からの設定。

※OneSpin Solution社