diff options
| -rw-r--r-- | mips/mips.sail | 9 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 4 |
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) |