フォーマル検証のJasperが「シーケンシャル等価性チェック」の新アプリをリリース
2014年3月31日、フォーマル検証ツールを手掛けるJasper Design Automationは、新製品「Sequential Equivalency Checking App」のリリースを発表した。
Jasperは、特定の検証ニーズに特化したフォーマル検証ツールを「Jasper Apps」として展開しているが、今回発表した「Sequential Equivalency Checking App」も「Jasper Apps」の一つで、異なる2つのRTLの機能等価性を検証するもの。
クロック・ゲーティングによるローパワー化など、既存のRTLに手を加えた場合に元のRTLと変更後のRTLの機能等価性をチェックする必要があるが、それをフォーマル検証技術で網羅的に行うのが「Sequential Equivalency Checking App」で、等価性の検証と同時にGUIベースのデバッグの環境も提供する。
同種の製品としてはCalypto Design Systemsが古くから「SLEC RTL」という製品を提供しているが、「Sequential Equivalency Checking App」の強みは高速な処理性能で、新規開発した専用エンジンにより同社の通常のフォーマル検証よりも遥かに高速な検証が可能。市販の他社ツールと比較しても高速で、ある例では他社ツールで2日かけても証明しきれなかったデザインを数時間で証明したという。
Jasperによると「Sequential Equivalency Checking App」は、同社の大手顧客の要求で開発したもので、欧米では既にベータ版から複数の企業が利用。昨年のJasperユーザー・ミーティングでは、NVIDIAが「Sequential Equivalency Checking App」を使った事例を発表している。日本国内においても複数の企業が先行ユーザーとして同ツールを利用しているようだ。
※画像は全てJasper提供のデータ
= EDA EXPRESS 菰田 浩 =
（2014.04.04
）