Cadenceがフォーマル検証ツール「JasperGold」に機械学習を用いた新技術を搭載、検証効率を劇的に改善
2019年5月8日、Cadenceは第三世代目の製品となるフォーマル検証ツール「Cadence® JasperGold® Formal Verification Platform」（以下、新型JasperGold」を発表した。
発表によると新型「JasperGold」は、機械学習技術の活用によりフォーマル検証のコア技術を改良。具体的には「Smart Proof Technology」と呼ぶ、機械学習を用いた証明アルゴリズムと証明エンジンの選択・設定機能を使い、より高速な証明を可能にする。Cadenceは「Smart Proof Technology」によって、証明の実行速度が最大4倍に高速化できるとしており、実際に同ツールを試用したSTMicroelectronicsの担当者は、証明の実行時間が即座に平均２倍高速化できたとコメントしている。機械学習技術は、リグレッション・テストの実行の最適化においても活用されており、Cadenceによると実行速度を最大６倍高速化できるという。
またCadenceによると、新型「JasperGold」は1年前のバージョンと比較してコンパイル規模が２倍になり、メモリ使用量を平均５０％削減することが可能に。更にクラウド上で利用できる並列コンパイル技術によって、扱えるデザイン規模を効果的に増やすことができるという事だ。
前出のSTMicroelectronicsの担当者によると、新型「JasperGold」を試用した結果、検証効率を劇的に改善できたという話で、証明の実行速度の高速化に加え、リグレッション・テストの高速化（5倍高速化）、収束しないプロパティの削減（50％以上削減）も確認できたという。
= EDA EXPRESS 菰田 浩 =
（2019.05.08
）