Name
Title | ||
|---|---|---|
Formal design verification for correctness of pipelined microprocessors with out-of-order instruction execution |
Abstract | ||
|---|---|---|
In this paper, we propose a verification method for pipelined microprocessors with out-of-order execution. We define a class of pipelined microprocessors with out-of-order execution and give a sufficient condition that guarantees the correctness of implementation. Each microprocessor in this class has a pipeline stg1,…,stgn such that the stages stgc ,…,stgn are so-called “in-order pipeline” and changes the execution order of instructions within the stages of stg1,…,stgc-1. Using our method, we carried out the correctness proof of a practical 6-stage pipelined microprocessor that has a so-called scoreboard. We used a verifier having a decision procedure for Presburger sentences. The total CPU time spent in the proof was about 8 hours |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1109/ASPDAC.1999.759989 | ASP-DAC |
Keywords | Field | DocType |
design constraint,scoreboard,in-order pipeline,microprocessor chips,abstraction level,formal design verification,reduced instruction set computing,data hazards,6-stage pipelined microprocessor,decision procedure,presburger sentences,pipelined microprocessors,hazards and race conditions,out-of-order instruction execution,high level synthesis,correctness of implementation,risc,formal verification,pipeline processing,hazards,pipelines,out of order,informatics,out of order execution,dynamic scheduling | Formal design,Computer science,CPU time,Correctness,High-level synthesis,Parallel computing,Microprocessor,Real-time computing,Reduced instruction set computing,Out-of-order execution,Formal verification | Conference |
ISBN | Citations | PageRank |
0-7803-5012-X | 0 | 0.34 |
References | Authors | |
4 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Takashi Takenaka | 1 | 37 | 7.74 |
| Junji Kitamichi | 2 | 64 | 10.32 |
| Teruo Higashino | 3 | 1086 | 119.60 |
| kenichi taniguchi | 4 | 256 | 35.56 |