From df646dec03bbc482e68c0908779bde4aa5d8cec5 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 6 Nov 2024 14:29:24 +0000 Subject: [PATCH] Fix delegated interrupt handling When the N extension was removed this code was accidentally broken because it doesn't respect mie for delegated interrupts any more. The `internal_error`s should be unreachable, at least for the sequential output. I believe formal backends may decide `mideleg` is going to be non-zero even without S, but I think that was an existing issue. --- model/riscv_sys_control.sail | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6379f5676..9384b8ef5 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -244,7 +244,20 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { match processPending(mip, mie, mideleg.bits, mIE) { Ints_Empty() => None(), Ints_Pending(p) => Some((p, Machine)), - Ints_Delegated(d) => if sIE then Some((d, Supervisor)) else None(), + Ints_Delegated(d) => { + if not(extensionEnabled(Ext_S)) then { + // Can't delegate to user mode. This code is unreachable because + // `mideleg.bits` is 0 without supervisor mode. + internal_error(__FILE__, __LINE__, "N extension not supported"); + } else { + /* the delegated bits are pending for S-mode */ + match processPending(Mk_Minterrupts(d), mie, zeros(), sIE) { + Ints_Empty() => None(), + Ints_Pending(p) => Some((p, Supervisor)), + Ints_Delegated(d) => internal_error(__FILE__, __LINE__, "N extension not supported"), + } + } + } } } }