| 研究課題/領域番号 |
22K11962
|
|---|
| 研究機関 | 京都橘大学 |
|---|
研究代表者 |
浜口 清治 京都橘大学, 工学部, 教授 (80238055)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| キーワード | 設計自動化 / カバレッジ駆動検証 / SATソルバ |
|---|
| 研究実績の概要 |
本研究の目的は特に標準規格の入出力プロトコルを持つ回路設計を対象として，SATソルバ(Satisfiability Solver， 論理式の充足可能性判定器)および機械学習を用いた手法を確立することである． 2022年度は具体的には次のような成果を得た．
(a) 並行プロセスによるカバレッジ検証の効率の評価
まず，トグルカバレッジをターゲットとして評価を行った．報告者による先行研究では，ランダムシミュレーションとSATソルバーを用いた入力パターン生成を組み合わせたアプローチを提案しており，実験を通じて有効であることがわかっていた．しかし、検証プロセスにおいてSATソルバーの実行時間が支配的要素であるため、これが検証プロセスの進行を妨げていることが判明していた。これを改良するために、ランダム/SATベースの処理を並列化することで、この先行研究を拡張した．実験の結果、並列化のアプローチがカバレッジ改善のために有効であることが示された．本結果については論文として投稿し，採録が決まっている(発行は2023年6月)．
(b) ブランチカバレッジを対象としたカバレッジ検証の評価
本年度はさらに，設計記述内の分岐条件に関するカバレッジ(ブランチカバレッジ)について評価を行った．ブランチカバレッジについてはすでに他の研究グループによる評価結果が出ているが，本研究ではランダムシミュレーションのみではなく，SATソルバを組み合わせることによって，カバレッジを改善できることが確認できた．またランダムパタンについても信号線の変化に着目した生成を行うことにより，より良いカバレッジ改善が得られることを確認した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
入出力プロトコルを前提とした自動検証手法については，基本的なしくみは確定しており，予備的な実験を行っているが，AMBA AXI プロトコルへの対応が想定より手数がかかっていて進捗が遅れている．また，基礎実験に注力したため，ベイジアンネットワークの利用については実装が遅れている．
|
| 今後の研究の推進方策 |
2022年度の成果を踏まえ2023年度は次の２点を中心に研究を進める．
(a) 入出力プロトコルを前提とした自動検証手法の確立と評価
2022年度に予定していたが以下の(b)に関連する基礎実験に注力したため2023年度に実施する．FPGA 等のインターフェースでよく用いられている AMBA AXI を主として取り上げ，これを対象に自動検証を行う手法を確立する．
(b) 機械学習とSATソルバを用いた方式の確立と評価
この手法では，ランダムパタンの生成をどうするかが課題であるが，2022年度に実施した計算機実験によって，信号の変化に着目して生成するとカバレッジの改善に効果があることが確認できている．この結果を踏まえて，ランダム生成したデータ転送コマンド列とカバーされたカバーポイントの関係を機械学習する．学習結果をもとにクロスカバレッジなどのカバレッジを改善する入力パタンの生成を行って，カバレッジ改善への影響を評価する．
|
| 次年度使用額が生じた理由 |
2022年度はコロナパンデミックの影響が残り，主要な研究集会がオンライン開催となり，旅費の支出が小さくなったことがひとつの要因である．また，計算機実験を部分的にクラウドサービスに頼ることにしたことと，一部のシステム実装の遅れから，使用額が当初予想を下回った．
網羅的な計算機実験には大きな計算機資源が必要となるため，次年度使用額については，システム開発用ワークステーションの購入とクラウドサービスの利用を念頭において，実験の充実を図る予定である．
|
