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

2013 Fiscal Year Research-status Report

• Project/Area Number: 25330061
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: Shimane University
• Principal Investigator: 浜口 清治 島根大学, 総合理工学研究科(研究院), 教授 (80238055)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: シミュレーションベース検証 / ベイジアンネットワーク / カバレッジ駆動検証 / フォーマル検証技術

Research Abstract

SoC(システム・オン・チップ)，マイコン，FPGAなどの設計工程では,設計検証が依然大きな比重を占めており効率化が課題となっている．シミュレーションべースの検証手法の一つとして，ランダムにテストパタンを生成して検証カバレッジを向上させる手法がある．カバレッジ上昇を加速するため機械学習を利用してランダムパタン生成のパラメータを制御する手法があり自動化という点で有効である．本研究では，回路の構造情報や充足可能性判定器 (SATソルバ)を利用して，既存の機械学習による手法の弱点の克服を目指している．
初年度は基本となる実験系の構築を行った．具体的には，回路の設計記述に対して，ランダムテストを実施して，ベイジアンネットワークの機械学習を行い，これを利用してパラメータを調整するシステムである．本研究では，回路の構造情報を利用して，機械学習による予測性能の改善を目的の一つとしているが，予備実験を行った結果，単純な学習アルゴリズムでは，構造情報を利用しても必ずしもカバレッジ改善に効果があるとは限らないことが判明した．今後，種々の学習アルゴリズムについて比較を行っていく予定である．
また，本研究では，ランダムパタン生成ではカバーが難しいケースをSATソルバの利用により扱えるようにすることも目標としている．これについて，カバレッジレポートからカバー困難な条件を見つけ出し，SATソルバを使ってカバーするための入力パタンの生成を行うシステムを構築した．ランダムパタン生成に比べて，トグルカバレッジについては最大5倍の改善を確認した．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

当初の予定では，クロスカバレッジと呼ばれる条件の組み合わせをターゲットとした手法について検討を始めることとしていたが，本来の目標の一つである構造情報を利用した場合の計算機実験の結果が想定よりも良くなかったため，クロスカバレッジに関する検討が遅れている．一方，主として平成26年度に実施予定であったSATソルバの利用に関しては，すでに計算実験を始めており，全体での遅れは軽微であると考えている．

Strategy for Future Research Activity

上記で述べたように，ベイジアンネットワークによる機械学習については，構造情報の利用について想定したような結果が得られていない．種々の学習アルゴリズムの適用について評価を行っていく予定である．同時にクロスカバレッジへの手法の適用について検討していく．SATソルバの利用に関しては，すでに実験システムを構築しており，SATソルバのより効果的な適用方法について検討していく．
最終的には当初の予定通り，構造情報を利用したベイジアンネットワークの学習とSATソルバを用いた，効率のよりカバレッジ駆動検証手法の確立を目指す．