diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-15 11:07:56 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-15 11:18:44 -0700 |
| commit | 39ed62d79e9f4ead6f52e755df9f9562e44696ac (patch) | |
| tree | 4b4ac003bdbf86f3b01d68667c47f464f93a87ae /model/riscv_vmem_sv48.sail | |
| parent | 8b39adca2fafad9037f21202782ac29c776b7526 (diff) | |
| download | sail-riscv-39ed62d79e9f4ead6f52e755df9f9562e44696ac.zip sail-riscv-39ed62d79e9f4ead6f52e755df9f9562e44696ac.tar.gz sail-riscv-39ed62d79e9f4ead6f52e755df9f9562e44696ac.tar.bz2 | |
Allow extensions to types of memory access, and factor out PTE and PTW definitions.
Diffstat (limited to 'model/riscv_vmem_sv48.sail')
| -rw-r--r-- | model/riscv_vmem_sv48.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index a898ac7..664807c 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -1,6 +1,6 @@ /* Sv48 address translation for RV64. */ -val walk48 : (vaddr48, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape} +val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape} function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { let va = Mk_SV48_Vaddr(vaddr); let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), @@ -105,7 +105,7 @@ function flush_TLB48(asid, addr) = /* address translation */ -val translate48 : (asid64, paddr64, vaddr48, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem} +val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem} function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { PTW_Failure(f) => TR_Failure(f), |