お知らせ 2023年度・2024年度 学生員 会費割引キャンペーン実施中です
お知らせ 技術研究報告と和文論文誌Cの同時投稿施策(掲載料1割引き)について
お知らせ 電子情報通信学会における研究会開催について
お知らせ NEW 参加費の返金について
電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
[ログイン]
技報アーカイブ
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2014-03-05 15:45
VerilogHDLによるハードウェア設計への記号モデル検査の適用事例
横川智教東山大地岡山県立大)・近藤真史川崎医療福祉大)・佐藤洋一郎有本和民岡山県立大VLD2013-166
抄録 (和) 従来のランダムテストによるIP検証では,検証の網羅性を保証することが極めて困難であることから,モデル検査による形式的検証の適用への要求が高まっている.しかしながら,モデル検査の検証コストが対象システムの規模に対して指数的に増大する,いわゆる状態爆発問題が発生することから,実問題への適用は十分に進められているとはいえない.本稿では,記号モデル検査ツールNuSMVをVerilog-HDLによる8ビットマイコンM8Rの設計記述に適用した事例について報告する.まず,Verilog-HDLの記述をNuSMVの入力であるSMV言語によるモデルへとマッピングするための枠組みについて示す.また,モデルサイズ削減のためのHDL記述の簡単化についてのアプローチについても示す.最後に,M8Rの命令セットのデコーダ部分のみを抽出してSMV言語でモデル化し,NuSMVによる検証を実施した結果について示す. 
(英) In this paper, we show a case study where a design of 8bit microcomputer M8R, which is described by Verilog-HDL, is verified using symbolic model checker NuSMV.We provide a framework for translating a Verilog-HDL description into an SMV model.We also show approaches to simplify the Verilog-HDL description for model size reduction.We extract the decode procedure of M8R and represent the procedure as an input of SMV.We show the verification results using NuSMV.
キーワード (和) 形式検証 / Verilog-HDL / 記号モデル検査 / SMV / / / /  
(英) formal verification / Velilog-HDL / symbolic model checking / SMV / / / /  
文献情報 信学技報, vol. 113, no. 454, VLD2013-166, pp. 177-182, 2014年3月.
資料番号 VLD2013-166 
発行日 2014-02-24 (VLD) 
ISSN Print edition: ISSN 0913-5685    Online edition: ISSN 2432-6380
著作権に
ついて
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034)
PDFダウンロード VLD2013-166

研究会情報
研究会 VLD  
開催期間 2014-03-03 - 2014-03-05 
開催地(和) 沖縄県青年会館 
開催地(英) Okinawa Seinen Kaikan 
テーマ(和) システムオンシリコンを支える設計技術 
テーマ(英) Design Technology for System-on-Silicon 
講演論文情報の詳細
申込み研究会 VLD 
会議コード 2014-03-VLD 
本文の言語 日本語 
タイトル(和) VerilogHDLによるハードウェア設計への記号モデル検査の適用事例 
サブタイトル(和)  
タイトル(英) A Case Study of Symbolic Model Checking for Verilog-HDL Hardware Design 
サブタイトル(英)  
キーワード(1)(和/英) 形式検証 / formal verification  
キーワード(2)(和/英) Verilog-HDL / Velilog-HDL  
キーワード(3)(和/英) 記号モデル検査 / symbolic model checking  
キーワード(4)(和/英) SMV / SMV  
キーワード(5)(和/英) /  
キーワード(6)(和/英) /  
キーワード(7)(和/英) /  
キーワード(8)(和/英) /  
第1著者 氏名(和/英/ヨミ) 横川 智教 / Tomoyuki Yokogawa / ヨコガワ トモユキ
第1著者 所属(和/英) 岡山県立大学 (略称: 岡山県立大)
Okayama Prefectural University (略称: Okayama Pref. Univ.)
第2著者 氏名(和/英/ヨミ) 東山 大地 / Daichi Higashiyama / ヒガシヤマ ダイチ
第2著者 所属(和/英) 岡山県立大学 (略称: 岡山県立大)
Okayama Prefectural University (略称: Okayama Pref. Univ.)
第3著者 氏名(和/英/ヨミ) 近藤 真史 / Masafumi Kondo / サトウ ヨウイチロウ
第3著者 所属(和/英) 川崎医療福祉大学 (略称: 川崎医療福祉大)
Kawasaki University of Medical Welware (略称: Kawasaki Univ. of Medical Welfare)
第4著者 氏名(和/英/ヨミ) 佐藤 洋一郎 / Yoichiro Sato / アリモト カズタミ
第4著者 所属(和/英) 岡山県立大学 (略称: 岡山県立大)
Okayama Prefectural University (略称: Okayama Pref. Univ.)
第5著者 氏名(和/英/ヨミ) 有本 和民 / Kazutami Arimoto /
第5著者 所属(和/英) 岡山県立大学 (略称: 岡山県立大)
Okayama Prefectural University (略称: Okayama Pref. Univ.)
第6著者 氏名(和/英/ヨミ) / /
第6著者 所属(和/英) (略称: )
(略称: )
第7著者 氏名(和/英/ヨミ) / /
第7著者 所属(和/英) (略称: )
(略称: )
第8著者 氏名(和/英/ヨミ) / /
第8著者 所属(和/英) (略称: )
(略称: )
第9著者 氏名(和/英/ヨミ) / /
第9著者 所属(和/英) (略称: )
(略称: )
第10著者 氏名(和/英/ヨミ) / /
第10著者 所属(和/英) (略称: )
(略称: )
第11著者 氏名(和/英/ヨミ) / /
第11著者 所属(和/英) (略称: )
(略称: )
第12著者 氏名(和/英/ヨミ) / /
第12著者 所属(和/英) (略称: )
(略称: )
第13著者 氏名(和/英/ヨミ) / /
第13著者 所属(和/英) (略称: )
(略称: )
第14著者 氏名(和/英/ヨミ) / /
第14著者 所属(和/英) (略称: )
(略称: )
第15著者 氏名(和/英/ヨミ) / /
第15著者 所属(和/英) (略称: )
(略称: )
第16著者 氏名(和/英/ヨミ) / /
第16著者 所属(和/英) (略称: )
(略称: )
第17著者 氏名(和/英/ヨミ) / /
第17著者 所属(和/英) (略称: )
(略称: )
第18著者 氏名(和/英/ヨミ) / /
第18著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者 第1著者 
発表日時 2014-03-05 15:45:00 
発表時間 25分 
申込先研究会 VLD 
資料番号 VLD2013-166 
巻番号(vol) vol.113 
号番号(no) no.454 
ページ範囲 pp.177-182 
ページ数
発行日 2014-02-24 (VLD) 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会