loading...
HW/SW Co-Verification of a RISC CPU using Bounded Model Checking
Austin, Texas November 03-November 05
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MTV.2005.12Sixth International Workshop on Micro ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Daniel Gro?e, Ulrich K?, Rolf Drechsler, "HW/SW Co-Verification of a RISC CPU using Bounded Model Checking," Microprocessor Test and Verification, International Workshop on, pp. 133-137, Sixth International Workshop on Microprocessor Test and Verification (MTV'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/MTV.2005.12,
author = {Daniel Gro?e and Ulrich K? and Rolf Drechsler},
title = {HW/SW Co-Verification of a RISC CPU using Bounded Model Checking},
journal ={Microprocessor Test and Verification, International Workshop on},
volume = {0},
year = {2005},
issn = {1550-4093},
pages = {133-137},
doi = {http://doi.ieeecomputersociety.org/10.1109/MTV.2005.12},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Microprocessor Test and Verification, International Workshop on
TI - HW/SW Co-Verification of a RISC CPU using Bounded Model Checking
SN - 1550-4093
SP133
EP137
A1 - Daniel Gro?e,
A1 - Ulrich K?,
A1 - Rolf Drechsler,
PY - 2005
KW - null
VL - 0
JA - Microprocessor Test and Verification, International Workshop on
ER -
 
Daniel Gro?e, University of Bremen, Germany
Ulrich K?, University of Bremen, Germany
Rolf Drechsler, University of Bremen, Germany
Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.
Citation:
Daniel Gro?e, Ulrich K?, Rolf Drechsler, "HW/SW Co-Verification of a RISC CPU using Bounded Model Checking," mtv, pp.133-137, Sixth International Workshop on Microprocessor Test and Verification (MTV'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.