diff --git a/Makefile b/Makefile index af355efc1..c71206e02 100644 --- a/Makefile +++ b/Makefile @@ -48,6 +48,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbkb.sail SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_insts_zawrs.sail SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2fdb63f92..86ff6ff06 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -176,3 +176,9 @@ unit memea(mach_bits len, sail_int n) { return UNIT; } + +/* Zawrs : Wait-on-Reservation-Set */ +bool reservation_set_valid(unit u) +{ + return reservation_valid; +} diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 341bd5964..9bf6269cf 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -42,3 +42,6 @@ unit plat_term_write(mach_bits); mach_bits plat_htif_tohost(unit); unit memea(mach_bits, sail_int); + +/* Zawrs : Wait-on-Reservation-Set */ +bool reservation_set_valid(unit); diff --git a/model/riscv_insts_zawrs.sail b/model/riscv_insts_zawrs.sail new file mode 100644 index 000000000..cb6ec1411 --- /dev/null +++ b/model/riscv_insts_zawrs.sail @@ -0,0 +1,57 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +/* This file specifies the instructions in the 'Zawrs' extension. */ + +val reservation_set_valid = { + ocaml: "Platform.reservation_set_valid", + interpreter: "Platform.reservation_set_valid", + c: "reservation_set_valid", + lem: "reservation_set_valid" + } : unit -> bool + +/* ****************************************************************** */ +union clause ast = WRS : (wrsop) + +mapping clause encdec = WRS(WRS_STO) if haveZawrs() + <-> 0b000000011101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveZawrs() + +mapping clause encdec = WRS(WRS_NTO) if haveZawrs() + <-> 0b000000001101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveZawrs() + +/* Hart must resume if a locally enabled interrupt becomes pending, even if delegated */ +function interrupts_pending() -> bool = ((mip.bits() & mie.bits()) != zero_extend(0b0)) + +function clause execute (WRS(op)) = { + + platform_start_wrs_timeout((op == WRS_STO)); + + while reservation_set_valid() & not(interrupts_pending()) & not(platform_is_wrs_timed_out()) do (); + + platform_stop_wrs_timeout(); + + let timed_out = reservation_set_valid() & not(interrupts_pending()); + + match (op, timed_out) { + (_, false) => RETIRE_SUCCESS, + (WRS_STO, true) => RETIRE_SUCCESS, + (WRS_NTO, true) => match cur_privilege { + Machine => { RETIRE_SUCCESS }, + _ => if mstatus.TW() == 0b1 + then { handle_illegal(); RETIRE_FAIL } + else { RETIRE_SUCCESS } + } + } +} + +mapping wrs_mnemonic : wrsop <-> string = { + WRS_STO <-> "wrs.sto", + WRS_NTO <-> "wrs.nto", +} +mapping clause assembly = WRS(op) <-> wrs_mnemonic(op) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 19e3d30ae..42deeb423 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -454,3 +454,15 @@ function platform_wfi() -> unit = { mcycle = mtimecmp; } } + +/* Start implementation defined short timeout if short is true + * For no timeout, start a implementation defined timeout if privilege + * level is less than M. + */ +function platform_start_wrs_timeout(short : bool) -> unit = () + +/* Stop any timer started by WRS */ +function platform_stop_wrs_timeout() -> unit = () + +/* Return status of WRS timer timeout */ +function platform_is_wrs_timed_out() -> bool = true diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 65d141923..0ade1c77f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,6 +168,9 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Zawrs extension support */ +function haveZawrs() -> bool = true + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 2b1c132ec..5b68237d1 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -357,6 +357,9 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} +/* Zawrs : Wait-on-Reservation-Set */ +enum wrsop = {WRS_STO, WRS_NTO} + mapping bool_bits : bool <-> bits(1) = { true <-> 0b1, false <-> 0b0 diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 69f271496..3d04c2285 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -181,3 +181,7 @@ let init arch elf_file = in ( write_rom 0 rom; get_slice_int (cur_arch_bitwidth (), rom_base, Big_int.zero) ) + +(* Zawrs: Wait-on-Reservation-Set *) +let reservation_set_valid () = + "none" <> !reservation