Actions for A Systematic Methodology for Verifying Superscalar Microprocessors

Email RIS file
Bookmark
Report an Issue

A Systematic Methodology for Verifying Superscalar Microprocessors

Author
Srivas, Mandayam
Published
Feb. 1999.
Physical Description
1 electronic document
Additional Creators
Gopalakrishnan, Ganesh and Hosabettu, Ravi
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
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 interactive 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.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 19990018275.
NASA/CR-1999-208991.
NAS 1.26:208991.
Terms of Use and Reproduction
No Copyright.
View MARC record | catkey: 15643511