【EDSF2011】Jasperの新製品「ActiveProp」は3種類のプロパティを自動生成

パシフィコ横浜で開催されたElectronic Design and Solution Fair 2011のレポート。

米Jasper Design Automation社のフォーマル検証ツールを日本で供給するCyberTec社のブースでは、今回のEDSFairが初お披露目となる新製品「ActiveProp」を展示していた。

Jasper社の新製品「ActiveProp」は、RTLコードの機能検証およびデバッグ用に開発された新ツールで、SVAプロパティを自動生成してくれるスタンド・アローンの製品である。現時点ではまだβ版としてのリリースに留まっているが、2011年のQ1後半には正式版として製品がリリースされる計画となっている。

「ActiveProp」の嬉しい点。それはアサーション・ベース検証の大きな壁と言える、プロパティの作成を全自動で処理してくれるという事に尽きる。プロパティの自動生成にあたり設計者が用意するのは、デザイン（RTL）とそのシミュレーション結果（VCD/FSDB）のみで、「ActiveProp」でデザインを読み込んだ後、ツールが示してくれる着目ポイント（信号線のリスト）から着目したい信号線を指定すると、自動的にSVA形式のassert/assume/cover3種類のプロパティとそのレポートを生成してくれる。シミュレーターと「ActiveProp」をAPIで繋ぎ、シミュレーターを走らせながらシミュレーション結果を「ActiveProp」に取り込む事も可能である。

※画像はCyberTec社提供

「ActiveProp」で生成したプロパティはSVA（SystemVerilog Assertion）形式で出力されるため、Jasper社のフォーマル検証ツール「JasperGold」はもちろんの事、他社製のフォーマル検証ツール、シミュレーター、エミュレーターなど様々なツールで利用する事ができる。しかし、Jasper製品と組み合わせて利用する事でより大きな検証効果をもたらすが可能で、Jasperでは「ActiveProp」の利用法を大きく3つ提案している。

１．設計初期段階での利用

RTL開発および検証の初期段階において「ActiveProp」を用いてアサーションを生成し、機能検証に活用する。生成されたアサーションをJasperGold/ActiveDesignを活用して確認する事でアサーションの品質を高める事ができる。

２．設計最終段階での利用

RTL開発および検証の最終段階において、ランダム検証のカバレッジの収束やコーナー・ケース・バグの発見に利用する。「ActiveProp」を用いてシミュレーション結果からカバープロパティを生成しJasperGoldで解析すれば、機能カバレッジの最後の数％を達成可能かどうか判断できる。また、シミュレーション結果から生成されたアサーションはデザインの動作を表している可能性が高いので、アサーションをJasperGoldであらゆる入力シーケンスで網羅検証する事で、コーナーケースもチェックできる。

３．IP再利用時の利用

Jaspperの「ActiveDesign」でデザイン変更前後の動作解析を行う際に、「ActiveProp」の生成したプロパティを「ActiveDesign」のビヘイビアやレシピとして使用。複数のバージョン間の動作の差異を効率的に解析できる。

※画像はCyberTec社提供

尚、「ActiveProp」のプロパティ生成機能は単にプロパティを生成するだけでなく、その重要性を考慮してプロパティをランキング表示する機能や、シミュレーション結果を追加するとより意味のあるプロパティを生成する学習機能も備えている。更に「ActiveProp」は異なる階層間の信号線の関係も考慮してプロパティを生成する事が可能で、これは他社のプロパティ自動生成ツールには無い大きな特徴の一つと言える。

※画像はJasper社提供

CyberTecは、今回のEDSFairでは「ActiveProp」を一つの目玉として展示していたが、出展社セミナー「フォーマルエンジン始動！設計品質と検証効率を改善せよ！」では、以前から提唱しているポスト・シリコン・デバッグでのフォーマル検証の活用法やRTL開発における見える化手法などを紹介。満席のセミナー会場ではその手法にうなずく参加者の姿が目立った。