@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00214505,
 author = {伊沢, 亮一 and 金谷, 延幸 and 藤原, 吉唯 and 竹久, 達也 and 丑丸, 逸人 and 有末, 大 and 牧田, 大佑 and 三村, 聡志 and 末田, 卓巳 and 井上, 大介 and Ryoichi, Isawa and Nobuyuki, Kanaya and Yoshitada, Fujiwara and Tatsuta, Takehisa and Hayato, Ushimaru and Dai, Arisue and Daisuke, Makita and Satoshi, Mimura and Takumi, Sueda and Daisuke, Inoue},
 book = {コンピュータセキュリティシンポジウム2021論文集},
 month = {Oct},
 note = {HDL（Hardware Description Language）コードをシミュレーションで検証する時，実行されていないステートメントは未検証となってしまうため，コードのカバレッジ（網羅率）が検証の品質を計測する重要な指標の一つとなる．一般的なランダム検証ではモジュール（HDLコード）への入力をランダムに決めるため，十分なカバレッジが得られないことがある．そこで我々はブランチカバレッジを100\%にするための自動検証システムを提案する．提案システムの特徴はレジスタ値を直接設定する仕組みを検証対象のモジュールに入れ，モジュールの検証されていないステートに強制的に遷移させる点にある．これにより遷移先のステートメントを実行することでカバレッジを向上させる．モジュールへの入力とレジスタに設定する値はモジュールに含まれるif文などの条件をもとにSMT（Satisfiability Modulo Theories）ソルバを用いて求める．実験では一般に公開されているIPコア3つを用意し，提案システムによりブランチカバレッジがいずれも100\%になることを確認した．加えて，ランダム検証の結果も比較対象として載せる．, 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.},
 pages = {778--785},
 publisher = {情報処理学会},
 title = {HDLコードに対するSMTソルバを用いた自動検証システムの提案},
 year = {2021}
}