diff options
| -rw-r--r-- | cheri/cheri_insts.sail | 8 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 20 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 3 |
3 files changed, 14 insertions, 17 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index cccb361a..a54b8526 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -554,7 +554,7 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = exit (SignalExceptionBadAddr(AdEL, vAddr64)) else { - pAddr := (TranslateOrExit(vAddr64, LoadData)); + pAddr := (TLBTranslate(vAddr64, LoadData)); widthBytes := wordWidthBytes(width); memResult := if (linked) then { @@ -609,7 +609,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = exit (SignalExceptionBadAddr(AdES, vAddr64)) else { - pAddr := (TranslateOrExit(vAddr64, StoreData)); + pAddr := (TLBTranslate(vAddr64, StoreData)); rs_val := rGPR(rs); if (conditional) then { @@ -670,7 +670,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = exit (SignalExceptionBadAddr(AdES, vAddr64)) else { - pAddr := (TranslateOrExit(vAddr64, if cs_val.tag then StoreData else StoreData)); (* XXX use StoreCap here. *) + pAddr := (TLBTranslate(vAddr64, if cs_val.tag then StoreData else StoreData)); (* XXX use StoreCap here. *) if (conditional) then { success := if (CP0LLBit[0]) then @@ -715,7 +715,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) = exit (SignalExceptionBadAddr(AdEL, vAddr64)) else { - pAddr := (TranslateOrExit(vAddr64, LoadData)); (* XXX use LoadCap here. *) + pAddr := (TLBTranslate(vAddr64, LoadData)); (* XXX use LoadCap here. *) let (tag, mem) = (if (linked) then { diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index 04bfc48d..722e3d00 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1033,7 +1033,7 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = if ~ (isAddressAligned(vAddr, width)) then exit (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *) else - let pAddr = (TranslateOrExit(vAddr, LoadData)) in + let pAddr = (TLBTranslate(vAddr, LoadData)) in { memResult := if (linked) then { @@ -1068,7 +1068,7 @@ function clause execute (Store(width, conditional, base, rt, offset)) = if ~ (isAddressAligned(vAddr, width)) then exit (SignalExceptionBadAddr(AdES, vAddr)) (* unaligned access *) else - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { if (conditional) then { @@ -1101,7 +1101,7 @@ function clause execute(LWL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); - let pAddr = (TranslateOrExit(vAddr, LoadData)) in + let pAddr = (TLBTranslate(vAddr, LoadData)) in { mem_val := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); @@ -1121,7 +1121,7 @@ function clause execute(LWR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); - let pAddr = (TranslateOrExit(vAddr, LoadData)) in + let pAddr = (TLBTranslate(vAddr, LoadData)) in { mem_val := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); @@ -1143,7 +1143,7 @@ function clause execute(SWL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { reg_val := rGPR(rt); switch (vAddr[1..0]) @@ -1163,7 +1163,7 @@ function clause execute(SWR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); - let (pAddr) = (TranslateOrExit(vAddr, StoreData)) in + let (pAddr) = (TLBTranslate(vAddr, StoreData)) in { wordAddr := pAddr[63..2] : 0b00; reg_val := rGPR(rt); @@ -1185,7 +1185,7 @@ function clause execute(LDL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { mem_val := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *) reg_val := rGPR(rt); @@ -1211,7 +1211,7 @@ function clause execute(LDR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { mem_val := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *) reg_val := rGPR(rt); @@ -1237,7 +1237,7 @@ function clause execute(SDL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { reg_val := rGPR(rt); switch (vAddr[2..0]) @@ -1263,7 +1263,7 @@ function clause execute(SDR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); - let pAddr = (TranslateOrExit(vAddr, StoreData)) in + let pAddr = (TLBTranslate(vAddr, StoreData)) in { reg_val := rGPR(rt); wordAddr := pAddr[63..3] : 0b000; diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index e27a49d7..c338adf1 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -229,9 +229,6 @@ function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = addr } -function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) = - TLBTranslate(vAddr, accessType) - typedef regno = bit[5] (* a register number *) typedef imm16 = bit[16] (* 16-bit immediate *) typedef regregreg = (regno, regno, regno) (* a commonly used instruction format with three register operands *) |