IEICE Technical Committee Submission System
Conference Paper's Information
Online Proceedings
[Sign in]
... (for ESS/CS/ES/ISS)
Tech. Rep. Archives
... (for ES/CS)
 Go Top Page Go Previous   [Japanese] / [English] 

Paper Abstract and Keywords
Presentation 2016-02-29 13:30
Tool Support for Verifying Large Scale Hardware Design with Verilog-HDL
Yuta Morimitsu, Tomoyuki Yokogawa (Okayama Prefectural Univ.), Masafumi Kondo, Hisashi Miyazaki (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Prefectural Univ.), Norihiro Yoshida (Nagoya Univ.)
Abstract (in Japanese) (See Japanese page) 
(in English) 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.
Keyword (in Japanese) (See Japanese page) 
(in English) formal verification / model checking / NuSMV / / / / /  
Reference Info. IEICE Tech. Rep., vol. 115, no. 465, VLD2015-111, pp. 1-6, Feb. 2016.
Paper # VLD2015-111 
Date of Issue 2016-02-22 (VLD) 
ISSN Print edition: ISSN 0913-5685  Online edition: ISSN 2432-6380

Conference Information
Committee VLD  
Conference Date 2016-02-29 - 2016-03-02 
Place (in Japanese) (See Japanese page) 
Place (in English) Okinawa Seinen Kaikan 
Topics (in Japanese) (See Japanese page) 
Topics (in English)  
Paper Information
Registration To VLD 
Conference Code 2016-02-VLD 
Language Japanese 
Title (in Japanese) (See Japanese page) 
Sub Title (in Japanese) (See Japanese page) 
Title (in English) Tool Support for Verifying Large Scale Hardware Design with Verilog-HDL 
Sub Title (in English)  
Keyword(1) formal verification  
Keyword(2) model checking  
Keyword(3) NuSMV  
Keyword(4)  
Keyword(5)  
Keyword(6)  
Keyword(7)  
Keyword(8)  
1st Author's Name Yuta Morimitsu  
1st Author's Affiliation Okayama Prefectural University (Okayama Prefectural Univ.)
2nd Author's Name Tomoyuki Yokogawa  
2nd Author's Affiliation Okayama Prefectural University (Okayama Prefectural Univ.)
3rd Author's Name Masafumi Kondo  
3rd Author's Affiliation Kawasaki University of Medical Welfare (Kawasaki Univ. of Medical Welfare)
4th Author's Name Hisashi Miyazaki  
4th Author's Affiliation Kawasaki University of Medical Welfare (Kawasaki Univ. of Medical Welfare)
5th Author's Name Yoichiro Sato  
5th Author's Affiliation Okayama Prefectural University (Okayama Prefectural Univ.)
6th Author's Name Kazutami Arimoto  
6th Author's Affiliation Okayama Prefectural University (Okayama Prefectural Univ.)
7th Author's Name Norihiro Yoshida  
7th Author's Affiliation Nagoya University (Nagoya Univ.)
8th Author's Name  
8th Author's Affiliation ()
9th Author's Name  
9th Author's Affiliation ()
10th Author's Name  
10th Author's Affiliation ()
11th Author's Name  
11th Author's Affiliation ()
12th Author's Name  
12th Author's Affiliation ()
13th Author's Name  
13th Author's Affiliation ()
14th Author's Name  
14th Author's Affiliation ()
15th Author's Name  
15th Author's Affiliation ()
16th Author's Name  
16th Author's Affiliation ()
17th Author's Name  
17th Author's Affiliation ()
18th Author's Name  
18th Author's Affiliation ()
19th Author's Name  
19th Author's Affiliation ()
20th Author's Name  
20th Author's Affiliation ()
Speaker
Date Time 2016-02-29 13:30:00 
Presentation Time 25 
Registration for VLD 
Paper # IEICE-VLD2015-111 
Volume (vol) IEICE-115 
Number (no) no.465 
Page pp.1-6 
#Pages IEICE-6 
Date of Issue IEICE-VLD-2016-02-22 


[Return to Top Page]

[Return to IEICE Web Page]


The Institute of Electronics, Information and Communication Engineers (IEICE), Japan