パシフィック・デザインが自社開発したRTLフォーマル・プロパティ・チェッカを発売
2012年7月、パシフィック・デザイン株式会社は、自社開発したRTLフォーマル・プロパティ・チェッカ「AiPG」の発売を開始した。
パシフィック・デザインの「AiPG」は、EDA技術の研究で有名な東京大学藤田昌宏教授の指導の下、2010年から具体的な開発が開始されたフォーマル検証ツールで、「SMTソルバ」と呼ばれるwordベースの探索エンジンをRTL検証に適用するもの。
「AiPG」は「SMTソルバ」の中でも世界最高速の「Boolector」というオーストリア ヨハネス・ケプラー大学が開発したGNU/GPLベースの探索エンジンを採用しており、最小限のプロパティ記述およびプロパティ指定をもとにwordベースでVerilogで記述されたRTLの網羅的検証を自動実行する事が可能。検証対象を自動的に指定するプロパティ生成機能と分散型並列処理により容易かつ高速な網羅的検証が可能で、Dead Codeの検出、対抗Deadlockの検出、リソース衝突の検出など、フォーマル検証ツールが有効とされる用途において、これまでに無いアプローチでのプロパティ・チェックを実現する。
「AiPG」はこの7月より販売が開始されており、パシフィック・デザインでは顧客のプロパティ要求を「AiPG」に組込み、プロパティ生成を自動化させるといった対応も行なっている。
= EDA EXPRESS 菰田 浩 =
（2012.07.19
）