Skip to content

Commit

Permalink
Fix delegated interrupt handling
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Timmmm committed Nov 6, 2024
1 parent b8d1fa5 commit df646de
Showing 1 changed file with 14 additions and 1 deletion.
15 changes: 14 additions & 1 deletion model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
}
}
}
}
}
}
Expand Down

0 comments on commit df646de

Please sign in to comment.