11. Full Pipeline🔗

The pipelined-fetch cell overlaps only fetch; the operand-pipeline chapter proves when the memory reads may also run a cycle early. This chapter composes the two into a single cell that overlaps fetch and operands, so straight-line independent code commits one instruction per cycle, and proves the composition still commits the sequential trace — with a one-cycle bubble only for the one real data hazard (a dependent operand read) or control hazard (a taken branch).

The overlap is a read stage running one instruction ahead of execute. While the execute stage commits the latched instruction fir with its latched operands, the read stage reads the next instruction's operands from the current architectural state — a cycle early, before the committing instruction writes back. The interlock (indepB) decides whether that early read is safe: it is, exactly when the committing instruction is independent of the one being read, and then the cell commits again next cycle; otherwise the early read is dropped and the cell bubbles for one cycle to re-read from the committed state.

The state pairs the architectural state and instruction memory with a busy bit, a fetch latch (validity, index, instruction), and an operand latch (validity plus the three latched memory operands). The operand-latch invariant OpInv is the load-bearing one: whenever the operands are valid, executing the latched instruction with them equals executing it directly — the latched operands are the right reads.

A committing cycle executes fir with its latched operands, prefetches the predicted fall-through instruction, and reads that instruction's operands early from the pre-commit state c.arch. The early read is marked valid only when the interlock reports the committing instruction independent of the prefetched one.

A bubble reads its operands from the committed state, so execLatched_eq makes its operand latch valid immediately — a bubble always satisfies OpInv.