2019 Fiscal Year Research-status Report
SATソルバと機械学習手法を融合した自動設計検証に関する研究
| 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 |
本研究では，ハードウェア設計に対するカバレッジ駆動検証に関して，入力制約を考慮した，設計の種類によらない方式の確立，機械学習とSATソルバを用いる2方式の統合を目指している．
2019年度は，まず，前年度に実装した分散実行に基づくカバレッジ駆動検証システムの拡張として2方式を実装・評価した．１つめは，SATソルバによってカバレッジ改善のための入力パターンを生成する際，探索区間をクロックサイクルの大小によって分割し複数のプロセスで分担する方法であり，ISCAS'89ベンチマーク回路の大規模設計に対して，カバーポイント数について従来法に比べて0.8%から5.4%の改善を得た．すでにカバーの難しいポイントが対象であることから，有意な結果であると判断している．2つめは従来用いていたトグルカバレッジとは異なる，レジスタに対する整数としての区間を基準としたレンジカバレッジへの拡張である．SATソルバと前年度実装したSMTソルバに基づく方法を比較した結果，cordic 計算を行う回路について，SATソルバでは 66.6%，SMTソルバでは 73.3% と算術演算が多く含まれる回路ほど，SMTソルバが有利になるという結果が得られている．
さらに，2019年度は，誤りを含む回路に対する誤り検出能力の実験的評価も開始している．設計データの演算をランダムに選んで，別の演算に置き換えた設計を誤り設計として生成し，カバレッジ駆動検証システムの上で，もとの設計データとシミュレーションを行って，誤りが検出できるかどうかを評価した．ISCAS'89ベンチマーク回路の s5378では，1000個の誤り設計に対して，各設計800秒制限のもとで，ランダムシミュレーションのみでは84.2%であった検出率が，SATソルバと組み合わせる本研究の方式では，89.0%となることを確認している．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
2019年度は，前年度の分散実行方式のシステムの拡充を主として行った．予備実験の結果，誤り検出実験には長時間(1セット1-2週間)を要することをが判明したため，もともと2020年度に予定していた実験を優先して開始することとした．一方，2019年度に予定していた，入力制約アルゴリズム，機械学習の導入については，例題の作成，プログラムの実装が遅れており，最終年度に実施する予定である．
|
| Strategy for Future Research Activity |
上記に述べたように，入力制約アルゴリズム，機械学習の導入については実装が遅れているが，計画の他の部分は順序を入れ替えて実施してきており，最終的に当初の計画通りの実施内容とする予定である．
|
| Causes of Carryover |
実装実験で大きな計算時間を必要とする部分があること，また，入力制約アルゴリズムと機械学習の導入に関する実験でも強力な計算機を利用する必要が見込まれることから，計算機実験用のクラウドサーバの費用として翌年度に繰り越すこととした．
|
