From a365bd24cd1905408798b21f16718e0481683146 Mon Sep 17 00:00:00 2001 From: guan jian <148229859+rez5427@users.noreply.github.com> Date: Mon, 2 Dec 2024 17:34:11 +0800 Subject: [PATCH] Remove pc alignment mask Remove `pc_alignment_mask()` and fix some issues around `xepc` legalisation. 1. `pc_alignment_mask()` didn't zero the lowest bit. 2. `pc_alignment_mask()` was applied ad-hoc after reading `xepc`, but in the spec it is just the read legalisation of `xepc`. 3. `legalize_xpec()` had incorrect condition for allowing `xepc[1]` to be writable. Signed-off-by: guan jian <148229859+rez5427@users.noreply.github.com> Co-authored-by: Yui5427 <785369607@qq.com> Co-authored-by: Jessica Clarke --- model/riscv_sys_control.sail | 4 ++-- model/riscv_sys_exceptions.sail | 26 +++++++++++++------------- model/riscv_sys_regs.sail | 20 ++++++++++++-------- 3 files changed, 27 insertions(+), 23 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 7890e4dbf..25e434866 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -293,7 +293,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); - prepare_xret_target(Machine) & pc_alignment_mask() + prepare_xret_target(Machine) }, (_, CTL_SRET()) => { let prev_priv = cur_privilege; @@ -310,7 +310,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); - prepare_xret_target(Supervisor) & pc_alignment_mask() + prepare_xret_target(Supervisor) }, } } diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index a4e5d6434..d7e030467 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -32,21 +32,21 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { /* xRET handling involves three functions: * - * get_xret_target: used to read the value of the xret target (no control flow transfer) - * set_xret_target: used to write a value of the xret target (no control flow transfer) + * get_xepc: used to read the value of the xret target (no control flow transfer) + * set_xepc: used to write a value of the xret target (no control flow transfer) * prepare_xret_target: used to get the value for control transfer to the xret target */ -val get_xret_target : Privilege -> xlenbits -function get_xret_target(p) = +val get_xepc : Privilege -> xlenbits +function get_xepc(p) = match p { - Machine => mepc, - Supervisor => sepc, + Machine => align_pc(mepc), + Supervisor => align_pc(sepc), User => internal_error(__FILE__, __LINE__, "Invalid privilege level"), } -val set_xret_target : (Privilege, xlenbits) -> xlenbits -function set_xret_target(p, value) = { +val set_xepc : (Privilege, xlenbits) -> xlenbits +function set_xepc(p, value) = { let target = legalize_xepc(value); match p { Machine => mepc = target, @@ -58,7 +58,7 @@ function set_xret_target(p, value) = { val prepare_xret_target : (Privilege) -> xlenbits function prepare_xret_target(p) = - get_xret_target(p) + get_xepc(p) /* other trap-related CSRs */ @@ -89,11 +89,11 @@ function clause is_CSR_defined(0x305) = true // mtvec function clause is_CSR_defined(0x341) = true // mepc function clause read_CSR(0x105) = get_stvec() -function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask() +function clause read_CSR(0x141) = get_xepc(Supervisor) function clause read_CSR(0x305) = get_mtvec() -function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask() +function clause read_CSR(0x341) = get_xepc(Machine) function clause write_CSR(0x105, value) = { set_stvec(value) } -function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) } +function clause write_CSR(0x141, value) = { set_xepc(Supervisor, value) } function clause write_CSR(0x305, value) = { set_mtvec(value) } -function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) } +function clause write_CSR(0x341, value) = { set_xepc(Machine, value) } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 5a70db00d..4e3e98bc4 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -445,16 +445,20 @@ register mepc : xlenbits /* The xepc legalization zeroes xepc[1:0] when misa.C is hardwired to 0. * When misa.C is writable, it zeroes only xepc[0]. */ -function legalize_xepc(v : xlenbits) -> xlenbits = - /* allow writing xepc[1] only if misa.C is enabled or could be enabled - XXX specification says this legalization should be done on read */ - if (sys_enable_writable_misa() & sys_enable_rvc()) | misa[C] == 0b1 +function legalize_xepc(v : xlenbits) -> xlenbits = { + // allow writing xepc[1] only if misa.C is enabled or could be enabled. + if sys_enable_rvc() then [v with 0 = bitzero] - else v & sign_extend(0b100) + else [v with 1..0 = zeros()] +} -/* masking for reads to xepc */ -function pc_alignment_mask() -> xlenbits = - ~(zero_extend(if misa[C] == 0b1 then 0b00 else 0b10)) +// Align value to min supported PC alignment. This is used to +// legalize xepc reads. +function align_pc(addr : xlenbits) -> xlenbits = { + if misa[C] == 0b1 + then [addr with 0 = bitzero] + else [addr with 1..0 = zeros()] +} /* auxiliary exception registers */