Each transition is one atomic step of one instruction instance — it may read/change its hart’s state and shared memory, never other harts’. A transition has a precondition and a post-state; execution interleaves transitions from many instructions freely. The catalog:
| Precondition / effect | |
|---|---|
| Fetch instruction | Extends the instruction tree at a fetch address (multiple successors possible after branches). No memory operations — opcodes come from the oracle. Eager-safe unless taken infinitely. |
| Register read / write · Internal step | Dataflow: reads take the most recent po-predecessor write of the register slice; internal steps run pure pseudocode. Always eager-safe. |
| Initiate load footprint → Satisfy (forward) / Satisfy (memory) → Complete loads | Loads resolve slice-wise, from unpropagated program-order-earlier stores (forwarding) and/or memory |
| Initiate store footprint → Instantiate values → Commit → Propagate → Complete | Footprint, then values (forwarding to later loads becomes possible!), then the no-return commit, then per-operation propagation to shared memory |
| Early sc fail · Paired sc · Commit+propagate sc · Late sc fail | SC may fail spontaneously early or late; the success path commits AND propagates in one atomic step, enabled only if the LR’s source stores were not overwritten |
| Satisfy+commit+propagate AMO | The whole AMO — load satisfy, arithmetic, store propagate — as ONE indivisible transition. No forwarding in or out (PPO rule 3, operationally). |
| Commit fence | Fences are single commit events whose preconditions encode the pred/succ ordering bits. |
| Finish instruction | Pseudocode done, restarts impossible, memory effects final; untaken branch subtrees are discarded here. |
A plain load’s typical life: register read → initiate → satisfy (forward and/or memory, per slice) → complete → register write → finish, with internal steps anywhere and the next fetch always available. Transitions marked eager (○) can fire as soon as enabled without excluding behaviors; the marked few (∙) — the ordering-sensitive ones — cannot.
Hardware Designer Notes
This page closes Part I. The transition catalog doubles as a review checklist for an OoO LSU design: every early action your hardware takes must correspond to an eager-safe transition or carry a repair path back to a legal state. Next stop: Volume II — machine mode, where the Linux-boot road continues.
Minimal Linux-boot hart MUST
- Nothing normative — but your RTL’s observable outcomes must be a subset of what these transitions generate
MAY simplify / trap-and-emulate
- Map your pipeline events onto the transitions (commit ≈ commit, store-queue drain ≈ propagate, replay ≈ restart) and check each hardware event’s precondition implies the model’s
- Use the SC commit+propagate precondition verbatim as the reservation-checker assertion in DV
Check yourself — transitions
1.When may the model's 'Commit and propagate store operation of an sc' transition fire?
2.Until which transition can a load instruction be restarted?
3.A store's operations may forward to later loads starting at which point?