| 講演名 | 2016-02-29 Verilog-HDLによる大規模ハードウェア設計の検証支援ツールの開発 森光 勇太(岡山県立大), 横川 智教(岡山県立大), 近藤 真史(川崎医療福祉大), 宮崎 仁(川崎医療福祉大), 佐藤 洋一郎(岡山県立大), 有本 和民(岡山県立大), 吉田 則裕(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では，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 |
| 資料番号 | VLD2015-111 |
| 発行日 | 2016-02-22 (VLD) |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2016/2/29(から3日開催) |
| 開催地（和） | 沖縄県青年会館 |
| 開催地（英） | Okinawa Seinen Kaikan |
| テーマ（和） | システムオンシリコンを支える設計技術 |
| テーマ（英） | |
| 委員長氏名（和） | 松永 裕介(九大) |
| 委員長氏名（英） | Yusuke Matsunaga(Kyushu Univ.) |
| 副委員長氏名（和） | 竹中 崇(NEC) |
| 副委員長氏名（英） | Takashi Takenana(NEC) |
| 幹事氏名（和） | 冨山 宏之(立命館大) / 福田 大輔(富士通研) |
| 幹事氏名（英） | Hiroyuki Tomiyama(Ritsumeikan Univ.) / Daisuke Fukuda(Fujitsu Labs.) |
| 幹事補佐氏名（和） | 谷口 一徹(立命館大) |
| 幹事補佐氏名（英） | Ittetsu Taniguchi(Ritsumeikan Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on VLSI Design Technologies |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Verilog-HDLによる大規模ハードウェア設計の検証支援ツールの開発 |
| サブタイトル（和） | |
| タイトル（英） | Tool Support for Verifying Large Scale Hardware Design with Verilog-HDL |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | モデル検査 / model checking |
| キーワード(3)（和/英） | NuSMV / NuSMV |
| 第 1 著者 氏名（和/英） | 森光 勇太 / Yuta Morimitsu |
| 第 1 著者 所属（和/英） | 岡山県立大学(略称：岡山県立大) Okayama Prefectural University(略称：Okayama Prefectural Univ.) |
| 第 2 著者 氏名（和/英） | 横川 智教 / Tomoyuki Yokogawa |
| 第 2 著者 所属（和/英） | 岡山県立大学(略称：岡山県立大) Okayama Prefectural University(略称：Okayama Prefectural Univ.) |
| 第 3 著者 氏名（和/英） | 近藤 真史 / Masafumi Kondo |
| 第 3 著者 所属（和/英） | 川崎医療福祉大学(略称：川崎医療福祉大) Kawasaki University of Medical Welfare(略称：Kawasaki Univ. of Medical Welfare) |
| 第 4 著者 氏名（和/英） | 宮崎 仁 / Hisashi Miyazaki |
| 第 4 著者 所属（和/英） | 川崎医療福祉大学(略称：川崎医療福祉大) Kawasaki University of Medical Welfare(略称：Kawasaki Univ. of Medical Welfare) |
| 第 5 著者 氏名（和/英） | 佐藤 洋一郎 / Yoichiro Sato |
| 第 5 著者 所属（和/英） | 岡山県立大学(略称：岡山県立大) Okayama Prefectural University(略称：Okayama Prefectural Univ.) |
| 第 6 著者 氏名（和/英） | 有本 和民 / Kazutami Arimoto |
| 第 6 著者 所属（和/英） | 岡山県立大学(略称：岡山県立大) Okayama Prefectural University(略称：Okayama Prefectural Univ.) |
| 第 7 著者 氏名（和/英） | 吉田 則裕 / Norihiro Yoshida |
| 第 7 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2016-02-29 |
| 資料番号 | VLD2015-111 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | VLD-465 |
| ページ範囲 | pp.1-6(VLD), |
| ページ数 | 6 |
| 発行日 | 2016-02-22 (VLD) |