ONESPIN SOLUTIONS、新しいGapFreeVerification™プロセスによりフォーマル検証の生産性を劇的に向上

複雑なモジュールおよびIPに対して予測可能なフォーマル検証結果を体系的に提供

2008年2月18日、ドイツ、ミュンヘンおよびカリフォルニア州サニーベール発－革新的な、フィールド実績のあるフォーマル検証ソリューションを提供するEDA ベンダーOneSpin Solutions は本日、検証生産性を劇的に向上する、受賞歴のある同社の360 Module Verifier (360 MV) ソリューションに対する、特許出願中の体系的検証プロセス、GapFreeVerification を発表しました。この新しいプロセスは、複雑なモジュールおよびＩＰに対して予測可能な、再現性のある検証結果を体系的に提供するもので、初回からエラーのない動作を保証するギャップのないフォーマル検証を加速します。GapFreeVerificationは、ユーザーの処理とツールタスクの構造的かつ統合されたシーケンスを定義するものです。このシーケンスによりDUV（Design Under Verification）ならびにそのインフォーマルな仕様を、ギャップのないフォーマルな仕様と、等価性が証明されたDUVへと、高い予測性で変貌させることができます。

このGapFreeVerification プロセスは、今日の検証アプローチにおいて生産性を損なっている主要な要因の一つを実質的に解消します。それは、シミュレーションベースおよび他のフォーマル検証アプローチを使って (1)検証プランニングとレビュー、(2)複雑なカバレッジモデルの構築、(3)検証品質を向上させるための膨大なカバレッジ情報の収集と解析－いずれも検証の穴がないことを保証できませんが－を行うのに必要としている多大な工数です。

新しいOneSpinのプロセスは、ギャップのないプロパティセットで構成される、ハイレベルな機能リファレンスモデルをユーザーが体系的に構築することを可能にします。このハイレベルなリファレンスモデルは、DUVの期待される機能のすべてのフォーマルな仕様です。これは、テストベンチにより期待されるDUVの動作を指定したゴールデンリファレンスモデルと同等のものです。360 MVのプロパティチェックおよび完全性チェック機能を使って、RTLとネットリストをフォーマル等価性チェックで比較するのと同じ厳密さでリファレンスモデルとDUVが比較されます。これにより、ギャップのない検証とエラーのないDUVの動作が保証されます。さらに、新しいプロセスと強化された360 MVの各ツールでは、主として「バグハンティング」を目的とした他のフォーマル検証ツールでよく見られるようなキャパシティ、スケーラビリティ、ならびに偽の反例による問題は軽減されています。これらの問題を軽減することにより、GapFreeVerificationは体系的なフォーマル検証を、他のフォーマルアプローチが対応できない幅広い複雑なモジュールおよびＩＰにも拡大できます。

OneSpinの社長兼CEO、Peter Feistは次のように述べています。「検証をスケーラブルなものに保つためには、検証生産性の劇的な向上が必要です。360 MVと生産性の高い検証プロセスを統合することで、検証にかかる時間と労力を削減する重要なマイルストーンを達成しました。GapFreeVerificationは、10年にわたりユーザーと協力して複雑性の高い設計を体系的に検証する中で蓄積された経験とベストプラクティスを包含したものです。新しいプロセスはこの経験を初心者ユーザーにもフォーマル検証のエキスパートにも提供し、ギャップのない検証を効率的に実行し、予測可能な結果、すなわち複雑なモジュール／ＩＰ似対する最高の品質と、劇的な検証工数の削減を可能にするものです。」 価格と提供時期

GapFreeVerificationは現在提供中で、360 MVの最新バージョンに含まれており追加コストはかかりません。