2018 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ソルバを用いる２方式の統合を目指している．本研究では特にトグルカバレッジと呼ばれる，設計内信号線の値の変化に着目している．
2018年度は上記の２方式の統合のための土台として，分散実行に基づくカバレッジ駆動検証システムを実装・評価した．このシステムでは，通常のランダムシミュレーションと SATソルバを用いた入力パタン探索を，異なるプロセスとして任意個並列実行することができる．ISCAS'89ベンチマーク回路のうち規模の大きい設計５つに対して評価を行った．ランダムシミュレーションと SATソルバを順次繰り返して行う方法に比べて，ランダムシミュレーション用に１プロセス， SATソルバー方式用に３プロセスを割り当てた場合の結果では3600秒の時間制限の下で，５つの設計すべてについてトグルカバレッジが改善されるという結果を得た．例えば，もっとも規模の大きい s38417 についてはカバーすべきポイントの総数2926個に対して，38個分の改善が確認できた．
さらに SATソルバに変えて SMTソルバを用いる方式についてもプロトタイプ実装を行って評価した． SMTソルバは算術演算を多く含む設計に対して有効であり，実験の結果，算術演算器を18個-227個含む３つの設計に対していずれも改善が見られた．例えば，算術演算器を227個含みカバーすべきポイントの総数が10376個のDCT設計では，3600秒の制約のもとではSATソルバでは2037個しかカバーできなかったが，SMTソルバでは 7356個カバーすることできて，大幅な改善が見られた．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
2018年度は，複数の方式の統合のための土台となる分散並列実行可能な検証システムの実装・評価を行った．また，SMT ソルバを用いる方式についてもプロトタイプ実装・評価を行っている．以上は当初2019年度に予定していた内容である．当初は入力制約を考慮した方式の実装・評価を中心に行う予定であったが，今後の研究が容易になると判断し，上記の実装・評価を先行して行うこととした．これにより入力制約を考慮した入力パタンの生成や機械学習を利用する方式については，モジュールとして実装し，より容易にシステムに付け加えることができるようになる．一方，2018年度に予定していた入力制約を考慮した入力パタンの生成については，アルゴリズムの検討は行ったが未実装である．機械学習を利用する方式についても予備的な実験を行った段階にとどまった．
|
| Strategy for Future Research Activity |
2018年度は本来2019年度に予定していた実装・評価を行ったため，2018年度の計画分が遅れている．上記に述べたように，これは研究計画全体をより容易に進めるための変更であり，2019年度は当初2018年度に予定していた入力制約を考慮した入力パタン生成，機械学習の適用について検討・実装を続けていく．その後は当初の計画通り実施する予定である．
|
| Causes of Carryover |
研究計画について2018年度分と2019年度分を入れ替えて行うこととしたため，使用経費に差が生じた．具体的には商用のシミュレーションツールのライセンス費であり，これは2019年度に導入する予定である．
|
