| Item type |
Symposium(1) |
| 公開日 |
2021-10-19 |
| タイトル |
|
|
タイトル |
HDLコードに対するSMTソルバを用いた自動検証システムの提案 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
A Testing System Using an SMT Solver for HDL Code |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
ハードウェア記述言語（HDL），ブランチカバレッジ，Satisfiability Modulo Theories (SMT)，FPGA，Register Transfer Level (RTL ) |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構/株式会社ニッシン |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構/株式会社サイバーディフェンス研究所 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属 |
|
|
|
国立研究開発法人情報通信研究機構 |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology/Nissin Inc. |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology/Cyber Defense Institute, Inc. |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Information and Communications Technology |
| 著者名 |
伊沢, 亮一
金谷, 延幸
藤原, 吉唯
竹久, 達也
丑丸, 逸人
有末, 大
牧田, 大佑
三村, 聡志
末田, 卓巳
井上, 大介
|
| 著者名(英) |
Ryoichi, Isawa
Nobuyuki, Kanaya
Yoshitada, Fujiwara
Tatsuta, Takehisa
Hayato, Ushimaru
Dai, Arisue
Daisuke, Makita
Satoshi, Mimura
Takumi, Sueda
Daisuke, Inoue
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
HDL（Hardware Description Language）コードをシミュレーションで検証する時，実行されていないステートメントは未検証となってしまうため，コードのカバレッジ（網羅率）が検証の品質を計測する重要な指標の一つとなる．一般的なランダム検証ではモジュール（HDLコード）への入力をランダムに決めるため，十分なカバレッジが得られないことがある．そこで我々はブランチカバレッジを100\%にするための自動検証システムを提案する．提案システムの特徴はレジスタ値を直接設定する仕組みを検証対象のモジュールに入れ，モジュールの検証されていないステートに強制的に遷移させる点にある．これにより遷移先のステートメントを実行することでカバレッジを向上させる．モジュールへの入力とレジスタに設定する値はモジュールに含まれるif文などの条件をもとにSMT（Satisfiability Modulo Theories）ソルバを用いて求める．実験では一般に公開されているIPコア3つを用意し，提案システムによりブランチカバレッジがいずれも100\%になることを確認した．加えて，ランダム検証の結果も比較対象として載せる． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
When a module in HLD code is tested using a simulation, HDL-code coverage is one of the most important metrics for testing because part of the code is not checked if it is not executed. This makes it necessary to obtain as high coverage as possible. In this paper, we propose a testing system for modules written in HDL code, aiming at a branch coverage of 100\% during a simulation. For this aim, our system previously inserts input pins to a target module for directly setting its register values. Our system then automatically changes the current state of a module to another state during a simulation by setting the corresponding registers via the inserted pins. At this time, our system uses an SMT solver to obtain such register values for the state transition by satisfying branch-conditions contained in a module. |
| 書誌情報 |
コンピュータセキュリティシンポジウム2021論文集
p. 778-785,
発行日 2021-10-19
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJCSS2021105.pdf (448.3 kB)
