Name
Abstract | ||
|---|---|---|
Abstraction is central to formal verification. In term-level abstraction, the design is abstracted using a fragment of first-order logic with background theories, such as the theory of uninterpreted functions with equality. The main challenge in using term-level abstraction is determining what components to abstract and under what conditions. In this paper, we present an automatic technique to conditionally abstract register transfer level (RTL) hardware designs to the term level. Our approach is a layered approach that combines random simulation and machine learning inside a counter-example guided abstraction refinement (CEGAR) loop. First, random simulation is used to determine modules that are candidates for abstraction. Next, machine learning is used on the resulting simulation traces to generate candidate conditions under which those modules can be abstracted. Finally, a verifier is invoked. If spurious counterexamples arise, we refine the abstraction by performing a further iteration of random simulation and machine learning. We present an experimental evaluation on processor designs. |
Year | Venue | Keywords |
|---|---|---|
2011 | Formal Methods in Computer-Aided Design | layered approach,conditional abstraction,automatic technique,abstraction refinement,background theory,abstract register transfer level,machine learning,term level,random simulation,simulation trace,term-level abstraction,data models,integrated circuit,formal logic,computer model,learning artificial intelligence,nickel,register transfer level,computational modeling,formal verification,first order logic,vectors |
Field | DocType | ISBN |
Data modeling,Programming language,Abstraction,Computer science,Theoretical computer science,Logic simulation,Abstraction inversion,Register-transfer level,Counterexample,Spurious relationship,Formal verification | Conference | 978-1-4673-0896-0 |
Citations | PageRank | References |
5 | 0.42 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bryan A. Brady | 1 | 31 | 2.16 |
| Randal E. Bryant | 2 | 9204 | 1194.64 |
| Sanjit A. Seshia | 3 | 2226 | 168.09 |