NEWS
SynopsysのVC Formal SIGで聞いた機械学習を用いたフォーマル検証高速化機能の話 by ルネサス
2018年10月3日、日本シノプシスは品川で「シノプシス・ベリフィケーション・セミナー2018」の開催と合わせて同社のフォーマル検証ツールのユーザーを対象とした「VC Formal Special Interest Group (SIG)」を開催した。
ここでは同イベントで聞いたルネサス エレクトロニクスによる「VC Formal」新機能評価の内容を紹介する。
講演タイトル：「Regression Mode Accelerator (RMA) 評価結果」
講演者：ルネサス エレクトロニクス株式会社 デザインメソドロジ部 酒井 皓太氏
ルネサスの酒井氏の講演はSynopsysのフォーマル検証ツール「VC Formal」の検証高速化機能「Regression Mode Accelerator（以下、RMA）」のベータ版評価に関するもの。
「RMA」は今年8月に公にされたマシンラーニング技術を応用した新機能で、初回のフォーマル検証の実行結果を自動的に参照することで2回目以後の処理時間を短縮することが可能。Synopsysは同機能を用いることでフォーマル・プロパティ検証のスピードを10倍高速化することが可能としている。
酒井氏によると「RMA」評価のモチベーションは、下記大きく3つ。その期待に対する効果を確認すべく、全アサーションが2分以内に収束する低負荷テストデータと、12時間で未収束プロパティが残る高負荷テストデータの2種類のテストデータを用いて評価を実施した。
・最適エンジン選択によるマシンリソース削減→収束するプロパティはもっと速く
・自動抽象化・制約最小化の学習による収束性向上→収束しないプロパティはより少なく
・類似設計／類似プロパティへの学習→より大きな変更にも学習効果を発揮
評価１．低負荷テストデータの評価結果
酒井氏はまずイベントリンクコントローラのデザインを対象に「RMA」の効果を評価した。その結果「RMA」の学習機能を利用することで、2回目以降の実行で検証時間が4分の1に短縮され、メモリ使用量も半分以下に減った。1回目の実行では「RMA」を用いない場合と比べて検証時間は5％、メモリ使用量は10％増加した。これは学習に伴うオーバーヘッドと考えられるという。
評価２．高付加テストデータの評価結果
次にAXI3バスブリッジを対象に「RMA」の効果を評価した。SynopsysのアサーションIPによる142個のプロパティを使用した。その結果「RMA」の学習機能を利用することで、2回目以降の実行で収束したプロパティ数が1個増えたが、全てのプロパティを収束することはできず、学習機能を使わない時と同様にタイムアウトに終わった。メモリの使用量は1回目の実行以上に2回目の実行で増加した。
そこで収束プロパティ数の推移について分析したところ、1回目の実行結果の収束プロパティ数138個に到達する時間が2回目の実行の方が20,000秒近く早い事がわかった。
評価３．高付加テストデータ、デザインに小変更を加えた場合の評価結果
続いて評価２．と同じAXI3バスブリッジを対象に一部デザインを変更（書き込みレスポンスバッファ削減）し、評価２．で用いた学習データを用いて「VC Formal」を実行したところ、収束プロパティが更に1個増えた。この事から酒井氏は「RMA」はある程度のデザイン変更には対応可能と結論づけた。
評価４．高付加テストデータ、アサーションIPのパラメータを変更した場合の評価結果
最後に評価２，３と同じAXI3バスブリッジを対象に、利用しているアサーションIPのパラメータ（AXI3のバス幅）を変更し「RMA」の効果を評価した。パラメータを変更し全プロパティを一旦収束させ、その時の学習データを用いることでパラメータを元に戻しても効果が得られるかもしれないと期待したが、類似したプロパティであっても学習データを使い回す事はできなかった。
酒井氏は今回の評価を踏まえ、プロパティ検証の高速化において「RMA」は有効とした上で、収束性の向上や学習データの利用に関する更なるイノベーションに期待すると語った。
なお、補足情報となるが、Synopsys米国本社で「VC Formal」のR&Dに関わる野々下氏の説明によると、「RMA」にはローカルモードとサーバーモードの2つのモードがあり、サーバーモードで利用すればプロジェクト間で同じ学習データを利用する事も可能との事。また現在の「RMA」は、RTLの最初のバージョンの実行結果を繰り返し使うことで学習効果を上げ、リグレッション・テストの効率化を実現しているが、今後は更にマシンラーニングの活用範囲を広げていく方向で開発を進めているという。
｜ページの先頭へ｜