next up previous contents
Next: Tomasulo's algorithm Up: Refinement verification Previous: What about outputs?   Contents

An out-of-order instruction processor

The above may have seemed like a great deal of effort to verify such a simple design. However, we will find that the proof becomes only incrementally more complex when we move to a much more complex implementation - an instruction processor using Tomasulo's algorithm.