【52DAC】Cadenceがフォーマル検証ツール「JasperGold」を刷新、性能最大15倍向上

2015年6月15日、Cadenceは第52回DACの開催に合わせて新製品のフォーマル検証ツール「JasperGold」の発表を行った。

プレスリリース文

「JasperGold」という名前は、Cadenceが昨年4月に買収したJasper Design Automationの旗艦製品として市場では有名だが、今回Cadenceはその名前を引き継ぎ新たな製品としてリリースした。

新しい「JasperGold」は、旧製品とCadenceの提供していた「Incisive Formal Verifier」を統合したフォーマル検証ツールで、基本的には旧「JasperGold」をベースとしながらも両製品の良さを残しつつ中身は大きな変化を遂げている。

ライセンスの供給形式は、フォーマル検証ユーザーに対してやりたい事に合わせてアプリケーション毎に「App」としてソリューションを提供してきた旧「JasperGold」のスタイルがそのまま継承されており、新「JasperGold」においては以下の通り計12の「App」が用意されている。この「App」は今後もラインナップを増やす計画のようだ。

・Formal Property Verification APP

・X-Propagation Verification APP

・Connectivity Verification APP

・CSR Verification APP

・Low Power Verification APP

・ARCH APP

・Structural Property Synthesis APP

・Behavioral Property Synthesis APP

・Security Path Verification APP

・Sequential Equivalency Checking APP

・Coverage APP Option

・Deadlock Detection APP

ツールのインタフェースについては、旧「JasperGold」のユーザーにとっては今まで同様、「Incisive Formal Verifier」のユーザーにとっても内部のパーサーがリンクする構造となっており基本的に大きなインパクト無くツールを利用できる。

内部のフォーマル・エンジンに関しては、「JasperGold」と「Incisive Formal Verifier」の両ツールの持っていた複数のエンジンに加え新たなコンストレイント・ソルバーが用意され、これらエンジンを協調的に働かせるような仕組みになっており、ユーザーの目的に応じて都合の良いエンジンをツールが自動的に選んでくれる。つまりユーザーは使用するエンジンを意識すること無く、目的に応じた最適なアウトプットを手に入れる事ができる。これによりツールの処理性能は最大15倍程度引き上げる事が可能ということだ。

また、「JasperGold」はCadenceの設計/検証プラットフォーム「System Development Suite」の一部に位置付けられており、デバッグ環境「Indago」や検証マネジメント環境「vManager」と高度な連携が可能な一つの検証エンジンとなっている。そのため「vManager」を用いてフォーマル検証結果を可視化する事や、デバッグ環境「Indago」のバックグラウンドで「JasperGold」を走らせたりという事が可能。既にこういったツール連携はサポートされている。

ちなみに、今年の4月にリリースされたばかりのデバッグ環境「Indago Debug Platform」では、新たに「Adovanced Debug Analyzer App」という機能が用意されたが、その中身は「JasperGold」のフォーマル技術が利用されており、What-if解析やアサーションにフォーカスしたコード解析などシミュレーション結果のデバッグをより効率化できるようになっている。

その他、新たな「JasperGold」では、Lintツールとしても使えるRTLの構造チェック機能や、ローパワー検証向けの機能（CPFサポート済）など様々な機能追加/機能向上が図られているほか、「JasperGold」ユーザー向けにフォーマル検証で利用できる合成可能なアサーション・ベースのVIPも用意されている。

※日本ケイデンス・デザイン・システムズ社

= EDA EXPRESS 菰田　浩 =
（2015.06.12 ）