2020 Fiscal Year Annual Research Report
Study on Automated Design Verification Combining a SAT-based Method and a Machine Learning Technique
| Project/Area Number |
18K11216
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
浜口 清治 島根大学, 学術研究院理工学系, 教授 (80238055)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | カバレッジ駆動検証 / SATソルバ / 機械学習 |
|---|
| Outline of Annual Research Achievements |
IoTシステムの普及，機械学習技術の進展などにより，FPGA上での実装を中心にして，消費電力の低減化あるいは計算処理の加速を目指して，多種多様な回路設計が行われている．回路設計に対する動作検証は手数が大きく，可能なかぎり自動化する必要がある．本研究ではシミュレーションベース検証の一手法であるカバレッジ駆動型検証について，機械学習を利用する手法とSATソルバを用いる手法を組み合わせて改善することを目標とした．
当初の計画では，まず，入力制約付きの設計記述の作成とともに，特にベイジアンネットワークによる機械学習を用いる方式に入力制約を組み込む方式を実装・評価することとし，次に，誤り挿入をおこなった設計記述を作成し，カバレッジと誤り検出能力との関係を調べて，システム構成に反映させることとしていた．性能改善のための手段として，整数・実数の加減算やビットベクトル演算を扱うことができるSMT (Satisfiability Modulo Theory)ソルバの利用，分散実行による２方式の同時実行を計画した．
以上が当初の計画であったが，ターゲットとしていた Wishbone プロトコルベースの実設計記述をわずかしか入手できなかったことと，機械学習に用いる予定であったツールの性能に限界があったことなどから，目的のすべてを達成することはできず，特に上記ベイジアンネットワークによる機械学習については実装・実験を行うところまで進めることができなかった．結果として，当初計画のうち成果は，(1)SMTソルバによる性能の改善，(2)分散実行方式による性能の改善，(3)誤りを含む記述に対するエラー検出能力のSATソルバに改善，(4) 入力制約下でのカバレッジ駆動検証方式の確立と有効性の確認の4点となった．
|
