1 files changed, 0 insertions, 52 deletions
diff --git a/cheri/sail_latex/sailfnexecuteMTCzero.tex b/cheri/sail_latex/sailfnexecuteMTCzero.tex
deleted file mode 100644
index 61c6703e..00000000
--- a/cheri/sail_latex/sailfnexecuteMTCzero.tex
+++ /dev/null
@@ -1,52 +0,0 @@
-function clause #\hyperref[zexecute]{execute}# (#\hyperref[zMTCzero]{MTC0}#(rt, rd, sel, double)) = {
-  #\hyperref[zcheckCPzeroAccess]{checkCP0Access}#();
-  let reg_val = #\hyperref[zrGPR]{rGPR}#(rt) in
-  match (rd, sel)
-    {
-      (0b00000,0b000) => TLBIndex = #\hyperref[zmask]{mask}#(reg_val), /* NB no write to TLBProbe */
-      (0b00001,0b000) => (),                       /* TLBRandom is read only */
-      (0b00010,0b000) => TLBEntryLo0->#\hyperref[zbits]{bits}#() = reg_val,
-      (0b00011,0b000) => TLBEntryLo1->#\hyperref[zbits]{bits}#() = reg_val,
-      (0b00100,0b000) => TLBContext->#\hyperref[zPTEBase]{PTEBase}#() = reg_val[63..23],
-      (0b00100,0b010) => CP0UserLocal = reg_val,
-      (0b00101,0b000) => TLBPageMask  = reg_val[28..13],
-      (0b00110,0b000) => {
-        TLBWired     = #\hyperref[zmask]{mask}#(reg_val);
-        TLBRandom    = TLBIndexMax;
-      },
-      (0b00111,0b000) => CP0HWREna = (reg_val[31..29] @ 0b0000000000000000000000000 @ reg_val[3..0]),
-      (0b01000,0b000) => (), /* BadVAddr read only */
-      (0b01001,0b000) => CP0Count = reg_val[31..0],
-      (0b01010,0b000) => {
-        TLBEntryHi->#\hyperref[zR]{R}#()    = reg_val[63..62];
-        TLBEntryHi->#\hyperref[zVPNtwo]{VPN2}#() = reg_val[39..13];
-        TLBEntryHi->#\hyperref[zASID]{ASID}#() = reg_val[7..0];
-      },
-      (0b01011,0b000) => {  /* 11, sel 0: Compare reg */
-	CP0Compare = reg_val[31..0];
-        CP0Cause->#\hyperref[zIP]{IP}#() = CP0Cause.#\hyperref[zIP]{IP}#() & 0x7f; /* clear IP7 */
-      },
-      (0b01100,0b000) => {  /* 12 Status */
-        CP0Status->#\hyperref[zCU]{CU}#()  = reg_val[31..28];
-        CP0Status->#\hyperref[zBEV]{BEV}#() = reg_val[22];
-        CP0Status->#\hyperref[zIM]{IM}#()  = reg_val[15..8];
-        CP0Status->#\hyperref[zKX]{KX}#()  = reg_val[7];
-        CP0Status->#\hyperref[zSX]{SX}#()  = reg_val[6];
-        CP0Status->#\hyperref[zUX]{UX}#()  = reg_val[5];
-        CP0Status->#\hyperref[zKSU]{KSU}#() = reg_val[4..3];
-        CP0Status->#\hyperref[zERL]{ERL}#() = reg_val[2];
-        CP0Status->#\hyperref[zEXL]{EXL}#() = reg_val[1];
-        CP0Status->#\hyperref[zIE]{IE}#()  = reg_val[0];
-      },
-      (0b01101,0b000) => {   /* 13 Cause */
-        CP0Cause->#\hyperref[zIV]{IV}#() = reg_val[23]; /* TODO special interrupt vector not implemeneted */
-        let ip = CP0Cause.#\hyperref[zIP]{IP}#() in
-        CP0Cause->#\hyperref[zIP]{IP}#() = ((ip[7..2]) @ (reg_val[9..8]));
-      },
-      (0b01110,0b000) => CP0EPC = reg_val, /* 14, EPC */
-      (0b10000,0b000) => CP0ConfigK0 = reg_val[2..0], /*  K0 cache config 16: Config0 */
-      (0b10100,0b000) => TLBXContext->#\hyperref[zXPTEBase]{XPTEBase}#() = reg_val[63..33],
-      (0b11110,0b000) => CP0ErrorEPC = reg_val, /* 30, ErrorEPC */
-      _               => (#\hyperref[zSignalException]{SignalException}#(ResI))
-    }
-}