loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2003 IEEE International Conference on Computer Design (ICCD'03)
Verification of Timed Circuits with Failure Directed Abstractions
San Jose, California
October 13-October 15
ISBN: 0-7695-2025-1
ASCII Text
x 
 
Hao Zheng, Chris J. Myers, David Walter, Scott Little, Tomohiro Yoneda, "Verification of Timed Circuits with Failure Directed Abstractions," Computer Design, International Conference on, pp. 28, 2003 IEEE International Conference on Computer Design (ICCD'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/ICCD.2003.1240869,
author = {Hao Zheng and Chris J. Myers and David Walter and Scott Little and Tomohiro Yoneda},
title = {Verification of Timed Circuits with Failure Directed Abstractions},
journal ={Computer Design, International Conference on},
volume = {0},
year = {2003},
issn = {1063-6404},
pages = {28},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICCD.2003.1240869},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Design, International Conference on
TI - Verification of Timed Circuits with Failure Directed Abstractions
SN - 1063-6404
SP
EP
A1 - Hao Zheng,
A1 - Chris J. Myers,
A1 - David Walter,
A1 - Scott Little,
A1 - Tomohiro Yoneda,
PY - 2003
KW - null
VL - 0
JA - Computer Design, International Conference on
ER -
 
Hao Zheng, IBM Microelectronics in Burlington, VT
Chris J. Myers, University of Utah, Salt Lake City
David Walter, University of Utah, Salt Lake City
Scott Little, University of Utah, Salt Lake City
Tomohiro Yoneda, National Institute of Informatics in Tokyo, Japan.
This paper presents a method to address state explosion in timed circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that a specific failure condition does not occur. To each subproblem, abstraction is applied using safe transformations to reduce the complexity of verification. The abstraction preserves all essential behaviors conservatively for the specific failure model in the concrete description. Therefore, no violations of the given failure model are missed when only the abstract description is analyzed. An algorithm is also shown to examine the abstract error trace to either find a concrete error trace or report that it is a false negative. This paper presents results using the proposed failure directed abstractions as applied to two large timed circuit designs.
Citation:
Hao Zheng, Chris J. Myers, David Walter, Scott Little, Tomohiro Yoneda, "Verification of Timed Circuits with Failure Directed Abstractions," iccd, pp.28, 2003 IEEE International Conference on Computer Design (ICCD'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.