diff options
Diffstat (limited to 'model/riscv_vmem_sv32.sail')
| -rw-r--r-- | model/riscv_vmem_sv32.sail | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index e535915..1a27072 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -6,7 +6,7 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] -val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rreg, escape} +val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape} function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), @@ -37,13 +37,13 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { @@ -115,7 +115,7 @@ function flush_TLB32(asid, addr) = /* address translation */ -val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem} +val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt} function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match lookup_TLB32(asid, vAddr) { Some(idx, ent) => { |