Name
Abstract | ||
|---|---|---|
In this paper, we describe the modeling and verification of out-of-order microprocessors with unbounded resources using an expressive, yet efficiently decidable, quantifier-free fragment of first order logic. This logic includes uninterpreted functions, equality, ordering, constrained lambda expressions, and counter arithmetic. UCLID is a tool for specifying and verifying systems expressed in this logic. The paper makes two main contributions. First, we show that the logic is expressive enough to model components found in most modern microprocessors, independent of their actual sizes. Second, we demonstrate UCLID's verification capabilities, ranging from full automation for bounded property checking to a high degree of automation in proving restricted classes of invariants. These techniques, coupled with a counterexample generation facility, are useful in establishing correctness of processor designs. We demonstrate UCLID's methods using a case study of a synthetic model of an out-of-order processor where all the invariants were proved automatically. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-36126-X_9 | FMCAD |
Keywords | Field | DocType |
out-of-order microprocessors,model component,processor design,full automation,synthetic model,modern microprocessors,order logic,out-of-order processor,verification capability,actual size,first order logic,out of order | Programming language,Model checking,Computer science,Correctness,Program counter,Theoretical computer science,Decidability,Automation,Distributed computing,Uclid,Discrete mathematics,First-order logic,Formal verification | Conference |
Volume | ISSN | ISBN |
2517 | 0302-9743 | 3-540-00116-6 |
Citations | PageRank | References |
57 | 2.49 | 20 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shuvendu K. Lahiri | 1 | 1424 | 68.18 |
| Sanjit A. Seshia | 2 | 2226 | 168.09 |
| Randal E. Bryant | 3 | 9204 | 1194.64 |