fixes to make counter interrupt work: don't attempt to read register fields during instruction fetch as this is apparently broken, writing to fields also a bit dodgy. Finally only raise exception if exl and erl are not set.

2 files changed, 7 insertions, 4 deletions

diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index ec4e8f8e..53a813e6 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1374,7 +1374,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
       case (0b01001,0b000) -> CP0Count := reg_val[31..0]
       case (0b01011,0b000) -> {  (* 11, sel 0: Compare reg *)
         CP0Compare := reg_val[31..0]; 
-        (CP0Cause.IP)[15] := 0
+        (CP0Cause[15]) := bitzero;
       }
       case (0b01100,0b000) -> {  (* 12 Status *)
         (CP0Status.CU)  := reg_val[31..28];
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 28afb156..f01d6f4e 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -224,15 +224,18 @@ function unit checkCP0Access () =
 
 function unit incrementCP0Count() = {
   CP0Count := (CP0Count + 1);
-  if (CP0Count == CP0Compare) then {
-    ((CP0Cause.IP)[15]) := bitone;
+  if (unsigned(CP0Count) == unsigned(CP0Compare)) then {
+    (CP0Cause[15]) := bitone;
   };
   (* XXX Sail does not allow reading fields here :-( *)
   let (bit[32])status = CP0Status in
   let (bit[32])cause  = CP0Cause in
   let (bit[8]) ims = (status[15..8]) in
   let (bit[8]) ips = (cause[15..8]) in
-  if ((CP0Status.IE) & ((ips & ims) != 0x00)) then
+  let ie           = status[0] in
+  let exl          = status[1] in
+  let erl          = status[2] in
+  if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then
     exit (SignalException(Int));
 }