This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
14th Asian Test Symposium (ATS'05)
An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications
Calcutta, India
December 18-December 21
ISBN: 0-7695-2481-8
ASCII Text
x 
 
Nikolaos D. Liveris, Hai Zhou, Prithviraj Banerjee, "An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications," 2012 IEEE 21st Asian Test Symposium, pp. 28-33, 14th Asian Test Symposium (ATS'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/ATS.2005.24,
author = {Nikolaos D. Liveris and Hai Zhou and Prithviraj Banerjee},
title = {An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications},
journal ={2012 IEEE 21st Asian Test Symposium},
volume = {0},
year = {2005},
issn = {1081-7735},
pages = {28-33},
doi = {http://doi.ieeecomputersociety.org/10.1109/ATS.2005.24},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - 2012 IEEE 21st Asian Test Symposium
TI - An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications
SN - 1081-7735
SP28
EP33
A1 - Nikolaos D. Liveris,
A1 - Hai Zhou,
A1 - Prithviraj Banerjee,
PY - 2005
KW - null
VL - 0
JA - 2012 IEEE 21st Asian Test Symposium
ER -
 
Nikolaos D. Liveris, Northwestern University, Evanston, IL
Hai Zhou, Northwestern University, Evanston, IL
Prithviraj Banerjee, University of Illinois, Chicago, IL
In this paper a new framework for formal verification is presented. The new framework called EVRM (Efficient VeRification based on Mathematica [1]) can be used for the property verification of a Register Transfer Level implementation using a System Level description as the golden model. EVRM is based on word level techniques and uses theMathematica tool for the satisfiability procedure. Results show that it can be orders of magnitude faster than CBMC [2] in proving property correctness or providing a counterexample for computation-intensive applications. For certain applications CBMC requires more than 5 hours to provide an answer, while EVRM provides an answer in less than 10 minutes.
Citation:
Nikolaos D. Liveris, Hai Zhou, Prithviraj Banerjee, "An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications," ats, pp.28-33, 14th Asian Test Symposium (ATS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.