diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-13 18:26:02 -0800 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-13 18:26:02 -0800 |
commit | 3c7e647a0136b5a7b6fc0eb9b47c38867ec3e9f0 (patch) | |
tree | 64e27f8b62b6142eee82168eb6e5f11d72c3cb4e /model/riscv_vmem_rv64.sail | |
parent | a81a59cf7605113f3b3d353bec460fa83622c65c (diff) | |
download | sail-riscv-3c7e647a0136b5a7b6fc0eb9b47c38867ec3e9f0.zip sail-riscv-3c7e647a0136b5a7b6fc0eb9b47c38867ec3e9f0.tar.gz sail-riscv-3c7e647a0136b5a7b6fc0eb9b47c38867ec3e9f0.tar.bz2 |
Add Sv32 and Sv48 by essentially copying Sv39.
Being first-order prevents straight-forward abstraction over the PTE operations, but perhaps there is another way to generalize and unify.
Diffstat (limited to 'model/riscv_vmem_rv64.sail')
-rw-r--r-- | model/riscv_vmem_rv64.sail | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail new file mode 100644 index 0000000..c7d9048 --- /dev/null +++ b/model/riscv_vmem_rv64.sail @@ -0,0 +1,63 @@ +/* RV64 Supervisor-mode address translation and page-table walks. */ + +/* Define the architectural satp and its legalizer. */ + +register satp : xlenbits + +function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = + legalize_satp64(a, o, v) + +/* Compute the address translation mode. */ + +val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +function translationMode(priv) = { + if priv == Machine then Sbare + else { + let arch = architecture(get_mstatus_SXL(mstatus)); + match arch { + Some(RV64) => { + let mbits : satp_mode = Mk_Satp64(satp).Mode(); + match satp64Mode_of_bits(RV64, mbits) { + Some(m) => m, + None() => internal_error("invalid RV64 translation mode in satp") + } + }, + Some(RV32) => { + let s = Mk_Satp32(satp[31..0]); + if s.Mode() == false then Sbare else Sv32 + }, + _ => internal_error("unsupported address translation arch") + } + } +} + +/* Top-level address translation dispatcher */ + +val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wreg} +function translateAddr(vAddr, ac, rt) = { + let effPriv : Privilege = match rt { + Instruction => cur_privilege, + Data => if mstatus.MPRV() == true + then privLevel_of_bits(mstatus.MPP()) + else cur_privilege + }; + let mxr : bool = mstatus.MXR() == true; + let do_sum : bool = mstatus.SUM() == true; + let mode : SATPMode = translationMode(effPriv); + + let asid = curAsid64(satp); + let ptb = curPTB64(satp); + + match mode { + Sbare => TR_Address(vAddr), + SV39 => match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) { + TR_Address(pa) => TR_Address(EXTZ(pa)), + TR_Failure(f) => TR_Failure(translationException(ac, f)) + }, + SV48 => match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) { + TR_Address(pa) => TR_Address(EXTZ(pa)), + TR_Failure(f) => TR_Failure(translationException(ac, f)) + }, + _ => internal_error("unsupported address translation scheme") + } +} |