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

A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm Without a Reorder Buffer
 by Ravi Hosabettu, Mandayam Srivas & Ganesh Gopalakrishnan.

The Completion Functions Approach was proposed in [HSG98] as a systematic way to decompose 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. However, its applicability depends on the fact that the implementation "commits" the unfinished instructions in the pipeline in program order. In this paper, we extend the completion functions approach when this is not true and demonstrate it on an implementation of Tomasulo's algorithm without a reorder buffer. The approach leads to an elegant decomposition of the proof of the correctness criterion, does not involve the construction of an explicit intermediate abstraction, makes heavy use of an automatic case-analysis strategy based on decision procedures and rewriting, and addresses both safety and liveness issues.


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