The operational model’s honest edges, and how to build a verification flow around all three formalizations.
Known limitations: no self-modifying code (fetch is oracle-fed over fixed instruction memory — FENCE.I behavior unmodeled); no misaligned-atomicity-granule PMA (misaligned accesses always decompose to bytes); ISA coverage is the Sail RV64I+A fragment, not the full GC set; and the mixed-size RSW family (uA A.7) is the known axiomatic/operational discrepancy — resolve it by following the stricter operational verdict.
The three-model DV flow in one paragraph: run the public litmus suite against RTL under randomized perturbation; diff outcome sets against herd (fast, axiomatic, full-suite); when a diff needs a step-by-step explanation, reproduce it in rmem interactively to get a transition-level witness; when a model question arises (would rule X change anything?), pose it to Alloy for a bounded search. Anything your RTL exhibits that all models forbid is a bug of the weeks-of-debugging class — this flow finds it in simulation.
Hardware Designer Notes
Part I ends here: the complete unprivileged contract for a Linux-boot core, from encodings to the formal memory model. Part II picks up at machine mode — reset, traps, CSRs, and the privileged machinery that turns a hart into a bootable CPU.
Minimal Linux-boot hart MUST
- Cover the model gaps by other means: FENCE.I paths via directed self-modifying-code tests; misaligned-granule behavior via your PMA test plan; F/D/C interactions via the architectural compliance suite
MAY simplify / trap-and-emulate
- Contribute divergences upstream — the models are living artifacts and the memory-model task group tracks discrepancies
Check yourself — model limitations
1.Which of these does the operational model NOT cover?
2.Your RTL shows an outcome herd allows but rmem forbids (a mixed-size test). Ship it?