diff options
Diffstat (limited to 'mips/mips_prelude.sail')
| -rw-r--r-- | mips/mips_prelude.sail | 94 |
1 files changed, 0 insertions, 94 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index b282764d..80350af1 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -499,100 +499,6 @@ function unit incrementCP0Count() = { SignalException(Int); } -function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = - let entryValid = entry.valid in - let entryR = entry.r in - let entryMask = entry.pagemask in - let entryVPN = entry.vpn2 in - let entryASID = entry.asid in - let entryG = entry.g in - (entryValid & - (r == entryR) & - ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) & - ((asid == (entryASID)) | (entryG))) - -function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = - let r = (VAddr[63..62]) in - let vpn2 = (VAddr[39..13]) in - let asid = TLBEntryHi.ASID in { - foreach (idx from 0 to 63) { - if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then - return (Some ((TLBIndexT) idx)) - }; - None - } - -function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = { - let idx = tlbSearch(vAddr) in - switch(idx) { - case (Some(idx)) -> - let entry = (TLBEntries[idx]) in - let entryMask = entry.pagemask in - - let evenOddBit = switch(entryMask) { - case 0x0000 -> 12 - case 0x0003 -> 14 - case 0x000f -> 16 - case 0x003f -> 18 - case 0x00ff -> 20 - case 0x03ff -> 22 - case 0x0fff -> 24 - case 0x3fff -> 26 - case 0xffff -> 28 - case _ -> undefined - } in - let isOdd = (vAddr[evenOddBit]) in - let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then - (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1) - else - (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in - if (~(v)) then - (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr)) - else if ((accessType == StoreData) & ~(d)) then - (SignalExceptionTLB(TLBMod, vAddr)) - else - (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), - if (accessType == StoreData) then caps else capl) - case None -> (SignalExceptionTLB( - if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)) - } -} - -function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = - { - let currentAccessLevel = getAccessLevel() in - let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in - let (requiredLevel, addr) = switch(vAddr[63..62]) { - case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *) - case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *) - case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *) - case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *) - case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *) - case (_, _) -> (Kernel, None) (* xkseg mapped *) - } - case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *) - case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *) - case 0b00 -> (User, None) (* xuseg - user mapped *) - } in - if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - let (pa, c) = switch(addr) { - case (Some(a)) -> (a, false) - case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - TLBTranslate2(vAddr, accessType) - } - in if (unsigned(pa) > MAX_PA) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - (pa, c) - } - -function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = - let (addr, c) = TLBTranslateC(vAddr, accessType) in addr - typedef regno = bit[5] (* a register number *) typedef imm16 = bit[16] (* 16-bit immediate *) (* a commonly used instruction format with three register operands *) |