Loading...
Please wait, while we are loading the content...
Similar Documents
A Systematic Methodology for Verifying Superscalar Microprocessors
| Content Provider | Semantic Scholar |
|---|---|
| Author | Mandayam, K. Srivas Ravi, Hosabettu Ganesh, Gopalakrishnan |
| Copyright Year | 1999 |
| Abstract | We present a systematic approach to decompose and incrementally build the proof of correctness of pipelined microprocessors. The central idea is to construct the abstraction function by using completion functions, one per unfinished instruction, each of which specifies the effect (on the observables) of completing the instruction. In addition to avoiding the term size and case explosion problem that limits the pure flushing approach, our method helps localize errors, and also handles stages with interative loops. The technique is illustrated on pipelined and superscalar pipelined implementations of a subset of the DLX architecture. It has also been applied to a processor with out-of-order execution. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.odu.edu/~mln/ltrs-pdfs/NASA-99-cr208991.pdf |
| Alternate Webpage(s) | http://techreports.larc.nasa.gov/ltrs/PDF/1999/cr/NASA-99-cr208991.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
