summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mips/mips_insts.sail5
-rw-r--r--mips/mips_prelude.sail154
-rw-r--r--src/lem_interp/run_with_elf.ml123
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml124
4 files changed, 367 insertions, 39 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index e1f8d8e0..6e1f0a06 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1396,7 +1396,8 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
checkCP0Access();
let (bit[64]) result = switch (rd, sel)
{
- case (0b00000,0b000) -> (0x00000000 : [TLBProbe] : 0x0000000 : TLBIndex) (* 0, TLB Index *)
+ case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in
+ (0x00000000 : [TLBProbe] : idx) (* 0, TLB Index *)
case (0b00001,0b000) -> EXTZ(TLBRandom) (* 1, TLB Random *)
case (0b00010,0b000) -> TLBEntryLo0 (* 2, TLB EntryLo0 *)
case (0b00011,0b000) -> TLBEntryLo1 (* 3, TLB EntryLo1 *)
@@ -1425,7 +1426,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
: 0b000)
case (0b10000,0b001) -> EXTZ( (* 16, sel 1: Config1 *)
0b1 (* M *)
- : 0b000111 (* MMU size-1 *)
+ : TLBIndexMax (* MMU size-1 *)
: 0b000 (* IS icache sets *)
: 0b000 (* IL icache lines *)
: 0b000 (* IA icache assoc. *)
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 989fddb9..27efc4b5 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -85,9 +85,9 @@ typedef XContextReg = register bits [63 : 0] {
30 .. 4: BadVPN2;
}
-let ([:8:]) TLBNumEntries = 8
-typedef TLBIndexT = (bit[3])
-let (TLBIndexT) TLBIndexMax = 0b111
+let ([:64:]) TLBNumEntries = 64
+typedef TLBIndexT = (bit[6])
+let (TLBIndexT) TLBIndexMax = 0b111111
let MAX_VA = unsigned(0xffffffffff)
let MAX_PA = unsigned(0xfffffffff)
@@ -114,13 +114,13 @@ typedef TLBEntry = register bits [116 : 0] {
}
register (bit[1]) TLBProbe
-register (bit[3]) TLBIndex
-register (bit[3]) TLBRandom
+register (TLBIndexT) TLBIndex
+register (TLBIndexT) TLBRandom
register (TLBEntryLoReg) TLBEntryLo0
register (TLBEntryLoReg) TLBEntryLo1
register (ContextReg) TLBContext
register (bit[16]) TLBPageMask
-register (bit[3]) TLBWired
+register (TLBIndexT) TLBWired
register (TLBEntryHiReg) TLBEntryHi
register (XContextReg) TLBXContext
@@ -132,8 +132,64 @@ register (TLBEntry) TLBEntry04
register (TLBEntry) TLBEntry05
register (TLBEntry) TLBEntry06
register (TLBEntry) TLBEntry07
-
-let (vector <0, 8, inc, (TLBEntry)>) TLBEntries = [
+register (TLBEntry) TLBEntry08
+register (TLBEntry) TLBEntry09
+register (TLBEntry) TLBEntry10
+register (TLBEntry) TLBEntry11
+register (TLBEntry) TLBEntry12
+register (TLBEntry) TLBEntry13
+register (TLBEntry) TLBEntry14
+register (TLBEntry) TLBEntry15
+register (TLBEntry) TLBEntry16
+register (TLBEntry) TLBEntry17
+register (TLBEntry) TLBEntry18
+register (TLBEntry) TLBEntry19
+register (TLBEntry) TLBEntry20
+register (TLBEntry) TLBEntry21
+register (TLBEntry) TLBEntry22
+register (TLBEntry) TLBEntry23
+register (TLBEntry) TLBEntry24
+register (TLBEntry) TLBEntry25
+register (TLBEntry) TLBEntry26
+register (TLBEntry) TLBEntry27
+register (TLBEntry) TLBEntry28
+register (TLBEntry) TLBEntry29
+register (TLBEntry) TLBEntry30
+register (TLBEntry) TLBEntry31
+register (TLBEntry) TLBEntry32
+register (TLBEntry) TLBEntry33
+register (TLBEntry) TLBEntry34
+register (TLBEntry) TLBEntry35
+register (TLBEntry) TLBEntry36
+register (TLBEntry) TLBEntry37
+register (TLBEntry) TLBEntry38
+register (TLBEntry) TLBEntry39
+register (TLBEntry) TLBEntry40
+register (TLBEntry) TLBEntry41
+register (TLBEntry) TLBEntry42
+register (TLBEntry) TLBEntry43
+register (TLBEntry) TLBEntry44
+register (TLBEntry) TLBEntry45
+register (TLBEntry) TLBEntry46
+register (TLBEntry) TLBEntry47
+register (TLBEntry) TLBEntry48
+register (TLBEntry) TLBEntry49
+register (TLBEntry) TLBEntry50
+register (TLBEntry) TLBEntry51
+register (TLBEntry) TLBEntry52
+register (TLBEntry) TLBEntry53
+register (TLBEntry) TLBEntry54
+register (TLBEntry) TLBEntry55
+register (TLBEntry) TLBEntry56
+register (TLBEntry) TLBEntry57
+register (TLBEntry) TLBEntry58
+register (TLBEntry) TLBEntry59
+register (TLBEntry) TLBEntry60
+register (TLBEntry) TLBEntry61
+register (TLBEntry) TLBEntry62
+register (TLBEntry) TLBEntry63
+
+let (vector <0, 64, inc, (TLBEntry)>) TLBEntries = [
TLBEntry00,
TLBEntry01,
TLBEntry02,
@@ -141,7 +197,63 @@ TLBEntry03,
TLBEntry04,
TLBEntry05,
TLBEntry06,
-TLBEntry07
+TLBEntry07,
+TLBEntry08,
+TLBEntry09,
+TLBEntry10,
+TLBEntry11,
+TLBEntry12,
+TLBEntry13,
+TLBEntry14,
+TLBEntry15,
+TLBEntry16,
+TLBEntry17,
+TLBEntry18,
+TLBEntry19,
+TLBEntry20,
+TLBEntry21,
+TLBEntry22,
+TLBEntry23,
+TLBEntry24,
+TLBEntry25,
+TLBEntry26,
+TLBEntry27,
+TLBEntry28,
+TLBEntry29,
+TLBEntry30,
+TLBEntry31,
+TLBEntry32,
+TLBEntry33,
+TLBEntry34,
+TLBEntry35,
+TLBEntry36,
+TLBEntry37,
+TLBEntry38,
+TLBEntry39,
+TLBEntry40,
+TLBEntry41,
+TLBEntry42,
+TLBEntry43,
+TLBEntry44,
+TLBEntry45,
+TLBEntry46,
+TLBEntry47,
+TLBEntry48,
+TLBEntry49,
+TLBEntry50,
+TLBEntry51,
+TLBEntry52,
+TLBEntry53,
+TLBEntry54,
+TLBEntry55,
+TLBEntry56,
+TLBEntry57,
+TLBEntry58,
+TLBEntry59,
+TLBEntry60,
+TLBEntry61,
+TLBEntry62,
+TLBEntry63
]
register (bit[32]) CP0Compare
@@ -398,25 +510,13 @@ function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
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
+ 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
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 5e238750..95d25336 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -503,15 +503,16 @@ let mips_register_data_all = [
("CP0UserLocal", (D_decreasing, 64, 63));
("CP0BadVAddr", (D_decreasing, 64, 63));
("TLBProbe" ,(D_decreasing, 1, 0));
- ("TLBIndex" ,(D_decreasing, 3, 2));
- ("TLBRandom" ,(D_decreasing, 3, 2));
+ ("TLBIndex" ,(D_decreasing, 6, 5));
+ ("TLBRandom" ,(D_decreasing, 6, 5));
("TLBEntryLo0",(D_decreasing, 64, 63));
("TLBEntryLo1",(D_decreasing, 64, 63));
("TLBContext" ,(D_decreasing, 64, 63));
("TLBPageMask",(D_decreasing, 16, 15));
- ("TLBWired" ,(D_decreasing, 3, 2));
+ ("TLBWired" ,(D_decreasing, 6, 5));
("TLBEntryHi" ,(D_decreasing, 64, 63));
("TLBXContext",(D_decreasing, 64, 63));
+
("TLBEntry00" ,(D_decreasing, 117, 116));
("TLBEntry01" ,(D_decreasing, 117, 116));
("TLBEntry02" ,(D_decreasing, 117, 116));
@@ -520,6 +521,62 @@ let mips_register_data_all = [
("TLBEntry05" ,(D_decreasing, 117, 116));
("TLBEntry06" ,(D_decreasing, 117, 116));
("TLBEntry07" ,(D_decreasing, 117, 116));
+ ("TLBEntry08" ,(D_decreasing, 117, 116));
+ ("TLBEntry09" ,(D_decreasing, 117, 116));
+ ("TLBEntry10" ,(D_decreasing, 117, 116));
+ ("TLBEntry11" ,(D_decreasing, 117, 116));
+ ("TLBEntry12" ,(D_decreasing, 117, 116));
+ ("TLBEntry13" ,(D_decreasing, 117, 116));
+ ("TLBEntry14" ,(D_decreasing, 117, 116));
+ ("TLBEntry15" ,(D_decreasing, 117, 116));
+ ("TLBEntry16" ,(D_decreasing, 117, 116));
+ ("TLBEntry17" ,(D_decreasing, 117, 116));
+ ("TLBEntry18" ,(D_decreasing, 117, 116));
+ ("TLBEntry19" ,(D_decreasing, 117, 116));
+ ("TLBEntry20" ,(D_decreasing, 117, 116));
+ ("TLBEntry21" ,(D_decreasing, 117, 116));
+ ("TLBEntry22" ,(D_decreasing, 117, 116));
+ ("TLBEntry23" ,(D_decreasing, 117, 116));
+ ("TLBEntry24" ,(D_decreasing, 117, 116));
+ ("TLBEntry25" ,(D_decreasing, 117, 116));
+ ("TLBEntry26" ,(D_decreasing, 117, 116));
+ ("TLBEntry27" ,(D_decreasing, 117, 116));
+ ("TLBEntry28" ,(D_decreasing, 117, 116));
+ ("TLBEntry29" ,(D_decreasing, 117, 116));
+ ("TLBEntry30" ,(D_decreasing, 117, 116));
+ ("TLBEntry31" ,(D_decreasing, 117, 116));
+ ("TLBEntry32" ,(D_decreasing, 117, 116));
+ ("TLBEntry33" ,(D_decreasing, 117, 116));
+ ("TLBEntry34" ,(D_decreasing, 117, 116));
+ ("TLBEntry35" ,(D_decreasing, 117, 116));
+ ("TLBEntry36" ,(D_decreasing, 117, 116));
+ ("TLBEntry37" ,(D_decreasing, 117, 116));
+ ("TLBEntry38" ,(D_decreasing, 117, 116));
+ ("TLBEntry39" ,(D_decreasing, 117, 116));
+ ("TLBEntry40" ,(D_decreasing, 117, 116));
+ ("TLBEntry41" ,(D_decreasing, 117, 116));
+ ("TLBEntry42" ,(D_decreasing, 117, 116));
+ ("TLBEntry43" ,(D_decreasing, 117, 116));
+ ("TLBEntry44" ,(D_decreasing, 117, 116));
+ ("TLBEntry45" ,(D_decreasing, 117, 116));
+ ("TLBEntry46" ,(D_decreasing, 117, 116));
+ ("TLBEntry47" ,(D_decreasing, 117, 116));
+ ("TLBEntry48" ,(D_decreasing, 117, 116));
+ ("TLBEntry49" ,(D_decreasing, 117, 116));
+ ("TLBEntry50" ,(D_decreasing, 117, 116));
+ ("TLBEntry51" ,(D_decreasing, 117, 116));
+ ("TLBEntry52" ,(D_decreasing, 117, 116));
+ ("TLBEntry53" ,(D_decreasing, 117, 116));
+ ("TLBEntry54" ,(D_decreasing, 117, 116));
+ ("TLBEntry55" ,(D_decreasing, 117, 116));
+ ("TLBEntry56" ,(D_decreasing, 117, 116));
+ ("TLBEntry57" ,(D_decreasing, 117, 116));
+ ("TLBEntry58" ,(D_decreasing, 117, 116));
+ ("TLBEntry59" ,(D_decreasing, 117, 116));
+ ("TLBEntry60" ,(D_decreasing, 117, 116));
+ ("TLBEntry61" ,(D_decreasing, 117, 116));
+ ("TLBEntry62" ,(D_decreasing, 117, 116));
+ ("TLBEntry63" ,(D_decreasing, 117, 116));
("UART_WDATA" ,(D_decreasing, 8, 7));
("UART_RDATA" ,(D_decreasing, 8, 7));
@@ -909,8 +966,8 @@ 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("TLBRandom", 5, 6, Interp_interface.D_decreasing), Reg.find "TLBRandom" !reg);
+ (Interp_interface.Reg0("TLBWired", 5, 6, 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", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry00" !reg);
(Interp_interface.Reg0("TLBEntry01", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry01" !reg);
@@ -920,6 +977,62 @@ let get_addr_trans_regs _ =
(Interp_interface.Reg0("TLBEntry05", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry05" !reg);
(Interp_interface.Reg0("TLBEntry06", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry06" !reg);
(Interp_interface.Reg0("TLBEntry07", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry07" !reg);
+ (Interp_interface.Reg0("TLBEntry08", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry08" !reg);
+ (Interp_interface.Reg0("TLBEntry09", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry09" !reg);
+ (Interp_interface.Reg0("TLBEntry10", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry10" !reg);
+ (Interp_interface.Reg0("TLBEntry11", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry11" !reg);
+ (Interp_interface.Reg0("TLBEntry12", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry12" !reg);
+ (Interp_interface.Reg0("TLBEntry13", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry13" !reg);
+ (Interp_interface.Reg0("TLBEntry14", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry14" !reg);
+ (Interp_interface.Reg0("TLBEntry15", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry15" !reg);
+ (Interp_interface.Reg0("TLBEntry16", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry16" !reg);
+ (Interp_interface.Reg0("TLBEntry17", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry17" !reg);
+ (Interp_interface.Reg0("TLBEntry18", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry18" !reg);
+ (Interp_interface.Reg0("TLBEntry19", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry19" !reg);
+ (Interp_interface.Reg0("TLBEntry20", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry20" !reg);
+ (Interp_interface.Reg0("TLBEntry21", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry21" !reg);
+ (Interp_interface.Reg0("TLBEntry22", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry22" !reg);
+ (Interp_interface.Reg0("TLBEntry23", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry23" !reg);
+ (Interp_interface.Reg0("TLBEntry24", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry24" !reg);
+ (Interp_interface.Reg0("TLBEntry25", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry25" !reg);
+ (Interp_interface.Reg0("TLBEntry26", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry26" !reg);
+ (Interp_interface.Reg0("TLBEntry27", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry27" !reg);
+ (Interp_interface.Reg0("TLBEntry28", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry28" !reg);
+ (Interp_interface.Reg0("TLBEntry29", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry29" !reg);
+ (Interp_interface.Reg0("TLBEntry30", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry30" !reg);
+ (Interp_interface.Reg0("TLBEntry31", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry31" !reg);
+ (Interp_interface.Reg0("TLBEntry32", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry32" !reg);
+ (Interp_interface.Reg0("TLBEntry33", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry33" !reg);
+ (Interp_interface.Reg0("TLBEntry34", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry34" !reg);
+ (Interp_interface.Reg0("TLBEntry35", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry35" !reg);
+ (Interp_interface.Reg0("TLBEntry36", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry36" !reg);
+ (Interp_interface.Reg0("TLBEntry37", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry37" !reg);
+ (Interp_interface.Reg0("TLBEntry38", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry38" !reg);
+ (Interp_interface.Reg0("TLBEntry39", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry39" !reg);
+ (Interp_interface.Reg0("TLBEntry40", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry40" !reg);
+ (Interp_interface.Reg0("TLBEntry41", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry41" !reg);
+ (Interp_interface.Reg0("TLBEntry42", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry42" !reg);
+ (Interp_interface.Reg0("TLBEntry43", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry43" !reg);
+ (Interp_interface.Reg0("TLBEntry44", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry44" !reg);
+ (Interp_interface.Reg0("TLBEntry45", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry45" !reg);
+ (Interp_interface.Reg0("TLBEntry46", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry46" !reg);
+ (Interp_interface.Reg0("TLBEntry47", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry47" !reg);
+ (Interp_interface.Reg0("TLBEntry48", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry48" !reg);
+ (Interp_interface.Reg0("TLBEntry49", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry49" !reg);
+ (Interp_interface.Reg0("TLBEntry50", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry50" !reg);
+ (Interp_interface.Reg0("TLBEntry51", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry51" !reg);
+ (Interp_interface.Reg0("TLBEntry52", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry52" !reg);
+ (Interp_interface.Reg0("TLBEntry53", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry53" !reg);
+ (Interp_interface.Reg0("TLBEntry54", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry54" !reg);
+ (Interp_interface.Reg0("TLBEntry55", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry55" !reg);
+ (Interp_interface.Reg0("TLBEntry56", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry56" !reg);
+ (Interp_interface.Reg0("TLBEntry57", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry57" !reg);
+ (Interp_interface.Reg0("TLBEntry58", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry58" !reg);
+ (Interp_interface.Reg0("TLBEntry59", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry59" !reg);
+ (Interp_interface.Reg0("TLBEntry60", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry60" !reg);
+ (Interp_interface.Reg0("TLBEntry61", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry61" !reg);
+ (Interp_interface.Reg0("TLBEntry62", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry62" !reg);
+ (Interp_interface.Reg0("TLBEntry63", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry63" !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 56b9807b..0b563b27 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -503,15 +503,16 @@ let mips_register_data_all = [
("CP0UserLocal", (D_decreasing, 64, 63));
("CP0BadVAddr", (D_decreasing, 64, 63));
("TLBProbe" ,(D_decreasing, 1, 0));
- ("TLBIndex" ,(D_decreasing, 3, 2));
- ("TLBRandom" ,(D_decreasing, 3, 2));
+ ("TLBIndex" ,(D_decreasing, 6, 5));
+ ("TLBRandom" ,(D_decreasing, 6, 5));
("TLBEntryLo0",(D_decreasing, 64, 63));
("TLBEntryLo1",(D_decreasing, 64, 63));
("TLBContext" ,(D_decreasing, 64, 63));
("TLBPageMask",(D_decreasing, 16, 15));
- ("TLBWired" ,(D_decreasing, 3, 2));
+ ("TLBWired" ,(D_decreasing, 6, 5));
("TLBEntryHi" ,(D_decreasing, 64, 63));
("TLBXContext",(D_decreasing, 64, 63));
+
("TLBEntry00" ,(D_decreasing, 117, 116));
("TLBEntry01" ,(D_decreasing, 117, 116));
("TLBEntry02" ,(D_decreasing, 117, 116));
@@ -520,6 +521,63 @@ let mips_register_data_all = [
("TLBEntry05" ,(D_decreasing, 117, 116));
("TLBEntry06" ,(D_decreasing, 117, 116));
("TLBEntry07" ,(D_decreasing, 117, 116));
+ ("TLBEntry08" ,(D_decreasing, 117, 116));
+ ("TLBEntry09" ,(D_decreasing, 117, 116));
+ ("TLBEntry10" ,(D_decreasing, 117, 116));
+ ("TLBEntry11" ,(D_decreasing, 117, 116));
+ ("TLBEntry12" ,(D_decreasing, 117, 116));
+ ("TLBEntry13" ,(D_decreasing, 117, 116));
+ ("TLBEntry14" ,(D_decreasing, 117, 116));
+ ("TLBEntry15" ,(D_decreasing, 117, 116));
+ ("TLBEntry16" ,(D_decreasing, 117, 116));
+ ("TLBEntry17" ,(D_decreasing, 117, 116));
+ ("TLBEntry18" ,(D_decreasing, 117, 116));
+ ("TLBEntry19" ,(D_decreasing, 117, 116));
+ ("TLBEntry20" ,(D_decreasing, 117, 116));
+ ("TLBEntry21" ,(D_decreasing, 117, 116));
+ ("TLBEntry22" ,(D_decreasing, 117, 116));
+ ("TLBEntry23" ,(D_decreasing, 117, 116));
+ ("TLBEntry24" ,(D_decreasing, 117, 116));
+ ("TLBEntry25" ,(D_decreasing, 117, 116));
+ ("TLBEntry26" ,(D_decreasing, 117, 116));
+ ("TLBEntry27" ,(D_decreasing, 117, 116));
+ ("TLBEntry28" ,(D_decreasing, 117, 116));
+ ("TLBEntry29" ,(D_decreasing, 117, 116));
+ ("TLBEntry30" ,(D_decreasing, 117, 116));
+ ("TLBEntry31" ,(D_decreasing, 117, 116));
+ ("TLBEntry32" ,(D_decreasing, 117, 116));
+ ("TLBEntry33" ,(D_decreasing, 117, 116));
+ ("TLBEntry34" ,(D_decreasing, 117, 116));
+ ("TLBEntry35" ,(D_decreasing, 117, 116));
+ ("TLBEntry36" ,(D_decreasing, 117, 116));
+ ("TLBEntry37" ,(D_decreasing, 117, 116));
+ ("TLBEntry38" ,(D_decreasing, 117, 116));
+ ("TLBEntry39" ,(D_decreasing, 117, 116));
+ ("TLBEntry40" ,(D_decreasing, 117, 116));
+ ("TLBEntry41" ,(D_decreasing, 117, 116));
+ ("TLBEntry42" ,(D_decreasing, 117, 116));
+ ("TLBEntry43" ,(D_decreasing, 117, 116));
+ ("TLBEntry44" ,(D_decreasing, 117, 116));
+ ("TLBEntry45" ,(D_decreasing, 117, 116));
+ ("TLBEntry46" ,(D_decreasing, 117, 116));
+ ("TLBEntry47" ,(D_decreasing, 117, 116));
+ ("TLBEntry48" ,(D_decreasing, 117, 116));
+ ("TLBEntry49" ,(D_decreasing, 117, 116));
+ ("TLBEntry50" ,(D_decreasing, 117, 116));
+ ("TLBEntry51" ,(D_decreasing, 117, 116));
+ ("TLBEntry52" ,(D_decreasing, 117, 116));
+ ("TLBEntry53" ,(D_decreasing, 117, 116));
+ ("TLBEntry54" ,(D_decreasing, 117, 116));
+ ("TLBEntry55" ,(D_decreasing, 117, 116));
+ ("TLBEntry56" ,(D_decreasing, 117, 116));
+ ("TLBEntry57" ,(D_decreasing, 117, 116));
+ ("TLBEntry58" ,(D_decreasing, 117, 116));
+ ("TLBEntry59" ,(D_decreasing, 117, 116));
+ ("TLBEntry60" ,(D_decreasing, 117, 116));
+ ("TLBEntry61" ,(D_decreasing, 117, 116));
+ ("TLBEntry62" ,(D_decreasing, 117, 116));
+ ("TLBEntry63" ,(D_decreasing, 117, 116));
+
("UART_WDATA" ,(D_decreasing, 8, 7));
("UART_RDATA" ,(D_decreasing, 8, 7));
("UART_WRITTEN" ,(D_decreasing, 1, 0));
@@ -996,8 +1054,8 @@ 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("TLBRandom", 5, 6, Interp_interface.D_decreasing), Reg.find "TLBRandom" !reg);
+ (Interp_interface.Reg0("TLBWired", 5, 6, 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", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry00" !reg);
(Interp_interface.Reg0("TLBEntry01", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry01" !reg);
@@ -1007,6 +1065,62 @@ let get_addr_trans_regs _ =
(Interp_interface.Reg0("TLBEntry05", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry05" !reg);
(Interp_interface.Reg0("TLBEntry06", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry06" !reg);
(Interp_interface.Reg0("TLBEntry07", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry07" !reg);
+ (Interp_interface.Reg0("TLBEntry08", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry08" !reg);
+ (Interp_interface.Reg0("TLBEntry09", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry09" !reg);
+ (Interp_interface.Reg0("TLBEntry10", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry10" !reg);
+ (Interp_interface.Reg0("TLBEntry11", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry11" !reg);
+ (Interp_interface.Reg0("TLBEntry12", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry12" !reg);
+ (Interp_interface.Reg0("TLBEntry13", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry13" !reg);
+ (Interp_interface.Reg0("TLBEntry14", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry14" !reg);
+ (Interp_interface.Reg0("TLBEntry15", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry15" !reg);
+ (Interp_interface.Reg0("TLBEntry16", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry16" !reg);
+ (Interp_interface.Reg0("TLBEntry17", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry17" !reg);
+ (Interp_interface.Reg0("TLBEntry18", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry18" !reg);
+ (Interp_interface.Reg0("TLBEntry19", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry19" !reg);
+ (Interp_interface.Reg0("TLBEntry20", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry20" !reg);
+ (Interp_interface.Reg0("TLBEntry21", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry21" !reg);
+ (Interp_interface.Reg0("TLBEntry22", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry22" !reg);
+ (Interp_interface.Reg0("TLBEntry23", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry23" !reg);
+ (Interp_interface.Reg0("TLBEntry24", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry24" !reg);
+ (Interp_interface.Reg0("TLBEntry25", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry25" !reg);
+ (Interp_interface.Reg0("TLBEntry26", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry26" !reg);
+ (Interp_interface.Reg0("TLBEntry27", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry27" !reg);
+ (Interp_interface.Reg0("TLBEntry28", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry28" !reg);
+ (Interp_interface.Reg0("TLBEntry29", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry29" !reg);
+ (Interp_interface.Reg0("TLBEntry30", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry30" !reg);
+ (Interp_interface.Reg0("TLBEntry31", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry31" !reg);
+ (Interp_interface.Reg0("TLBEntry32", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry32" !reg);
+ (Interp_interface.Reg0("TLBEntry33", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry33" !reg);
+ (Interp_interface.Reg0("TLBEntry34", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry34" !reg);
+ (Interp_interface.Reg0("TLBEntry35", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry35" !reg);
+ (Interp_interface.Reg0("TLBEntry36", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry36" !reg);
+ (Interp_interface.Reg0("TLBEntry37", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry37" !reg);
+ (Interp_interface.Reg0("TLBEntry38", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry38" !reg);
+ (Interp_interface.Reg0("TLBEntry39", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry39" !reg);
+ (Interp_interface.Reg0("TLBEntry40", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry40" !reg);
+ (Interp_interface.Reg0("TLBEntry41", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry41" !reg);
+ (Interp_interface.Reg0("TLBEntry42", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry42" !reg);
+ (Interp_interface.Reg0("TLBEntry43", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry43" !reg);
+ (Interp_interface.Reg0("TLBEntry44", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry44" !reg);
+ (Interp_interface.Reg0("TLBEntry45", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry45" !reg);
+ (Interp_interface.Reg0("TLBEntry46", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry46" !reg);
+ (Interp_interface.Reg0("TLBEntry47", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry47" !reg);
+ (Interp_interface.Reg0("TLBEntry48", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry48" !reg);
+ (Interp_interface.Reg0("TLBEntry49", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry49" !reg);
+ (Interp_interface.Reg0("TLBEntry50", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry50" !reg);
+ (Interp_interface.Reg0("TLBEntry51", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry51" !reg);
+ (Interp_interface.Reg0("TLBEntry52", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry52" !reg);
+ (Interp_interface.Reg0("TLBEntry53", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry53" !reg);
+ (Interp_interface.Reg0("TLBEntry54", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry54" !reg);
+ (Interp_interface.Reg0("TLBEntry55", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry55" !reg);
+ (Interp_interface.Reg0("TLBEntry56", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry56" !reg);
+ (Interp_interface.Reg0("TLBEntry57", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry57" !reg);
+ (Interp_interface.Reg0("TLBEntry58", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry58" !reg);
+ (Interp_interface.Reg0("TLBEntry59", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry59" !reg);
+ (Interp_interface.Reg0("TLBEntry60", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry60" !reg);
+ (Interp_interface.Reg0("TLBEntry61", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry61" !reg);
+ (Interp_interface.Reg0("TLBEntry62", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry62" !reg);
+ (Interp_interface.Reg0("TLBEntry63", 116, 117, Interp_interface.D_decreasing), Reg.find "TLBEntry63" !reg);
])
let get_opcode pc_a =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 22:06:50 +0000