SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Decomposing the Proof of Correctness of Pipelined Microprocessors
 by Ravi Hosabettu, Mandayam Srivas & Ganesh Gopalakrishnan.

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 using completion functions) one per unfinished instruction) each of which specifies the effect (on the observables ) of completing the instruction. In addition to avoiding term-size and case explosion problem that limits the pure flush ing approach, our method helps localize errors) and also handles stages with iterative loops. The technique is illustrated on a pipelined and a superscalar pipelined implementations of a subset of the DLX architecture. It has also been applied to a processor with out-of-order execution.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2018 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy