講演抄録/キーワード |
講演名 |
2016-02-29 13:30
Verilog-HDLによる大規模ハードウェア設計の検証支援ツールの開発 ○森光勇太・横川智教(岡山県立大)・近藤真史・宮崎 仁(川崎医療福祉大)・佐藤洋一郎・有本和民(岡山県立大)・吉田則裕(名大) VLD2015-111 |
抄録 |
(和) |
本稿では,Verilog-HDLで記述された大規模ハードウェア設計の検証支援ツールについて報告する.
検証には,フォーマル検証技術の一種である記号モデル検査に基づく検証器であるNuSMVを用いる.
本ツールでは,Verilog-HDLによる設計記述を,NuSMVの入力となるSMVプログラムへと自動的に変換する.
また,Verilogコードの構文解析にはpyverilogを用いており,pyverilogが生成した抽象構文木を入力として,SMVプログラムの生成を行う. |
(英) |
In this paper, we developed a tool supporting formal verification of large scale hardware design described by Verilog-HDL.
We use a model-checker NuSMV which supports symbolic mode checking.
Symbolic model checking is one of formal verification techniques and can avoid state explosion problem by representing a state transition graph as a boolean formula.
Our tool translates a hardware design described by Verilog-HDL into an SMV program which is an input of NuSMV.
We use pyverilog toolkit for parsing Verilog code and our tool outputs the SMV program from abstract syntactic tree which is generated by pyverilog. |
キーワード |
(和) |
形式的検証 / モデル検査 / NuSMV / / / / / |
(英) |
formal verification / model checking / NuSMV / / / / / |
文献情報 |
信学技報, vol. 115, no. 465, VLD2015-111, pp. 1-6, 2016年2月. |
資料番号 |
VLD2015-111 |
発行日 |
2016-02-22 (VLD) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
VLD2015-111 |