diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/platform.ml | 2 | ||||
| -rw-r--r-- | riscv/riscv.sail | 6 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 3 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 14 |
4 files changed, 14 insertions, 11 deletions
diff --git a/riscv/platform.ml b/riscv/platform.ml index ddae4840..092df80f 100644 --- a/riscv/platform.ml +++ b/riscv/platform.ml @@ -102,7 +102,7 @@ let insns_per_tick () = Big_int.of_int P.insns_per_tick let reservation = ref "none" (* shouldn't match any valid address *) let load_reservation addr = - Printf.eprintf "reservation <- %s\n" (!reservation); + Printf.eprintf "reservation <- %s\n" (string_of_bits addr); reservation := string_of_bits addr let match_reservation addr = diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 687531c1..7f51ba85 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -868,9 +868,7 @@ union clause ast = SFENCE_VMA : (regbits, regbits) mapping clause encdec = SFENCE_VMA(rs1, rs2) <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SFENCE_VMA(rs1, rs2) = { - /* FIXME: spec leaves unspecified what happens if this is executed in M-mode. - We assume it is the same as S-mode, which is definitely wrong. - */ + /* TODO: handle PMP/TLB synchronization when executed in M-mode. */ if cur_privilege == User then { handle_illegal(); false } else match (architecture(mstatus.SXL()), mstatus.TVM()) { (Some(RV64), true) => { handle_illegal(); false }, @@ -922,7 +920,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(a val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} function process_loadres(rd, addr, value, is_unsigned) = match extend_value(is_unsigned, value) { - MemValue(result) => { X(rd) = result; load_reservation(addr); true }, + MemValue(result) => { load_reservation(addr); X(rd) = result; true }, MemException(e) => { handle_mem_exception(addr, e); false } } diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index e7ca9418..6b903e70 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -245,5 +245,6 @@ function init_platform() -> unit = { } function tick_platform() -> unit = { - htif_tick() + cancel_reservation(); + htif_tick(); } diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index e8128edf..3152b95c 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -793,7 +793,7 @@ union ctl_result = { function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits)) -> xlenbits = { print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info))); - cancel_reservation(); + match (del_priv) { Machine => { mcause->IsInterrupt() = intr; @@ -809,6 +809,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log + cancel_reservation(); + match tvec_addr(mtvec, mcause) { Some(epc) => epc, None() => internal_error("Invalid mtvec mode") @@ -832,6 +834,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log + cancel_reservation(); + match tvec_addr(stvec, scause) { Some(epc) => epc, None() => internal_error("Invalid stvec mode") @@ -858,10 +862,10 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, cur_privilege = privLevel_of_bits(mstatus.MPP()); mstatus->MPP() = privLevel_to_bits(User); - cancel_reservation(); - print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); + + cancel_reservation(); mepc }, (_, CTL_SRET()) => { @@ -871,10 +875,10 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, cur_privilege = if mstatus.SPP() == true then Supervisor else User; mstatus->SPP() = false; - cancel_reservation(); - print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); + + cancel_reservation(); sepc } } |