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
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;
Conference_Titel :
Computer Design, 2003. Proceedings. 21st International Conference on
Print_ISBN :
0-7695-2025-1
DOI :
10.1109/ICCD.2003.1240869