講演抄録/キーワード |
講演名 |
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 |