summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mips/mips_insts.sail121
-rw-r--r--mips/mips_prelude.sail193
-rw-r--r--src/lem_interp/run_with_elf.ml29
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml29
4 files changed, 349 insertions, 23 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index a265bd13..063472ca 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1323,18 +1323,18 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
checkCP0Access();
let (bit[64]) result = switch (rd, sel)
{
- case (0b00000,0b000) -> 0 (* 0, TLB Index *)
- case (0b00001,0b000) -> 0 (* 1, TLB Random *)
- case (0b00010,0b000) -> 0 (* 2, TLB EntryLo0 *)
- case (0b00011,0b000) -> 0 (* 3, TLB EntryLo1 *)
- case (0b00100,0b000) -> 0 (* 4, TLB Context *)
- case (0b00101,0b000) -> 0 (* 5, TLB PageMask *)
- case (0b00110,0b000) -> 0 (* 6, TLB Wired *)
- case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 6, HWREna *)
+ 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 (0b00100,0b000) -> TLBContext (* 4, TLB Context *)
+ case (0b00101,0b000) -> EXTZ(TLBPageMask : 0x000) (* 5, TLB PageMask *)
+ case (0b00110,0b000) -> EXTZ(TLBWired) (* 6, TLB Wired *)
+ case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 7, HWREna *)
case (0b01000,0b000) -> CP0BadVAddr (* 8, BadVAddr reg *)
case (0b01000,0b001) -> 0 (* 8, BadInstr reg XXX TODO *)
case (0b01001,0b000) -> EXTZ(CP0Count) (* 9, Count reg *)
- case (0b01010,0b000) -> 0 (* 10, TLB EntryHi *)
+ case (0b01010,0b000) -> TLBEntryHi (* 10, TLB EntryHi *)
case (0b01011,0b000) -> EXTZ(CP0Compare) (* 11, Compare reg *)
case (0b01100,0b000) -> EXTZ(CP0Status) (* 12, Status reg *)
case (0b01101,0b000) -> EXTZ(CP0Cause) (* 13, Cause reg *)
@@ -1377,10 +1377,11 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
: 0b0000 (* SL L2 lines *)
: 0b0000) (* SA L2 assoc. *)
case (0b10000,0b011) -> 0x0000000000002000 (* 16, sel 3: Config3 zero except for bit 13 == ulri *)
+ case (0b10000,0b101) -> 0x0000000000000000 (* 16, sel 5: Config5 beri specific -- no extended TLB *)
case (0b10001,0b000) -> CP0LLAddr (* 17, sel 0: LLAddr *)
case (0b10010,0b000) -> 0 (* 18, WatchLo *)
case (0b10011,0b000) -> 0 (* 19, WatchHi *)
- case (0b10100,0b000) -> 0 (* 20, XContext *)
+ case (0b10100,0b000) -> TLBXContext (* 20, XContext *)
case (0b11110,0b000) -> CP0ErrorEPC (* 30, ErrorEPC *)
case _ -> {exit (SignalException(ResI)); 0}
} in
@@ -1397,9 +1398,25 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
let reg_val = (rGPR(rt)) in
switch (rd, sel)
{
+ 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 (0b00100,0b000) -> (TLBContext.PTEBase) := (reg_val[63..23])
case (0b00100,0b010) -> CP0UserLocal := reg_val
+ case (0b00101,0b000) -> TLBPageMask := (reg_val[28..13])
+ case (0b00110,0b000) -> {
+ TLBWired := mask(reg_val);
+ TLBRandom := TLBIndexMax;
+ }
case (0b00111,0b000) -> CP0HWREna := (reg_val[31..29] : 0b0000000000000000000000000 : reg_val[3..0])
+ case (0b01000,0b000) -> () (* BadVAddr read only *)
case (0b01001,0b000) -> CP0Count := reg_val[31..0]
+ case (0b01010,0b000) -> {
+ (TLBEntryHi.R) := (reg_val[63..62]);
+ (TLBEntryHi.VPN2) := (reg_val[39..13]);
+ (TLBEntryHi.ASID) := (reg_val[7..0]);
+ }
case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *)
CP0Compare := reg_val[31..0];
(CP0Cause[15]) := bitzero;
@@ -1421,11 +1438,95 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
(CP0Cause.IP)[9..8] := reg_val[9..8];
}
case (0b01110,0b000) -> CP0EPC := reg_val (* 14, EPC *)
+ case (0b10100,0b000) -> (TLBXContext.PTEBase) := (reg_val[63..33])
case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *)
case _ -> exit (SignalException(ResI))
}
}
+function unit TLBWriteEntry((TLBIndexT) idx) = {
+ pagemask := ((bit[16]) TLBPageMask);
+ switch(pagemask) {
+ case 0x0000 -> ()
+ case 0x0003 -> ()
+ case 0x000f -> ()
+ case 0x003f -> ()
+ case 0x00ff -> ()
+ case 0x03ff -> ()
+ case 0x0fff -> ()
+ case 0x3fff -> ()
+ case 0xffff -> ()
+ case _ -> exit (SignalException(MCheck))
+ };
+ ((TLBEntries[idx]).pagemask) := pagemask;
+ ((TLBEntries[idx]).r ) := TLBEntryHi.R;
+ ((TLBEntries[idx]).vpn2 ) := TLBEntryHi.VPN2;
+ ((TLBEntries[idx]).asid ) := TLBEntryHi.ASID;
+ ((TLBEntries[idx]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
+ ((TLBEntries[idx]).valid ) := bitone;
+ ((TLBEntries[idx]).pfn0 ) := TLBEntryLo0.PFN;
+ ((TLBEntries[idx]).c0 ) := TLBEntryLo0.C;
+ ((TLBEntries[idx]).d0 ) := TLBEntryLo0.D;
+ ((TLBEntries[idx]).v0 ) := TLBEntryLo0.V;
+ ((TLBEntries[idx]).pfn1 ) := TLBEntryLo1.PFN;
+ ((TLBEntries[idx]).c1 ) := TLBEntryLo1.C;
+ ((TLBEntries[idx]).d1 ) := TLBEntryLo1.D;
+ ((TLBEntries[idx]).v1 ) := TLBEntryLo1.V;
+}
+
+union ast member TLBWI
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some(TLBWI)
+function clause execute (TLBWI) = {
+ checkCP0Access();
+ TLBWriteEntry(TLBIndex);
+}
+
+union ast member TLBWR
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some(TLBWR)
+function clause execute (TLBWR) = {
+ checkCP0Access();
+ TLBWriteEntry(TLBRandom);
+}
+
+union ast member TLBR
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some(TLBR)
+function clause execute (TLBR) = {
+ checkCP0Access();
+ let entry = TLBEntries[TLBIndex] in {
+ TLBPageMask := entry.pagemask;
+ TLBEntryHi.R := entry.r;
+ TLBEntryHi.VPN2 := entry.vpn2;
+ TLBEntryHi.ASID := entry.asid;
+ TLBEntryLo0.PFN := entry.pfn0;
+ TLBEntryLo0.C := entry.c0;
+ TLBEntryLo0.D := entry.d0;
+ TLBEntryLo0.V := entry.v0;
+ TLBEntryLo0.G := entry.g;
+ TLBEntryLo1.PFN := entry.pfn1;
+ TLBEntryLo1.C := entry.c1;
+ TLBEntryLo1.D := entry.d1;
+ TLBEntryLo1.V := entry.v1;
+ TLBEntryLo1.G := entry.g;
+ }
+}
+
+union ast member TLBP
+function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some(TLBP)
+function clause execute ((TLBP)) = {
+ checkCP0Access();
+ let result = tlbSearch(TLBEntryHi) in
+ switch(result) {
+ case (Some(idx)) -> {
+ TLBProbe := [bitzero];
+ TLBIndex := idx;
+ }
+ case None -> {
+ TLBProbe := [bitone];
+ TLBIndex := 0;
+ }
+ }
+}
+
union ast member (regno, regno) RDHWR
function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = Some(RDHWR(rt, rd))
function clause execute (RDHWR(rt, rd)) = {
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index f01d6f4e..6105deb8 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -23,6 +23,85 @@ typedef CauseReg = register bits [ 31 : 0 ] {
6 .. 2 : ExcCode; (* code of last exception *)
(*1 .. 0 : Z4;*)
}
+
+typedef TLBEntryLoReg = register bits [29 : 0] {
+ 29 .. 6 : PFN;
+ 5 .. 3 : C;
+ 2 : D;
+ 1 : V;
+ 0 : G;
+}
+
+typedef TLBEntryHiReg = register bits [63 : 0] {
+ 63 .. 62 : R;
+ 39 .. 13 : VPN2;
+ 7 .. 0 : ASID;
+}
+
+typedef ContextReg = register bits [63 : 0] {
+ 63 .. 23 : PTEBase;
+ 22 .. 4 : BadVPN2;
+ (*3 .. 0 : ZR;*)
+}
+
+typedef XContextReg = register bits [63 : 0] {
+ 63 .. 33: PTEBase;
+ 32 .. 31: R;
+ 30 .. 4: BadVPN2;
+}
+
+let ([:8:]) TLBNumEntries = 8
+typedef TLBIndexT = (bit[3])
+let (TLBIndexT) TLBIndexMax = 0b111
+
+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;
+}
+
+register (bit[1]) TLBProbe
+register (bit[3]) TLBIndex
+register (bit[3]) TLBRandom
+register (TLBEntryLoReg) TLBEntryLo0
+register (TLBEntryLoReg) TLBEntryLo1
+register (ContextReg) TLBContext
+register (bit[16]) TLBPageMask
+register (bit[3]) TLBWired
+register (TLBEntryHiReg) TLBEntryHi
+register (XContextReg) TLBXContext
+
+register (TLBEntry) TLBEntry00
+register (TLBEntry) TLBEntry01
+register (TLBEntry) TLBEntry02
+register (TLBEntry) TLBEntry03
+register (TLBEntry) TLBEntry04
+register (TLBEntry) TLBEntry05
+register (TLBEntry) TLBEntry06
+register (TLBEntry) TLBEntry07
+
+let (vector <0, 8, inc, (TLBEntry)>) TLBEntries = [
+TLBEntry00,
+TLBEntry01,
+TLBEntry02,
+TLBEntry03,
+TLBEntry04,
+TLBEntry05,
+TLBEntry06,
+TLBEntry07
+]
+
register (bit[32]) CP0Compare
register (CauseReg) CP0Cause
register (bit[64]) CP0EPC
@@ -126,8 +205,8 @@ val extern unit -> unit effect { barr } MEM_sync
typedef Exception = enumerate
{
- Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
- XTLBRefillL; XTLBRefillS
+ Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
+ XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck
}
(* Return the ISA defined code for an exception condition *)
@@ -135,7 +214,7 @@ function (bit[5]) ExceptionCode ((Exception) ex) =
switch (ex)
{
case Int -> mask(0x00) (* Interrupt *)
- case Mod -> mask(0x01) (* TLB modification exception *)
+ case TLBMod -> mask(0x01) (* TLB modification exception *)
case TLBL -> mask(0x02) (* TLB exception (load or fetch) *)
case TLBS -> mask(0x03) (* TLB exception (store) *)
case AdEL -> mask(0x04) (* Address error (load or fetch) *)
@@ -150,6 +229,9 @@ function (bit[5]) ExceptionCode ((Exception) ex) =
case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *)
case XTLBRefillL -> mask(0x02)
case XTLBRefillS -> mask(0x03)
+ case XTLBInvL -> mask(0x02)
+ case XTLBInvS -> mask(0x03)
+ case MCheck -> mask(0x18)
}
@@ -198,6 +280,16 @@ function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
SignalException(ex);
}
+function unit SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = {
+ CP0BadVAddr := badAddr;
+ (TLBContext.BadVPN2) := (badAddr[31..13]);
+ (TLBXContext.BadVPN2):= (badAddr[39..13]);
+ (TLBXContext.R) := (badAddr[63..62]);
+ (TLBEntryHi.R) := (badAddr[63..62]);
+ (TLBEntryHi.VPN2) := (badAddr[39..13]);
+ SignalException(ex);
+}
+
typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
typedef AccessLevel = enumerate {User; Supervisor; Kernel}
@@ -223,6 +315,9 @@ function unit checkCP0Access () =
}
function unit incrementCP0Count() = {
+ TLBRandom := (if (unsigned(TLBRandom) == unsigned(TLBWired))
+ then (TLBIndexMax) else (TLBRandom - 1));
+
CP0Count := (CP0Count + 1);
if (unsigned(CP0Count) == unsigned(CP0Compare)) then {
(CP0Cause[15]) := bitone;
@@ -239,26 +334,98 @@ function unit incrementCP0Count() = {
exit (SignalException(Int));
}
+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
+ ((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
+ if (tlbEntryMatch(r, vpn2, asid, TLBEntry00)) then
+ Some(0b000)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry01)) then
+ Some(0b001)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry02)) then
+ Some(0b010)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry03)) then
+ Some(0b011)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry04)) then
+ Some(0b100)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry05)) then
+ Some(0b101)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry06)) then
+ Some(0b110)
+ else if (tlbEntryMatch(r, vpn2, asid, TLBEntry07)) then
+ Some(0b111)
+ else
+ None
+
+function (bit[64]) 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 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 (pfn, v, c, d) = if (isOdd) then
+ (entry[28..5], entry[0], entry[4..2], entry[1])
+ else
+ (entry[57..34], entry[29], entry[33..31], entry[30]) 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])
+ case None -> exit (SignalExceptionTLB(if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
+ }
+}
+
function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
{
err := (if (accessType == StoreData) then AdES else AdEL);
let currentAccessLevel = getAccessLevel() in
let (requiredLevel, addr) = switch(vAddr[63..62]) {
case 0b11 -> switch(vAddr[61..31], vAddr[30..29]) { (* xkseg *)
- case (0b1111111111111111111111111111111, 0b11) -> exit (SignalException(err)) (* kseg3 mapped 32-bit compat TODO *)
- case (0b1111111111111111111111111111111, 0b10) -> exit (SignalException(err)) (* sseg mapped 32-bit compat TODO *)
- case (0b1111111111111111111111111111111, 0b01) -> (Kernel, EXTZ(vAddr[28..0])) (* kseg1 unmapped uncached 32-bit compat *)
- case (0b1111111111111111111111111111111, 0b00) -> (Kernel, EXTZ(vAddr[28..0])) (* kseg0 unmapped cached 32-bit compat *)
- case (_, _) -> exit (SignalException(err)) (* xkseg mapped TODO *)
+ case (0b1111111111111111111111111111111, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *)
+ case (0b1111111111111111111111111111111, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *)
+ case (0b1111111111111111111111111111111, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
+ case (0b1111111111111111111111111111111, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
+ case (_, _) -> (Kernel, None) (* xkseg mapped *)
}
- case 0b10 -> (Kernel, EXTZ(vAddr[58..0])) (* xkphys bits 61-59 are cache mode which we ignore *)
- case 0b01 -> exit (SignalException(err)) (* xsseg - supervisor mapped TODO *)
- case 0b00 -> exit (SignalException(err)) (* xuseg - user mapped TODO *)
+ case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode which we ignore *)
+ case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *)
+ case 0b00 -> (User, None) (* xuseg - user mapped *)
} in
if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
exit (SignalException(err))
- else
- addr
+ else switch(addr) {
+ case (Some(a)) -> a
+ case None -> TLBTranslate2(vAddr, accessType)
+ }
}
typedef regno = bit[5] (* a register number *)
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 7872a5b5..313babe4 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -500,6 +500,24 @@ let mips_register_data_all = [
("CP0Compare", (D_decreasing, 32, 31));
("CP0HWREna", (D_decreasing, 32, 31));
("CP0UserLocal", (D_decreasing, 64, 63));
+ ("TLBProbe" ,(D_decreasing, 1, 0));
+ ("TLBIndex" ,(D_decreasing, 3, 2));
+ ("TLBRandom" ,(D_decreasing, 3, 2));
+ ("TLBEntryLo0",(D_decreasing, 30, 29));
+ ("TLBEntryLo1",(D_decreasing, 30, 29));
+ ("TLBContext" ,(D_decreasing, 64, 63));
+ ("TLBPageMask",(D_decreasing, 16, 15));
+ ("TLBWired" ,(D_decreasing, 3, 2));
+ ("TLBEntryHi" ,(D_decreasing, 64, 63));
+ ("TLBXContext",(D_decreasing, 64, 63));
+ ("TLBEntry00" ,(D_decreasing, 113, 112));
+ ("TLBEntry01" ,(D_decreasing, 113, 112));
+ ("TLBEntry02" ,(D_decreasing, 113, 112));
+ ("TLBEntry03" ,(D_decreasing, 113, 112));
+ ("TLBEntry04" ,(D_decreasing, 113, 112));
+ ("TLBEntry05" ,(D_decreasing, 113, 112));
+ ("TLBEntry06" ,(D_decreasing, 113, 112));
+ ("TLBEntry07" ,(D_decreasing, 113, 112));
]
let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
@@ -880,6 +898,17 @@ let get_addr_trans_regs _ =
(Interp_interface.Reg0("CP0Count", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Count" !reg);
(Interp_interface.Reg0("CP0Compare", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Compare" !reg);
(Interp_interface.Reg0("inBranchDelay", 0, 1, Interp_interface.D_decreasing), Reg.find "inBranchDelay" !reg);
+ (Interp_interface.Reg0("TLBRandom", 2, 3, Interp_interface.D_decreasing), Reg.find "TLBRandom" !reg);
+ (Interp_interface.Reg0("TLBWired", 2, 3, Interp_interface.D_decreasing), Reg.find "TLBWired" !reg);
+ (Interp_interface.Reg0("TLBEntryHi", 63, 64, Interp_interface.D_decreasing), Reg.find "TLBEntryHi" !reg);
+ (Interp_interface.Reg0("TLBEntry00", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry00" !reg);
+ (Interp_interface.Reg0("TLBEntry01", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry01" !reg);
+ (Interp_interface.Reg0("TLBEntry02", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry02" !reg);
+ (Interp_interface.Reg0("TLBEntry03", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry03" !reg);
+ (Interp_interface.Reg0("TLBEntry04", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry04" !reg);
+ (Interp_interface.Reg0("TLBEntry05", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry05" !reg);
+ (Interp_interface.Reg0("TLBEntry06", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry06" !reg);
+ (Interp_interface.Reg0("TLBEntry07", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry07" !reg);
])
let get_opcode pc_a =
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 633dda72..dd7a5093 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -500,6 +500,24 @@ let mips_register_data_all = [
("CP0Compare", (D_decreasing, 32, 31));
("CP0HWREna", (D_decreasing, 32, 31));
("CP0UserLocal", (D_decreasing, 64, 63));
+ ("TLBProbe" ,(D_decreasing, 1, 0));
+ ("TLBIndex" ,(D_decreasing, 3, 2));
+ ("TLBRandom" ,(D_decreasing, 3, 2));
+ ("TLBEntryLo0",(D_decreasing, 30, 29));
+ ("TLBEntryLo1",(D_decreasing, 30, 29));
+ ("TLBContext" ,(D_decreasing, 64, 63));
+ ("TLBPageMask",(D_decreasing, 16, 15));
+ ("TLBWired" ,(D_decreasing, 3, 2));
+ ("TLBEntryHi" ,(D_decreasing, 64, 63));
+ ("TLBXContext",(D_decreasing, 64, 63));
+ ("TLBEntry00" ,(D_decreasing, 113, 112));
+ ("TLBEntry01" ,(D_decreasing, 113, 112));
+ ("TLBEntry02" ,(D_decreasing, 113, 112));
+ ("TLBEntry03" ,(D_decreasing, 113, 112));
+ ("TLBEntry04" ,(D_decreasing, 113, 112));
+ ("TLBEntry05" ,(D_decreasing, 113, 112));
+ ("TLBEntry06" ,(D_decreasing, 113, 112));
+ ("TLBEntry07" ,(D_decreasing, 113, 112));
]
let cheri_register_data_all = mips_register_data_all @ [
@@ -968,6 +986,17 @@ let get_addr_trans_regs _ =
(Interp_interface.Reg0("CP0Count", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Count" !reg);
(Interp_interface.Reg0("CP0Compare", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Compare" !reg);
(Interp_interface.Reg0("inBranchDelay", 0, 1, Interp_interface.D_decreasing), Reg.find "inBranchDelay" !reg);
+ (Interp_interface.Reg0("TLBRandom", 2, 3, Interp_interface.D_decreasing), Reg.find "TLBRandom" !reg);
+ (Interp_interface.Reg0("TLBWired", 2, 3, Interp_interface.D_decreasing), Reg.find "TLBWired" !reg);
+ (Interp_interface.Reg0("TLBEntryHi", 63, 64, Interp_interface.D_decreasing), Reg.find "TLBEntryHi" !reg);
+ (Interp_interface.Reg0("TLBEntry00", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry00" !reg);
+ (Interp_interface.Reg0("TLBEntry01", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry01" !reg);
+ (Interp_interface.Reg0("TLBEntry02", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry02" !reg);
+ (Interp_interface.Reg0("TLBEntry03", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry03" !reg);
+ (Interp_interface.Reg0("TLBEntry04", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry04" !reg);
+ (Interp_interface.Reg0("TLBEntry05", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry05" !reg);
+ (Interp_interface.Reg0("TLBEntry06", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry06" !reg);
+ (Interp_interface.Reg0("TLBEntry07", 112, 113, Interp_interface.D_decreasing), Reg.find "TLBEntry07" !reg);
])
let get_opcode pc_a =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:12:21 +0000