Skip to content

Commit 224f26a

Browse files
committed
Simplify getPendingSet
Since the N extension has been removed, getPendingSet can be greatly simplified. This is functionally the same as the previous code but a lot shorter and easier to understand. Fixes riscv#616
1 parent 5f4a8e6 commit 224f26a

File tree

1 file changed

+14
-54
lines changed

1 file changed

+14
-54
lines changed

model/riscv_sys_control.sail

+14-54
Original file line numberDiff line numberDiff line change
@@ -120,65 +120,25 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
120120
else None()
121121
}
122122

123-
/* Process the pending interrupts xip at a privilege according to
124-
* the enabled flags xie and the delegation in xideleg. Return
125-
* either the set of pending interrupts, or the set of interrupts
126-
* delegated to the next lower privilege.
127-
*/
128-
union interrupt_set = {
129-
Ints_Pending : xlenbits,
130-
Ints_Delegated : xlenbits,
131-
Ints_Empty : unit
132-
}
133-
function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits,
134-
priv_enabled : bool) -> interrupt_set = {
135-
/* interrupts that are enabled but not delegated are pending */
136-
let effective_pend = xip.bits & xie.bits & ~(xideleg);
137-
/* the others are delegated */
138-
let effective_delg = xip.bits & xideleg;
139-
/* we have pending interrupts if this privilege is enabled */
140-
if priv_enabled & (effective_pend != zeros())
141-
then Ints_Pending(effective_pend)
142-
else if effective_delg != zeros()
143-
then Ints_Delegated(effective_delg)
144-
else Ints_Empty()
145-
}
146-
147-
/* Given the current privilege level, iterate over privileges to get a
148-
* pending set for an enabled privilege.
123+
/* Given the current privilege level, return the pending set
124+
* of interrupts for the highest privilege that has any pending.
149125
*
150126
* We don't use the lowered views of {xie,xip} here, since the spec
151127
* allows for example the M_Timer to be delegated to the S-mode.
152128
*/
153129
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
154-
let effective_pending = mip.bits & mie.bits;
155-
if effective_pending == zeros() then None() /* fast path */
156-
else {
157-
/* Higher privileges than the current one are implicitly enabled,
158-
* while lower privileges are blocked. An unsupported privilege is
159-
* considered blocked.
160-
*/
161-
let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1);
162-
let sIE = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
163-
match processPending(mip, mie, mideleg.bits, mIE) {
164-
Ints_Empty() => None(),
165-
Ints_Pending(p) => Some((p, Machine)),
166-
Ints_Delegated(d) => {
167-
if not(extensionEnabled(Ext_S)) then {
168-
// Can't delegate to user mode. This code is unreachable because
169-
// `mideleg.bits` is 0 without supervisor mode.
170-
internal_error(__FILE__, __LINE__, "N extension not supported");
171-
} else {
172-
/* the delegated bits are pending for S-mode */
173-
match processPending(Mk_Minterrupts(d), mie, zeros(), sIE) {
174-
Ints_Empty() => None(),
175-
Ints_Pending(p) => Some((p, Supervisor)),
176-
Ints_Delegated(d) => internal_error(__FILE__, __LINE__, "N extension not supported"),
177-
}
178-
}
179-
}
180-
}
181-
}
130+
// mideleg can only be non-zero if we support Supervisor mode.
131+
assert(extensionEnabled(Ext_S) | mideleg.bits == zeros());
132+
133+
let pending_m = mip.bits & mie.bits & ~(mideleg);
134+
let pending_s = mip.bits & mie.bits & mideleg;
135+
136+
let mIE = (priv == Machine & mstatus[MIE] == 0b1) | priv == Supervisor | priv == User;
137+
let sIE = (priv == Supervisor & mstatus[SIE] == 0b1) | priv == User;
138+
139+
if mIE & (pending_m != zeros()) then Some((pending_m, Machine))
140+
else if sIE & (pending_s != zeros()) then Some((pending_s, Supervisor))
141+
else None()
182142
}
183143

184144
/* Examine the current interrupt state and return an interrupt to be *

0 commit comments

Comments
 (0)