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

Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach
 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. In this paper, we show that this "instruction-centric" view of the completion functions approach leads to an elegant decomposition of the proof for an out-of-order execution processor with a reorder buffer. The proof does not involve the construction of an explicit intermediate abstraction, makes heavy use of strategies based on decision procedures and rewriting, and addresses both safety and liveness issues with a clean separation between them.


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