機械学習を用いたカバレッジ駆動型ハードウェア検証の効率化に関する研究

2014 Fiscal Year Research-status Report

• Project/Area Number: 25330061
• Research Institution: Shimane University
• Principal Investigator: 浜口 清治 島根大学, 総合理工学研究科(研究院), 教授 (80238055)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: フォーマル検証 / SATソルバ / 機械学習

Outline of Annual Research Achievements

SoC(システム・オン・チップ)，FPGA などの設計工程では，設計検証が依然として大きな比重を占めており，効率化が重要な課題となっている．シミュレーションべースの検証手法の一つして，カバレッジと呼ばれるメトリクスを指標として，これを改善することにより，検証の品質を改善する方法が広く採用されている．カバレッジ上昇を加速するための手法として，機械学習を利用してテストパタン生成を制御する手法があり，自動化という点で有効である．本研究では，回路の構造情報やSATソルバを利用して，機械学習の手法の弱点の克服を目指している．
25年度に行った計算機実験の結果を受けて，26年度はベイジアンネットワークの種々の機械学習アルゴリズムについて，カバレッジ改善の観点から評価を行った．試行した5種類のアルゴリズムと3種類の設計について，どの場合にも明らかに有効となるアルゴリズムは発見できなかった．実験結果を分析・検討した結果，まず計算コストの低いアルゴリズムを適用して初期解を得たのち，より計算コストの大きなアルゴリズムを適用する手法が有効との見通しを得た．この実験過程で，設計記述から半自動的にテスト環境を生成するシステムを構築した．
また，本研究ではSATソルバを併用する方法との併用を目標としているが，これについて，25年度に開発したシステムを拡張して，シミュレーションの途中の状態からのSATソルバの適用が可能であるように改良した．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

クロスカバレッジと呼ばれる指標をターゲットとしたシステムを構築することになっていたが，25年度で良好な結果が得られなかったため，この部分のシステムの構築が遅れている．一方，SATソルバを利用したシステムおよびベイジアンネットワークの機械学習を利用する際にテスト環境を半自動的に構築するシステムが完成していることから，最終年度中に予定通りの実験と評価が可能であると考えている．

Strategy for Future Research Activity

上記で述べたように，25年度に行った計算機実験において構造情報の利用に関して想定した結果が得られなかったが，26年度の実験により，アルゴリズム構築の目途が得られている．すでにSATソルバを利用するシステムとベイジアンネットワークの機械学習を利用するシステムを作成しているため，これに改造を加えて，最終的に当初の計画通り，2手法を組み合わせた効率の良いカバレッジ駆動検証手法の確立を目指す．