diff options
Diffstat (limited to 'model/riscv_vmem_rv32.sail')
| -rw-r--r-- | model/riscv_vmem_rv32.sail | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index ba29332..3478be4 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -79,7 +79,7 @@ function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits /* Compute the address translation mode. */ -val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +val translationMode : (Privilege) -> SATPMode function translationMode(priv) = { if priv == Machine then Sbare else { @@ -96,7 +96,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { let mxr : bool = mstatus.MXR() == 0b1; let do_sum : bool = mstatus.SUM() == 0b1; @@ -118,11 +118,11 @@ function translateAddr_priv(vAddr, ac, effPriv) = { } } -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) function translateAddr(vAddr, ac) = translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) -val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg} +val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit function flush_TLB(asid_xlen, addr_xlen) -> unit = { let asid : option(asid32) = match (asid_xlen) { |