mips.sail: add an 'inBranchDelay' register so that SignalException can set correct state on exception. branchPending does not work because it is cleared before executing the branch delay.

2 files changed, 7 insertions, 6 deletions

diff --git a/mips/mips.sail b/mips/mips.sail
index 42c86b49..99054cdb 100644
--- a/mips/mips.sail
+++ b/mips/mips.sail
@@ -47,9 +47,9 @@ typedef StatusReg = register bits [31:0] {
 register (StatusReg) CP0Status
 
 (* Implementation registers -- not ISA defined *)
-register (bit[1])  branchPending
-register (bit[1])  exceptionSignalled
-register (bit[64]) delayedPC
+register (bit[1])  branchPending      (* Set by branch instructions to implement branch delay *)
+register (bit[1])  inBranchDelay      (* Needs to be set by outside world when in branch delay slot *)
+register (bit[64]) delayedPC          (* Set by branch instructions to implement branch delay *)
 
 (* General purpose registers *)
 
@@ -150,7 +150,7 @@ function unit SignalException ((Exception) ex) =
     (* Only update EPC and BD if not already in EXL mode *)
     if (~ (CP0Status.EXL)) then 
       {
-        if (branchPending == 0b1) then
+        if (inBranchDelay[0]) then
           {
             CP0EPC := PC - 4;
             CP0Cause.BD := 1;
@@ -174,7 +174,6 @@ function unit SignalException ((Exception) ex) =
       nextPC := vectorBase + EXTS(vectorOffset);
       CP0Cause.ExcCode      := ExceptionCode(ex);
       CP0Status.EXL         := 1;
-      exceptionSignalled    := 1;
   }
 
 function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 17adf7b7..9d0af83d 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -847,12 +847,14 @@ let set_next_instruction_address model =
        let n_pc = register_value_of_address n_addr D_decreasing in
        begin
          reg := Reg.add "nextPC" n_pc !reg;
+         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
        end
      | (Some pc_val, Some 1, Some delayedPC) -> 
        (* delay slot -- branch to delayed PC and clear branchPending *)
        begin 
          reg := Reg.add "nextPC" (register_value_of_address delayedPC D_decreasing) !reg;
-         reg := Reg.add "branchPending" (register_value_of_integer 1 1 Interp_interface.D_decreasing Nat_big_num.zero) !reg
+         reg := Reg.add "branchPending" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
+         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Interp_interface.D_decreasing (Nat_big_num.of_int 1)) !reg;
        end
      | (_, _, _) -> errorf "PC address contains unknown or undefined"; exit 1)