{"updated":"2025-01-19T16:36:09.592007+00:00","links":{},"id":214505,"created":"2025-01-19T01:15:19.233719+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00214505","sets":["6164:6165:6462:10749"]},"path":["10749"],"owner":"44499","recid":"214505","title":["HDLコードに対するSMTソルバを用いた自動検証システムの提案"],"pubdate":{"attribute_name":"公開日","attribute_value":"2021-10-19"},"_buckets":{"deposit":"96f37196-794b-4e55-b87f-ea5c5717691a"},"_deposit":{"id":"214505","pid":{"type":"depid","value":"214505","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"HDLコードに対するSMTソルバを用いた自動検証システムの提案","author_link":["551068","551060","551075","551057","551071","551059","551064","551067","551073","551074","551069","551072","551076","551070","551061","551058","551063","551065","551062","551066"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"HDLコードに対するSMTソルバを用いた自動検証システムの提案"},{"subitem_title":"A Testing System Using an SMT Solver for HDL Code","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"ハードウェア記述言語（HDL），ブランチカバレッジ，Satisfiability Modulo Theories (SMT)，FPGA，Register Transfer Level (RTL )","subitem_subject_scheme":"Other"}]},"item_type_id":"18","publish_date":"2021-10-19","item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_18_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構/株式会社ニッシン"},{"subitem_text_value":"国立研究開発法人情報通信研究機構/株式会社サイバーディフェンス研究所"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"},{"subitem_text_value":"国立研究開発法人情報通信研究機構"}]},"item_18_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology/Nissin Inc.","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology/Cyber Defense Institute, Inc.","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Information and Communications Technology","subitem_text_language":"en"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/214505/files/IPSJCSS2021105.pdf","label":"IPSJCSS2021105.pdf"},"date":[{"dateType":"Available","dateValue":"2023-10-19"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJCSS2021105.pdf","filesize":[{"value":"448.3 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"30"},{"tax":["include_tax"],"price":"0","billingrole":"46"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"bd3e9156-e3dc-4e70-b123-9a8f180f825c","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2021 by the Information Processing Society of Japan"}]},"item_18_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"伊沢, 亮一"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"金谷, 延幸"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"藤原, 吉唯"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"竹久, 達也"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"丑丸, 逸人"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"有末, 大"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"牧田, 大佑"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"三村, 聡志"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"末田, 卓巳"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"井上, 大介"}],"nameIdentifiers":[{}]}]},"item_18_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Ryoichi, Isawa","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Nobuyuki, Kanaya","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yoshitada, Fujiwara","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Tatsuta, Takehisa","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hayato, Ushimaru","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Dai, Arisue","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Daisuke, Makita","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Satoshi, Mimura","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Takumi, Sueda","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Daisuke, Inoue","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_5794","resourcetype":"conference paper"}]},"item_18_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"HDL（Hardware Description Language）コードをシミュレーションで検証する時，実行されていないステートメントは未検証となってしまうため，コードのカバレッジ（網羅率）が検証の品質を計測する重要な指標の一つとなる．一般的なランダム検証ではモジュール（HDLコード）への入力をランダムに決めるため，十分なカバレッジが得られないことがある．そこで我々はブランチカバレッジを100\\%にするための自動検証システムを提案する．提案システムの特徴はレジスタ値を直接設定する仕組みを検証対象のモジュールに入れ，モジュールの検証されていないステートに強制的に遷移させる点にある．これにより遷移先のステートメントを実行することでカバレッジを向上させる．モジュールへの入力とレジスタに設定する値はモジュールに含まれるif文などの条件をもとにSMT（Satisfiability Modulo Theories）ソルバを用いて求める．実験では一般に公開されているIPコア3つを用意し，提案システムによりブランチカバレッジがいずれも100\\%になることを確認した．加えて，ランダム検証の結果も比較対象として載せる．","subitem_description_type":"Other"}]},"item_18_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_18_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"785","bibliographic_titles":[{"bibliographic_title":"コンピュータセキュリティシンポジウム2021論文集"}],"bibliographicPageStart":"778","bibliographicIssueDates":{"bibliographicIssueDate":"2021-10-19","bibliographicIssueDateType":"Issued"}}]},"relation_version_is_last":true,"weko_creator_id":"44499"}}