diff options
| -rw-r--r-- | mips/mips_insts.sail | 2 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 9 |
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)); } |