入出力プロトコルに着目した機械学習によるカバレッジ駆動検証システムに関する研究

本研究の目的は特に標準規格の入出力プロトコルを持つ回路設計を対象として，SATソルバ(Satisfiability Solver， 論理式の充足可能性判定器)および機械学習を用いた手法を確立することである． 　2022年度は具体的には次のような成果を得た．(a) 並行プロセスによるカバレッジ検証の効率の評価まず，トグルカバレッジをターゲットとして評価を行った．報告者による先行研究では，ランダムシミュレーションとSATソルバーを用いた入力パターン生成を組み合わせたアプローチを提案しており，実験を通じて有効であることがわかっていた．しかし、検証プロセスにおいてSATソルバーの実行時間が支配的要素であるため、これが検証プロセスの進行を妨げていることが判明していた。これを改良するために、ランダム/SATベースの処理を並列化することで、この先行研究を拡張した．実験の結果、並列化のアプローチがカバレッジ改善のために有効であることが示された．本結果については論文として投稿し，採録が決まっている(発行は2023年6月)．(b) ブランチカバレッジを対象としたカバレッジ検証の評価本年度はさらに，設計記述内の分岐条件に関するカバレッジ(ブランチカバレッジ)について評価を行った．ブランチカバレッジについてはすでに他の研究グループによる評価結果が出ているが，本研究ではランダムシミュレーションのみではなく，SATソルバを組み合わせることによって，カバレッジを改善できることが確認できた．またランダムパタンについても信号線の変化に着目した生成を行うことにより，より良いカバレッジ改善が得られることを確認した．

本研究の目的は特に標準規格の入出力プロトコルを持つ回路設計を対象として，SATソルバ(Satisfiability Solver， 論理式の充足可能性判定器)および機械学習を用いた手法を確立することである． 　2022年度は具体的には次のような成果を得た．(a) 並行プロセスによるカバレッジ検証の効率の評価まず，トグルカバレッジをターゲットとして評価を行った．報告者による先行研究では，ランダムシミュレーションとSATソルバーを用いた入力パターン生成を組み合わせたアプローチを提案しており，実験を通じて有効であることがわかっていた．しかし、検証プロセスにおいてSATソルバーの実行時間が支配的要素であるため、これが検証プロセスの進行を妨げていることが判明していた。これを改良するために、ランダム/SATベースの処理を並列化することで、この先行研究を拡張した．実験の結果、並列化のアプローチがカバレッジ改善のために有効であることが示された．本結果については論文として投稿し，採録が決まっている(発行は2023年6月)．(b) ブランチカバレッジを対象としたカバレッジ検証の評価本年度はさらに，設計記述内の分岐条件に関するカバレッジ(ブランチカバレッジ)について評価を行った．ブランチカバレッジについてはすでに他の研究グループによる評価結果が出ているが，本研究ではランダムシミュレーションのみではなく，SATソルバを組み合わせることによって，カバレッジを改善できることが確認できた．またランダムパタンについても信号線の変化に着目した生成を行うことにより，より良いカバレッジ改善が得られることを確認した．