Name
Abstract | ||
|---|---|---|
Abstract— This paper,addresses,the presence,of logic which has,relevance,only during,initial time,frames,in a hardware design. We examine,transient logic in the form,of signals which settle to deterministic constants after some,prefix number,of time frames, as well as primary inputs used to enumerate complex initial states which,thereafter,become,irrelevant. Experience shows that a large percentage,of hardware,designs (industrial and benchmarks) have such logic, and this creates overhead in the overall verification process. In this paper, we present automated techniques to detect and eliminate such irrelevant logic, enabling verification efficiencies in terms of greater logic reductions, deeper Bounded Model Checking (BMC), and enhanced proof capability using induction,and,interpolation. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/FMCAD.2009.5351146 | FMCAD |
Keywords | DocType | Citations |
data mining,computational complexity,history,interpolation,registers,temporal logic,algorithm design and analysis,benchmark testing | Conference | 4 |
PageRank | References | Authors |
0.44 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael L. Case | 1 | 4 | 0.44 |
| Hari Mony | 2 | 186 | 13.30 |
| Jason Baumgartner | 3 | 313 | 23.36 |
| Robert Kanzelman | 4 | 107 | 6.16 |