米Jasper、フォーマル検証ツール「JasperGold」に拡張モデリングセット「Proof Accelerator」を追加

2008年4月9日、フォーマル検証ツール「JasperGold」を手掛ける、米Jasper Design Automation社は、「JasperGold」の拡張モデリングセット「Proof Accelerator」を発表した。

プレスリリース：http://www.jasper-da.com/press_releases/040908.htm（英文）

Jasperの発表によると新しい「Proof Accelerator」は、複雑なデータパスデザインの検証用に用意されたもので、下記4種類。これらを用いることで、単独シミュレーションによる従来方式の機能検証よりも優れたカバレッジを実現可能で、フォーマル検証の複雑さを減らすと同時にそのパフォーマンスとキャパシティを拡大できる。

・Formal Scoreboard Proof Accelerator
　　　　　シミュレーションにおけるスコアボードと同等のフォーマル検証スコアボード
・Clock Domain Crossing (CDC) Proof Accelerator
　　　　　複数の非同期クロックドメインを含むデザインブロックの検証用

・Cache Proof Accelerator
　　　　　複雑なキャッシュのモデリング用

・FIFO Proof Accelerator
　　　　　複雑なFIFOのモデリング用

今回発表された「Proof Accelerator」は、Jasperが長年の取り組みで成功させた、バスプロトコルを含めたデータパスデザインの検証から生み出されたもので、「JasperGold」と組み合わせて利用することで、シミュレーションでは不可能な「全てのシーケンスの完全な検証」を実現できるという。

※Jasper Design Automation社
http://www.jasper-da.com

※CyberTec株式会社（Jasper Design Automation社日本代理店）
http://www.cyber-tec.co.jp