Add more detail to riscv execution trace log.

3 files changed, 32 insertions, 8 deletions

diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 1e17b0f2..c6786ff7 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -102,22 +102,31 @@ function clint_load(addr, width) = {
 val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
 function clint_store(addr, width, data) = {
   let addr = addr - plat_clint_base ();
-  print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
+    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
     mip->MSI() = data[0] == 0b1;
     MemValue(())
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
+    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */
     MemValue(())
-  } else MemException(E_SAMO_Access_Fault)
+  } else {
+    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
+    MemException(E_SAMO_Access_Fault)
+  }
 }
 
 val tick_clock : unit -> unit effect {rreg, wreg}
 function tick_clock() = {
   mcycle = mcycle + 1;
   mtime  = mtime  + 1;
-  if mtime >=_u mtimecmp
-  then mip->MTI() = true
+  mip->MTI() = false;
+  if mtimecmp <_u mtime & mtimecmp != EXTZ(0b0) then {
+    print(" firing clint timer at mtime " ^ BitStr(mtime));
+    mip->MTI() = true
+  };
+  if mtimecmp != EXTZ(0b0) & mtimecmp != EXTS(0b1) then
+    print(" mtime=" ^ BitStr(mtime) ^ "  mtimecmp=" ^ BitStr(mtimecmp));
 }
 
 /* Basic terminal character I/O. */
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 73343029..31acaf10 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -60,7 +60,7 @@ function step() = {
         F_RVC(h) => {
           match decodeCompressed(h) {
             None() => {
-              print("[" ^ string_of_int(step_no) ^ "] " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
+              print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
               handle_decode_exception(EXTZ(h));
               false
             },
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 928b6c5c..ab1afe87 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -714,15 +714,30 @@ function curInterrupt(pend : Minterrupts, enbl : Minterrupts, delg : Minterrupts
     if (mstatus.MIE() == true) & (eff_mip != EXTZ(0b0))
     then match findPendingInterrupt(eff_mip) {
            Some(i) => let r = (i, Machine) in Some(r),
-           None()  => None()
+           None()  => { print("mstatus.MIE and eff_mip=" ^ BitStr(eff_mip) ^ ", but nothing pending");
+                        None() }
          }
     else if (mstatus.SIE() == true) & (eff_sip != EXTZ(0b0))
             & (cur_privilege == Supervisor | cur_privilege == User)
     then match findPendingInterrupt(eff_sip) {
            Some(i) => let r = (i, Supervisor) in Some(r),
-           None()  => None()
+           None()  => { print("mstatus.SIE and eff_sip=" ^ BitStr(eff_sip) ^ ", but nothing pending");
+                        None() }
          }
-    else None()
+    else {
+      let p = if pend.MTI() == true then "1" else "0";
+      let e = if enbl.MTI() == true then "1" else "0";
+      let d = if delg.MTI() == true then "1" else "0";
+      print(" MTI: pend=" ^ p ^ " enbl=" ^ e ^ " delg=" ^ d);
+      let eff_mip = en_mip & (~ (delg.bits())); /* retained at M-mode */
+      let eff_sip = en_mip & delg.bits();       /* delegated to S-mode */
+      print("mstatus=" ^ BitStr(mstatus.bits())
+            ^ " mie,sie=" ^ BitStr(mstatus.MIE()) ^ "," ^ BitStr(mstatus.SIE())
+            ^ " en_mip=" ^ BitStr(en_mip)
+            ^ " eff_mip=" ^ BitStr(eff_mip)
+            ^ " eff_sip=" ^ BitStr(eff_sip));
+      None()
+    }
   }
 }