2023 Fiscal Year Research-status Report
入出力プロトコルに着目した機械学習によるカバレッジ駆動検証システムに関する研究
| Project/Area Number |
22K11962
|
|---|
| Research Institution | Kyoto Tachibana University |
|---|
Principal Investigator |
浜口 清治 京都橘大学, 工学部, 教授 (80238055)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | 設計自動化 / カバレッジ駆動検証 / SATソルバ |
|---|
| Outline of Annual Research Achievements |
本研究では，ディジタル回路設計において手数の多い論理・レジスタ転送レベルでの設計検証を，可能なかぎり自動化することを目標としている．本研究における主な目標は特に標準規格の入出力プロトコルを持つ回路設計を対象として，SATソルバ(Satisfiability Solver， 論理式の充足可能性判定器)および機械学習を用いた手法を確立することである. 2023年度は具体的には次のような成果を得た.
(a)ブランチカバレッジを対象としたカバレッジ検証の評価
本年度は昨年度に引き続き，設計記述内の分岐条件に関するカバレッジ(ブランチカバレッジ)について評価を行った．すでにランダムシミュレーションのみではなく，SATソルバを組み合わせることによって，カバレッジを改善できることが確認できていたが，さらに信号線の変化パターンについて，中間結果に基づいて重みづけを動的に変えることによって，カバレッジが速度的にも量的にも改善されることを確認した．
(b)入出力プロトコルを前提とした自動検証手法の確立と評価
標準規格のAMBA AXI プロトコルをターゲットとしているが，設計回路例の作成が遅れており，今年度はより単純なプロトコルである Wishboneを対象に計算機実験を実施した．方法としては，Wishbone のラッパーの記述を，ハードウェア記述言語により作成し，開発中の検証システムを用いて実験を行った．その結果，カバレッジが約15％改善できることが確認できた．現状1例のみの試行となっているが，有望な結果とみており，実験を拡充していく予定である．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
入出力プロトコルを前提とした自動検証手法については，基本的なしくみは確定しており， Wishbone プロトコルを使った予備的な実験は行っているが，AMBA AXI プロトコルへの対応が想定より手数がかかっていて進捗が遅れている.
|
| Strategy for Future Research Activity |
(a) 入出力プロトコルを前提とした自動検証手法の確立と評価
2023年度はより簡単な Wishbone プロトコルに関する基礎実験に止まったが，2024年度は FPGA 等のインターフェースでよく用いられている AMBA AXIに対する自動検証を行う実験を行い定量的な評価を行う．
(b) 機械学習とSATソルバを用いた方式の評価
この手法では，ランダムパタンの生成をどうするかが課題であるが，2023年度の実験で，信号線の変化パターンに対して，重みづけを適応的に変化させることが判明している．この結果を踏まえて，重みづけの学習を行い，クロスカバレッジなどのカバレッジを改善する入力パタンの生成を行う実験を行い，カバレッジ改善への影響を評価する
|
| Causes of Carryover |
計算機実験における計算時間を短縮するため，複数の計算機を使う必要があったが，ワークステーション購入に比べてクラウドサービスを利用したほうが，柔軟な対応が可能であることが判明した．このため，システム実装用の計算機を除き，クラウドサービスを利用する運用とした結果，支出が当初予定を下回った．次年度使用分については，クラウドサービスの利用を念頭において，実験の拡充に充当する予定である.
|
