DocumentCode :
2219828
Title :
Verification of timed circuits with failure directed abstractions
Author :
Zheng, Hao ; Myers, Chris J. ; Walter, David ; Little, Scott ; Yoneda, Tomohiro
Author_Institution :
Utah Univ., Salt Lake City, UT, USA
fYear :
2003
fDate :
13-15 Oct. 2003
Firstpage :
28
Lastpage :
35
Abstract :
We present 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. We present results using the proposed failure directed abstractions as applied to two large timed circuit designs.
Keywords :
formal verification; reachability analysis; timing circuits; failure directed abstraction; failure model; reachability analysis; state explosion; timed circuit verification; Boolean functions; Circuits; Cities and towns; Concrete; Data structures; Explosions; Failure analysis; Interleaved codes; State-space methods; Timing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Design, 2003. Proceedings. 21st International Conference on
ISSN :
1063-6404
Print_ISBN :
0-7695-2025-1
Type :
conf
DOI :
10.1109/ICCD.2003.1240869
Filename :
1240869
Link To Document :
بازگشت