summaryrefslogtreecommitdiff
path: root/mips
diff options
context:
space:
mode:
Diffstat (limited to 'mips')
-rw-r--r--mips/mips_insts.sail16
-rw-r--r--mips/mips_prelude.sail77
2 files changed, 55 insertions, 38 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index d4459fb1..5827369e 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1325,8 +1325,8 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
{
case (0b00000,0b000) -> (0x00000000 : [TLBProbe] : 0x0000000 : TLBIndex) (* 0, TLB Index *)
case (0b00001,0b000) -> EXTZ(TLBRandom) (* 1, TLB Random *)
- case (0b00010,0b000) -> EXTZ(TLBEntryLo0)(* 2, TLB EntryLo0 *)
- case (0b00011,0b000) -> EXTZ(TLBEntryLo1)(* 3, TLB EntryLo1 *)
+ case (0b00010,0b000) -> TLBEntryLo0 (* 2, TLB EntryLo0 *)
+ case (0b00011,0b000) -> TLBEntryLo1 (* 3, TLB EntryLo1 *)
case (0b00100,0b000) -> TLBContext (* 4, TLB Context *)
case (0b00101,0b000) -> EXTZ(TLBPageMask : 0x000) (* 5, TLB PageMask *)
case (0b00110,0b000) -> EXTZ(TLBWired) (* 6, TLB Wired *)
@@ -1400,8 +1400,8 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
{
case (0b00000,0b000) -> TLBIndex := mask(reg_val) (* NB no write to TLBProbe *)
case (0b00001,0b000) -> () (* TLBRandom is read only *)
- case (0b00010,0b000) -> TLBEntryLo0 := mask(reg_val)
- case (0b00011,0b000) -> TLBEntryLo1 := mask(reg_val)
+ case (0b00010,0b000) -> TLBEntryLo0 := reg_val
+ case (0b00011,0b000) -> TLBEntryLo1 := reg_val
case (0b00100,0b000) -> (TLBContext.PTEBase) := (reg_val[63..23])
case (0b00100,0b010) -> CP0UserLocal := reg_val
case (0b00101,0b000) -> TLBPageMask := (reg_val[28..13])
@@ -1464,10 +1464,14 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
((TLBEntries[idx]).asid ) := TLBEntryHi.ASID;
((TLBEntries[idx]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
((TLBEntries[idx]).valid ) := bitone;
+ ((TLBEntries[idx]).caps0 ) := TLBEntryLo0.CapS;
+ ((TLBEntries[idx]).capl0 ) := TLBEntryLo0.CapL;
((TLBEntries[idx]).pfn0 ) := TLBEntryLo0.PFN;
((TLBEntries[idx]).c0 ) := TLBEntryLo0.C;
((TLBEntries[idx]).d0 ) := TLBEntryLo0.D;
((TLBEntries[idx]).v0 ) := TLBEntryLo0.V;
+ ((TLBEntries[idx]).caps1 ) := TLBEntryLo1.CapS;
+ ((TLBEntries[idx]).capl1 ) := TLBEntryLo1.CapL;
((TLBEntries[idx]).pfn1 ) := TLBEntryLo1.PFN;
((TLBEntries[idx]).c1 ) := TLBEntryLo1.C;
((TLBEntries[idx]).d1 ) := TLBEntryLo1.D;
@@ -1497,11 +1501,15 @@ function clause execute (TLBR) = {
TLBEntryHi.R := entry.r;
TLBEntryHi.VPN2 := entry.vpn2;
TLBEntryHi.ASID := entry.asid;
+ TLBEntryLo0.CapS:= entry.caps0;
+ TLBEntryLo0.CapL:= entry.capl0;
TLBEntryLo0.PFN := entry.pfn0;
TLBEntryLo0.C := entry.c0;
TLBEntryLo0.D := entry.d0;
TLBEntryLo0.V := entry.v0;
TLBEntryLo0.G := entry.g;
+ TLBEntryLo1.CapS:= entry.caps1;
+ TLBEntryLo1.CapL:= entry.capl1;
TLBEntryLo1.PFN := entry.pfn1;
TLBEntryLo1.C := entry.c1;
TLBEntryLo1.D := entry.d1;
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index e1ae31fb..04574115 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -24,7 +24,9 @@ typedef CauseReg = register bits [ 31 : 0 ] {
(*1 .. 0 : Z4;*)
}
-typedef TLBEntryLoReg = register bits [29 : 0] {
+typedef TLBEntryLoReg = register bits [63 : 0] {
+ 63 : CapS;
+ 62 : CapL;
29 .. 6 : PFN;
5 .. 3 : C;
2 : D;
@@ -57,21 +59,25 @@ let (TLBIndexT) TLBIndexMax = 0b111
let MAX_VA = unsigned(0xffffffffff)
let MAX_PA = unsigned(0xfffffffff)
-typedef TLBEntry = register bits [112 : 0] {
- 112 .. 97: pagemask; (* 16 bits *)
- 96 .. 95: r; (* 2 bits *)
- 94 .. 68: vpn2; (* 27 bits *)
- 67 .. 60: asid; (* 8 bits *)
- 59 : g;
- 58 : valid;
- 57 .. 34: pfn0; (* 24 bits *)
- 33 .. 31: c0; (* 3 bits *)
- 30 : d0;
- 29 : v0;
- 28 .. 5 : pfn1;
- 4 .. 2 : c1;
- 1 : d1;
- 0 : v1;
+typedef TLBEntry = register bits [116 : 0] {
+ 116 .. 101: pagemask;
+ 100 .. 99 : r ;
+ 98 .. 72 : vpn2 ;
+ 71 .. 64 : asid ;
+ 63 : g ;
+ 62 : valid ;
+ 61 : caps1 ;
+ 60 : capl1 ;
+ 59 .. 36 : pfn1 ;
+ 35 .. 33 : c1 ;
+ 32 : d1 ;
+ 31 : v1 ;
+ 30 : caps0 ;
+ 29 : capl0 ;
+ 28 .. 5 : pfn0 ;
+ 4 .. 2 : c0 ;
+ 1 : d0 ;
+ 0 : v0 ;
}
register (bit[1]) TLBProbe
@@ -338,13 +344,13 @@ function unit incrementCP0Count() = {
}
function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
- let entryVal = (bit[113]) entry in
- let entryValid = (entryVal[58]) in
- let entryR = (entryVal[96..95]) in
- let entryMask = (entryVal[112..97]) in
- let entryVPN = (entryVal[94..68]) in
- let entryASID = (entryVal[67..60]) in
- let entryG = (entryVal[59]) in
+ let entryVal = (bit[117]) entry in
+ let entryValid = (entryVal[62]) in
+ let entryR = (entryVal[100..99]) in
+ let entryMask = (entryVal[116..101]) in
+ let entryVPN = (entryVal[98..72]) in
+ let entryASID = (entryVal[71..64]) in
+ let entryG = (entryVal[63]) in
((entryValid) &
(r == (entryR)) &
((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
@@ -373,12 +379,12 @@ function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
else
None
-function (bit[64]) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
+function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
let idx = tlbSearch(vAddr) in
switch(idx) {
case (Some(idx)) ->
- let entry = ((bit[113])(TLBEntries[idx])) in
- let entryMask = (entry[112..97]) in
+ let entry = ((bit[117])(TLBEntries[idx])) in
+ let entryMask = (entry[116..101]) in
let evenOddBit = switch(entryMask) {
case 0x0000 -> 12
@@ -393,21 +399,21 @@ function (bit[64]) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) =
case _ -> undefined
} in
let isOdd = (vAddr[evenOddBit]) in
- let (pfn, v, c, d) = if (isOdd) then
- (entry[28..5], entry[0], entry[4..2], entry[1])
+ let (caps, capl, pfn, d, v) = if (isOdd) then
+ (entry[61], entry[60], entry[59..36], entry[32], entry[31])
else
- (entry[57..34], entry[29], entry[33..31], entry[30]) in
+ (entry[30], entry[29], entry[28..5], entry[1], entry[0]) in
if (~(v)) then
exit (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
else if ((accessType == StoreData) & ~(d)) then
exit (SignalExceptionTLB(TLBMod, vAddr))
else
- EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+ (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), if (accessType == StoreData) then caps else capl)
case None -> exit (SignalExceptionTLB(if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
}
}
-function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
+function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) =
{
let currentAccessLevel = getAccessLevel() in
let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
@@ -426,8 +432,8 @@ function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
- let pa = switch(addr) {
- case (Some(a)) -> a
+ let (pa, c) = switch(addr) {
+ case (Some(a)) -> (a, false)
case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
@@ -436,9 +442,12 @@ function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
in if (unsigned(pa) > MAX_PA) then
exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
- pa
+ (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 *)
typedef regregreg = (regno, regno, regno) (* a commonly used instruction format with three register operands *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 20:13:18 +0000