フォーマル検証のJasper今年のイチ押しは「Low Power Apps」ローパワー設計を網羅検証
2013年6月28日、フォーマル検証ソリューションを手掛ける米Jasper Design Automationは、新横浜のホテルで「Real-World Applicationセミナー」と題したプライベート・セミナーを開催した。
ここでは6月の第50回DACで聞いた話も踏まえ、同社の最新のソリューションについてレポートする。
ツールの話の前にまず同社の業績について紹介しておこう。
日本でのセミナーでも紹介されていたが、同社の売上は3年前の2010年頃から急伸しており、2007年以降の平均成長率は35％とEDA業界全体の成長を凌ぐ勢い。3年前に打ち出した個別の検証要求にフォーカスした自動化アプリ「Jasper Apps」の戦略があたり、大きく成長したとの事で、現在は半導体上位15社のうち10社が顧客。日本国内でも複数の大手メーカーが長らく同社のフォーマル検証ツールを利用している。同社の成長ぶりは本拠地米国で高く評価されており、今年5月には有望なハイテク・ベンチャーを称える「2013 Red Herring Top 100 North America」のファイナリストに選出された。（関連ニュース）
そんな成長著しいJasperが今年のイチ押し製品として5月にリリースしたのが、「Jasper Apps」の一つとなる新製品「Low Power Apps」。同ツールは複数のパワードメインを持つSOCの設計をターゲットにしたフォーマル検証ツールで、ローパワー設計が意図通り実現されているか、また設計におけるパワー最適化化手法が回路本来の機能を損ねていないかなどをRTLの段階で網羅検証することができる。
具体的には、RTLおよびパワー仕様記述言語UPFまたはCPFで記述されたパワー仕様を読み込み、パワー分割仕様に従いパワーを取り扱えるフォーマル・モデルをツール内部で生成。同時にパワー最適化の構造チェックを行う検査項目とパワー制御を検証するためのアサーションを生成し、それを基にフォーマル検証を実行する。
「Low Power Apps」は、Power-Awareの状態でパワー・シーケンスの検証やパワー・マネジメント回路の検証などフォーマル検証技術による機能検証が可能なため、パワー・マネジメントの導入がファンクションに与える影響を確認することが可能。このようなローパワー設計ソリューションはこれまで無かったとJasperのマーケティングおよび事業開発VPのOz Levia氏は言う。
※画像は全てJasper提供のデータ
確かに既存のソリューションとしては、RTLとパワー仕様の整合性をチェックするツールやパワー最適化の電力面の影響を見積るツールは存在しているが、UPFおよびCPFの機能を考慮して機能検証するソリューションは、テストケースを用いたダイナミック・シミュレーション以外無かった。網羅検証を行うフォーマル検証は、デザインの品質向上という面でシミュレーションより分があると言える。
尚、Jasperの新製品「Low Power Apps」は、既にSTMicroelectronicsとBroadcomが先行して実際のプロジェクトに使用しているという話で、この両社は第50回DACにてJasperブースで事例を紹介していた。
= EDA EXPRESS 菰田 浩 =
（2013.08.08
）