Name
Abstract | ||
|---|---|---|
We describe a framework for verifying a pipelined microprocessor whose implementation contains precise exceptions, external interrupts, and speculative execution. We present our correctness criterion which compares the state transitions of pipelined and non-pipelined machines in presence of external interrupts. To perform the verification, we created a table-based model of pipeline execution. This model records committed and in-flight instructions as performed by the microarchitecture. Given that certain requirements are met by this table-based model, we have mechanically verified our correctness criterion using the ACL2 theorem prover. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/BFb0028740 | CAV |
Keywords | Field | DocType |
precise exeptions,processor verification,speculative execution,theorem prover,state transition | Programming language,Computer science,Speculative execution,Correctness,Parallel computing,Automated theorem proving,Microprocessor,Algorithm,ACL2,Re-order buffer,Formal verification,Microarchitecture | Conference |
Volume | ISSN | ISBN |
1427 | 0302-9743 | 3-540-64608-6 |
Citations | PageRank | References |
58 | 3.91 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jun Sawada | 1 | 325 | 21.16 |
| Warren A. Hunt, Jr. | 2 | 520 | 59.18 |