フォーマル検証のJasperが新たに2つのプロパティ生成アプリを発表
2012年10月29日、フォーマル検証ツールを手掛ける米Jasper Design Automation社は、新たな「JasperGold Apps」として、2つのプロパティ生成アプリのリリースを発表した。
Jasperは、論理検証における様々な個別の問題に特化した専用ツールとして6種類の「JasperGold Apps」を今年5月にリリース（※関連記事）していたが、今回新たにリリースしたのは、「Structural Property Synthesis App」と「Behavioral Property Synthesis App」の2つ。
「Structural Property Synthesis App」は、よくある機能的なエラーを自動的にチェックするツールで、必要となるのはVerilogまたはVHDLで記述されたRTLのみ。ツールがRTLを解析し、内蔵するデッドコードチェック、FSMチェック、アリスメティックオーバーフローチェックといった数種類の機能チェックを行い、デザインの構造的なプロパティを自動生成する。生成されるプロパティは、ランキングや分類分けされ、SVAで出力されるため、Jasperのフォーマル検証環境に限らず市販のシミュレーターやエミュレーターでも利用可能。デザイン初期のデバッグだけでなく、RTLサインオフ時にも利用効果を得る事ができるという。
「Behavioral Property Synthesis App」は、RTLとシミュレーション結果(FSDB/VCD)から、デザイン中のカバレッジ・ホールを抽出し、機能カバレッジを向上させるための、アサーション、制約、カバーといったプロパティを自動生成するツールで、複数のサイクルにまたがる時系列的なプロパティや異なる階層の異なるモジュール間の信号関係についてプロパティを生成することが可能。「Structural Property Synthesis App」と同じく生成されるプロパティはランキングや分類分けされるため、効率的なフォーマル検証を実現し、機能カバレッジの向上、検証の収束に寄与する。
発表によるとSTARC（株式会社半導体理工学研究センター）は、既に今回リリースされた2種類の「JasperGold Apps」を評価しており、同ツールは「デザインに役立ち、シミュレーションだけでは難しい検証環境の質的向上を実現する」とコメントしている。
= EDA EXPRESS 菰田 浩 =
（2012.10.30
）