Name
Abstract | ||
|---|---|---|
This paper presents a method to address state explosion in timedcircuit verification by using abstraction directed by the failuremodel. This method allows us to decompose the verification probleminto a set of subproblems, each of which proves that a specificfailure condition does not occur. To each subproblem, abstractionis applied using safe transformations to reduce the complexity ofverification. The abstraction preserves all essential behaviorsconservatively for the specific failure model in the concretedescription. Therefore, no violations of the given failure modelare missed when only the abstract description is analyzed. Analgorithm is also shown to examine the abstract error trace toeither find a concrete error trace or report that it is a falsenegative. This paper presents results using the proposed failuredirected abstractions as applied to two large timed circuitdesigns. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/TCAD.2005.854638 | IEEE Trans. on CAD of Integrated Circuits and Systems |
Keywords | DocType | Volume |
failure model,abstraction.,concrete description,verification problem,abstract description,specific failure model,timed-circuit verification,index terms— timed circuits,essential behaviorsconservatively,failure modelare,proposed failure-directed abstraction,formal verification,specific failure condition,abstract error trace,failure directed abstractions,timedcircuit verification,proposed failuredirected abstraction,complexity ofverification,concrete error trace,verification probleminto,timed circuits,indexing terms,circuit design | Journal | 25 |
Issue | ISSN | ISBN |
3 | 1063-6404 | 0-7695-2025-1 |
Citations | PageRank | References |
8 | 0.53 | 31 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hao Zheng | 1 | 95 | 13.32 |
| Chris J. Myers | 2 | 607 | 75.73 |
| David Walter | 3 | 98 | 5.38 |
| Scott Little | 4 | 132 | 9.42 |
| Tomohiro Yoneda | 5 | 353 | 41.62 |