文献

J-GLOBAL ID：201402293570921338   整理番号：14A0569261

VerilogHDLによるハードウェア設計への記号モデル検査の適用事例

A Case Study of Symbolic Model Checking for Verilog-HDL Hardware Design

著者 (5件)： 横川智教 (岡山県大) ,  東山大地 (岡山県大) ,  近藤真史 (川崎医療福祉大) ,  佐藤洋一郎 (岡山県大) ,  有本和民 (岡山県大)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 113  号： 454(VLD2013 134-167)  ページ： 177-182  発行年： 2014年02月24日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 従来のランダムテストによるIP検証では,検証の網羅性を保証することが極めて困難であることから,モデル検査による形式的検証の適用への要求が高まっている。しかしながら,モデル検査の検証コストが対象システムの規模に対して指数的に増大する,いわゆる状態爆発問題が発生することから,実問題への適用は十分に進められているとはいえない。本稿では,記号モデル検査ツールNuSMVをVerilog-HDLによる8ビットマイコンM8Rの設計記述に適用した事例について報告する。まず,Verilog-HDLの記述をNuSMVの入力であるSMV言語によるモデルへとマッピングするための枠組みについて示す。また,モデルサイズ削減のためのHDL記述の簡単化についてのアプローチについても示す。最後に,M8Rの命令セットのデコーダ部分のみを抽出してSMV言語でモデル化し,NuSMVによる検証を実施した結果について示す。(著者抄録)

シソーラス用語： *ハードウェア記述言語 ,  *ハードウェア設計 ,  *モデル検査 ,  *検証 ,  論理合成 ,  *回路設計 ,  知的財産権 ,  二分決定グラフ ,  再利用 ,  *集積回路 ,  回路モデル ,  モデリング
準シソーラス用語： Verilog ,  形式検証 ,  記号モデル検査

分類 (1件)： 集積回路一般  (NC03161C)

引用文献 (7件)：

• E. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999.
• K.L. McMillan, Symbolic Model Checking, Kluwer Academic, 1993.
• “Nusmv”. http://nusmv.irst.itc.it/.
• R.E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Trans. Computers, vol.35, no.8, pp.677-691, 1986.
• A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” In Proc. of the 5th Int'l Conf. on Tools and Algorithms for Construction and Analysis of Systems(TACAS'99), pp.193-207, 1999.

タイトルに関連する用語 (4件)： ハードウェア設計 ,  記号 ,  モデル検査 ,  適用事例