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.

- Tomasulo's algorithm
- The abstract model
- Implementation
- Refinement maps
- Case splitting
- The proof
- Abstract counterexamples
- Multiple execution units
- Proving non-interference
- Adding a reorder buffer
- Proving liveness

2003-01-07