aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorThomas Bauereiss <tb592@cl.cam.ac.uk>2019-11-25 17:56:10 +0000
committerThomas Bauereiss <tb592@cl.cam.ac.uk>2019-11-25 17:56:10 +0000
commit1a653fc6207b8cb20204af6b2ccabab48a020945 (patch)
treeace99ff81dfb2fd7acd7bf056a197de4605f34c5 /model
parent0e42c867fba498746405d2b878a12fd4d143c5d8 (diff)
downloadsail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.zip
sail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.tar.gz
sail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.tar.bz2
Fix RV32 Lem build
Diffstat (limited to 'model')
-rw-r--r--model/riscv_vmem_rv32.sail2
-rw-r--r--model/riscv_vmem_sv32.sail4
2 files changed, 3 insertions, 3 deletions
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index 4ff7891..bea786c 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -26,7 +26,7 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function translateAddr(vAddr, ac) = {
let effPriv : Privilege = match ac {
Execute() => cur_privilege,
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index e535915..bf43f6f 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]),
@@ -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) => {