Fix riscv interrupt pending check to handle implicit enabling at lower privileges.

Also fix timer threshold comparison to be <= instead of <.

3 files changed, 14 insertions, 14 deletions

diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 55df7c5c..bfeff01d 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -105,12 +105,10 @@ function clint_load(addr, width) = {
 function clint_dispatch() -> unit = {
   print("clint::tick mtime <- " ^ BitStr(mtime));
   mip->MTI() = false;
-  if mtimecmp <_u mtime & mtimecmp != EXTZ(0b0) then {
-    print(" firing clint timer at mtime " ^ BitStr(mtime));
+  if mtimecmp <=_u mtime then {
+    print(" clint timer pending at mtime " ^ BitStr(mtime));
     mip->MTI() = true
-  };
-  if mtimecmp != EXTZ(0b0) & mtimecmp != EXTS(0b1) then
-    print(" mtime=" ^ BitStr(mtime) ^ "  mtimecmp=" ^ BitStr(mtimecmp));
+  }
 }
 
 /* The rreg effect is due to checking mtime. */
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index fe9d7e84..49f8e51c 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -44,7 +44,7 @@ function fetch() -> FetchResult = {
 /* returns whether an instruction was retired */
 val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 function step(step_no) = {
-  match curInterrupt(mip, mie, mideleg) {
+  match curInterrupt(cur_privilege, mip, mie, mideleg) {
     Some(intr, priv) => {
       print_bits("Handling interrupt: ", intr);
       handle_interrupt(intr, priv);
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 2beedded..bb3d13db 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -711,25 +711,27 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
  *
  * For now, it assumes 'S' and no 'N' extension, which is the common case.
  */
-function curInterrupt(pend : Minterrupts, enbl : Minterrupts, delg : Minterrupts)
+function curInterrupt(priv : Privilege, pend : Minterrupts, enbl : Minterrupts, delg : Minterrupts)
                      -> option((InterruptType, Privilege)) = {
   let en_mip : xlenbits = pend.bits() & enbl.bits();
   if en_mip == EXTZ(0b0) then None() /* fast path */
   else {
+    /* check implicit enabling when in lower privileges */
+    let eff_mie = priv != Machine | (priv == Machine & mstatus.MIE() == true);
+    let eff_sie = priv == User | (priv == Supervisor & mstatus.SIE() == true);
+    /* handle delegation */
     let eff_mip = en_mip & (~ (delg.bits())); /* retained at M-mode */
     let eff_sip = en_mip & delg.bits();       /* delegated to S-mode */
-    if (mstatus.MIE() == true) & (eff_mip != EXTZ(0b0))
+
+    if eff_mie & eff_mip != EXTZ(0b0)
     then match findPendingInterrupt(eff_mip) {
            Some(i) => let r = (i, Machine) in Some(r),
-           None()  => { print("mstatus.MIE and eff_mip=" ^ BitStr(eff_mip) ^ ", but nothing pending");
-                        None() }
+           None()  => { internal_error("non-zero eff_mip=" ^ BitStr(eff_mip) ^ ", but nothing pending") }
          }
-    else if (mstatus.SIE() == true) & (eff_sip != EXTZ(0b0))
-            & (cur_privilege == Supervisor | cur_privilege == User)
+    else if eff_sie & eff_sip != EXTZ(0b0)
     then match findPendingInterrupt(eff_sip) {
            Some(i) => let r = (i, Supervisor) in Some(r),
-           None()  => { print("mstatus.SIE and eff_sip=" ^ BitStr(eff_sip) ^ ", but nothing pending");
-                        None() }
+           None()  => { internal_error("non-zero eff_sip=" ^ BitStr(eff_sip) ^ ", but nothing pending") }
          }
     else {
       let p = if pend.MTI() == true then "1" else "0";