[tux3]

The RISC-V privileged spec describes their paging implementation (under the Supervisor-level ISA), while the unprivileged spec has a chapter and two appendices describing their memory model (RVWMO), formal axiomatic and operational models included.

Finding the inevitable bugs in the formal model is left as an exercise to the reader (three bugs where the axiomatic/operational models disagree are already known).

If you want a more gentle introduction, the Computer Organization and Design book is pretty nice.

[signa11]

the book, I have gone through (yes, exercises too :o), fwiw) thanks for the risc-v reference.