Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add Zawrs extension #398

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add Zawrs extension #398

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_platform.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
57 changes: 57 additions & 0 deletions model/riscv_insts_zawrs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 */
/*=======================================================================================*/
Timmmm marked this conversation as resolved.
Show resolved Hide resolved

/* ****************************************************************** */
/* 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 ();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if the best way to handle this is via waiting in the actual execute function. WFI doesn't work like this (to be fair it doesn't work at all because there's no proper interface for injecting interrupts currently).

Maybe the model should be a state machine and the step() function handled the WFI and WRS states explicitly?

I dunno, we probably need to think about this properly. Maybe this is fine for now though since the platform callbacks are just hard-coded to time out immediately.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The intent here is two folds:

  1. As a precise documentation of the ISA - this shows that the execution stalls while the instruction waits for these three conditions a) a snoop that invalidates the reservation set due to a store from another hart or a device b) an interrupt becomes pending c) the wait times out.
  2. Allows the platform test bench to inject these into the mode - a snoop invalidation or the platform specific timer timeout. This would also include advancing cycles and time.

We cannot step() as it is presently as we cannot fetch or execute instructions when stalled.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I agree it is nice to document the stalls like this. But documentation isn't the only purpose of the model. I think we want to be a bit careful about this because this is the first bit of code in the model that assumes that step() can block.

We cannot step() as it is presently as we cannot fetch or execute instructions when stalled.

My feeling is that step() should really mean "step the model state", not "fetch and execute an instruction". At the moment those are exactly the same because none of the execute functions call platform callbacks to wait for an event, including WFI. If step() blocks you need threads in lots of situations (e.g. multiple harts, cosimulation), which are quite a pain in C++ and even worse in C.

But it's true that turning step() into an explicit state machine would make the code less clear. Hmm.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thats why I wrote "as it is presently". I dont think it would make the code less clear as a state machine. We would need instead of RETIRE_SUCCESS, something like STALL_UNTIL and the code should setup the conditions for "until". The model would then want the execution to resume after the STALL_UNTIL - STALL_UNTIL then becomes sort of like a swapcontext().

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

something like STALL_UNTIL

Yeah exactly! We also use RETIRE_DEBUG_TRIGGER in Retired, and we should really have RETIRE_ILLEGAL too - see #412.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

there's no proper interface for injecting interrupts currently

#395 provides timer interrupts.


platform_stop_wrs_timeout();
Timmmm marked this conversation as resolved.
Show resolved Hide resolved

let timed_out = reservation_set_valid() & not(interrupts_pending());

match (op, timed_out) {
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
(_, 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)
12 changes: 12 additions & 0 deletions model/riscv_platform.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 3 additions & 0 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions model/riscv_types.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions ocaml_emulator/platform.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading