RISC-V: factor the execution trace.

This is now split into instructions, regs, memory and platform, each
controlled individually.  Currently all are enabled and not connected to
any command-line options, so a recompile is needed for trace tuning.

12 files changed, 126 insertions, 54 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index f2e9f7b6..bdd5bd04 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -58,6 +58,33 @@ let config_enable_dirty_update = ref false
 let config_enable_misaligned_access = ref false
 let config_mtval_has_illegal_inst_bits = ref false
 
+(* logging *)
+
+let config_print_instr       = ref true
+let config_print_reg         = ref true
+let config_print_mem_access  = ref true
+let config_print_platform    = ref true
+
+let print_instr s =
+  if !config_print_instr
+  then print_endline s
+  else ()
+
+let print_reg s =
+  if !config_print_reg
+  then print_endline s
+  else ()
+
+let print_mem_access s =
+  if !config_print_mem_access
+  then print_endline s
+  else ()
+
+let print_platform s =
+  if !config_print_platform
+  then print_endline s
+  else ()
+
 (* Mapping to Sail externs *)
 
 let bits_of_int i =
@@ -74,9 +101,9 @@ let make_rom start_pc =
   ( rom_size_ref := List.length rom;
     (*
     List.iteri (fun i c ->
-                Printf.eprintf "rom[0x%Lx] <- %x\n"
-                               (Int64.add P.rom_base (Int64.of_int i))
-                               c
+                print_mem_access "rom[0x%Lx] <- %x\n"
+                                 (Int64.add P.rom_base (Int64.of_int i))
+                                 c
                ) rom;
      *)
     rom )
@@ -104,15 +131,15 @@ let insns_per_tick () = Big_int.of_int P.insns_per_tick
 let reservation = ref "none"  (* shouldn't match any valid address *)
 
 let load_reservation addr =
-  Printf.eprintf "reservation <- %s\n" (string_of_bits addr);
+  print_platform (Printf.sprintf "reservation <- %s\n" (string_of_bits addr));
   reservation := string_of_bits addr
 
 let match_reservation addr =
-  Printf.eprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr);
+  print_platform (Printf.sprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr));
   string_of_bits addr = !reservation
 
 let cancel_reservation () =
-  Printf.eprintf "reservation <- none\n";
+  print_platform (Printf.sprintf "reservation <- none\n");
   reservation := "none"
 
 (* terminal I/O *)
@@ -129,8 +156,8 @@ let term_read () =
 let init elf_file =
   Elf.load_elf elf_file;
 
-  Printf.eprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ()));
-  Printf.eprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size;
+  print_platform (Printf.sprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ())));
+  print_platform (Printf.sprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size);
 
   let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in
   let rom = make_rom start_pc in
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 24913719..a2117bec 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -845,8 +845,6 @@ function cast_unit_vec b = match b {
   bitone  => 0b1
 }
 
-val print = "print_endline" : string -> unit
-
 val putchar = "putchar" : forall ('a : Type). 'a -> unit
 
 val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string
@@ -1057,10 +1055,16 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
 
 val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 
+val print = "print_endline" : string -> unit
 val print_int = "print_int" : (string, int) -> unit
 val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
 val print_string = "print_string" : (string, string) -> unit
 
+val print_instr    = {ocaml: "Platform.print_instr", c: "print_instr", _: "print_endline"} : string -> unit
+val print_reg      = {ocaml: "Platform.print_reg",   c: "print_reg", _: "print_endline"} : string -> unit
+val print_mem      = {ocaml: "Platform.print_mem_access", c: "print_mem_access", _: "print_endline"} : string -> unit
+val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", _: "print_endline"} : string -> unit
+
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 877251f4..c8fcdbab 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -1040,7 +1040,7 @@ function readCSR csr : csreg -> xlenbits =
     _     => { print_bits("unhandled read to CSR ", csr);
                0x0000_0000_0000_0000 }
   } in {
-    print("CSR " ^ csr ^ " -> " ^ BitStr(res));
+    print_reg("CSR " ^ csr ^ " -> " ^ BitStr(res));
     res
   }
 
@@ -1089,7 +1089,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     _     => None()
   } in
   match res {
-    Some(v) => print("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
+    Some(v) => print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
     None()  => print_bits("unhandled write to CSR ", csr)
   }
 
diff --git a/riscv/riscv_config.h b/riscv/riscv_config.h
new file mode 100644
index 00000000..f8f3eb30
--- /dev/null
+++ b/riscv/riscv_config.h
@@ -0,0 +1,7 @@
+#pragma once
+#include <stdbool.h>
+
+extern bool config_print_instr;
+extern bool config_print_reg;
+extern bool config_print_mem_access;
+extern bool config_print_platform;
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 37824ff4..3d380380 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -12,7 +12,7 @@ function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width
   match (t, __RISCV_read(addr, width, aq, rl, res)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
-    (_, Some(v))          => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+    (_, Some(v))          => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
                                MemValue(v) }
   }
 
@@ -116,7 +116,7 @@ function mem_write_ea (addr, width, aq, rl, con) = {
 
 // only used for actual memory regions, to avoid MMIO effects
 function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
-  print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   MemValue(__RISCV_write(addr, width, data))
 }
 
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 25b09bcd..c878f2a7 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -61,11 +61,11 @@ function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool
            & (addr + sizeof('n)) <=_u (rom_base + rom_size))
        then true
   else {
-    print("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
-    print("  plat_rom_base: " ^ BitStr(rom_base));
-    print("  plat_rom_size: " ^ BitStr(rom_size));
-    print("  plat_ram_base: " ^ BitStr(ram_base));
-    print("  plat_ram_size: " ^ BitStr(ram_size));
+    print_platform("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
+    print_platform("  plat_rom_base: " ^ BitStr(rom_base));
+    print_platform("  plat_rom_size: " ^ BitStr(rom_size));
+    print_platform("  plat_ram_base: " ^ BitStr(ram_base));
+    print_platform("  plat_ram_size: " ^ BitStr(ram_size));
     false
   }
 }
@@ -111,30 +111,30 @@ function clint_load(addr, width) = {
   /* FIXME: For now, only allow exact aligned access. */
   if addr == MSIP_BASE & ('n == 8 | 'n == 4)
   then {
-    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
+    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
     MemValue(zero_extend_type_hack(mip.MSI(), sizeof(8 * 'n)))
   }
   else if addr == MTIMECMP_BASE & ('n == 8)
   then {
-    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
+    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
     MemValue(zero_extend_type_hack(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */
   }
   else if addr == MTIME_BASE & ('n == 8)
   then {
-    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
     MemValue(zero_extend_type_hack(mtime, 64))
   }
   else {
-    print("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
+    print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
     MemException(E_Load_Access_Fault)
   }
 }
 
 function clint_dispatch() -> unit = {
-  print("clint::tick mtime <- " ^ BitStr(mtime));
+  print_platform("clint::tick mtime <- " ^ BitStr(mtime));
   mip->MTI() = false;
   if mtimecmp <=_u mtime then {
-    print(" clint timer pending at mtime " ^ BitStr(mtime));
+    print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
     mip->MTI() = true
   }
 }
@@ -144,17 +144,17 @@ val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryO
 function clint_store(addr, width, data) = {
   let addr = addr - plat_clint_base ();
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
-    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
+    print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
     mip->MSI() = data[0] == 0b1;
     clint_dispatch();
     MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
-    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
+    print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
     MemValue(true)
   } else {
-    print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
+    print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
     MemException(E_SAMO_Access_Fault)
   }
 }
@@ -191,7 +191,7 @@ register htif_exit_code : xlenbits
 
 val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
 function htif_load(addr, width) = {
-  print("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
+  print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
   /* FIXME: For now, only allow the expected access widths. */
   if width == 8
   then MemValue(zero_extend_type_hack(htif_tohost, 64))  /* FIXME: Redundant zero_extend currently required by Lem backend */
@@ -201,7 +201,7 @@ function htif_load(addr, width) = {
 /* The wreg effect is an artifact of using 'register' to implement device state. */
 val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wreg}
 function htif_store(addr, width, data) = {
-  print("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   /* Store the written value so that we can ack it later. */
   let cbits : xlenbits = EXTZ(data);
   htif_tohost = cbits;
@@ -209,7 +209,7 @@ function htif_store(addr, width, data) = {
   let cmd = Mk_htif_cmd(cbits);
   match cmd.device() {
     0x00 => { /* syscall-proxy */
-      print("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
+      print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
       if cmd.payload()[0] == 0b1
       then {
            htif_done = true;
@@ -218,7 +218,7 @@ function htif_store(addr, width, data) = {
       else ()
     },
     0x01 => { /* terminal */
-      print("htif-term cmd: " ^ BitStr(cmd.payload()));
+      print_platform("htif-term cmd: " ^ BitStr(cmd.payload()));
       match cmd.cmd() {
         0x00 => /* TODO: terminal input handling */ (),
         0x01 => plat_term_write(cmd.payload()[7..0]),
@@ -232,7 +232,7 @@ function htif_store(addr, width, data) = {
 
 val htif_tick : unit -> unit effect {rreg, wreg}
 function htif_tick() = {
-  print("htif::tick " ^ BitStr(htif_tohost));
+  print_platform("htif::tick " ^ BitStr(htif_tohost));
   htif_tohost = EXTZ(0b0)  /* htif ack */
 }
 
diff --git a/riscv/riscv_prelude.c b/riscv/riscv_prelude.c
index c8145df4..16219137 100644
--- a/riscv/riscv_prelude.c
+++ b/riscv/riscv_prelude.c
@@ -1,4 +1,5 @@
 #include "riscv_prelude.h"
+#include "riscv_config.h"
 
 unit print_string(sail_string prefix, sail_string msg)
 {
@@ -6,3 +7,26 @@ unit print_string(sail_string prefix, sail_string msg)
   return UNIT;
 }
 
+unit print_instr(sail_string s)
+{
+  if (config_print_instr) printf("%s\n", s);
+  return UNIT;
+}
+
+unit print_reg(sail_string s)
+{
+  if (config_print_reg) printf("%s\n", s);
+  return UNIT;
+}
+
+unit print_mem_access(sail_string s)
+{
+  if (config_print_mem_access) printf("%s\n", s);
+  return UNIT;
+}
+
+unit print_platform(sail_string s)
+{
+  if (config_print_platform) printf("%s\n", s);
+  return UNIT;
+}
diff --git a/riscv/riscv_prelude.h b/riscv/riscv_prelude.h
index 514022cd..a296c7e9 100644
--- a/riscv/riscv_prelude.h
+++ b/riscv/riscv_prelude.h
@@ -3,3 +3,8 @@
 #include "rts.h"
 
 unit print_string(sail_string prefix, sail_string msg);
+
+unit print_instr(sail_string s);
+unit print_reg(sail_string s);
+unit print_mem_access(sail_string s);
+unit print_platform(sail_string s);
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index f632a399..038c44b6 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -57,6 +57,11 @@ static int rvfi_dii_sock;
 unsigned char *spike_dtb = NULL;
 size_t spike_dtb_len = 0;
 
+bool config_print_instr = true;
+bool config_print_reg = true;
+bool config_print_mem_access = true;
+bool config_print_platform = true;
+
 static struct option options[] = {
   {"enable-dirty",                no_argument,       0, 'd'},
   {"enable-misaligned",           no_argument,       0, 'm'},
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 218be598..755420d9 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -62,13 +62,13 @@ function step(step_no) = {
           F_RVC(h) => {
             match decodeCompressed(h) {
               None() => {
-                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
+                print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
                 instbits = EXTZ(h);
                 handle_illegal();
                 (false, true)
               },
               Some(ast) => {
-                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+                print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
                 nextPC = PC + 2;
                 (execute(ast), true)
               }
@@ -77,13 +77,13 @@ function step(step_no) = {
           F_Base(w) => {
             match decode(w) {
               None() => {
-                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
+                print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
                 instbits = EXTZ(w);
                 handle_illegal();
                 (false, true)
               },
               Some(ast) => {
-                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+                print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
                 nextPC = PC + 4;
                 (execute(ast), true)
               }
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index d29a7690..58609949 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -845,14 +845,14 @@ function curInterrupt(priv : Privilege, pend : Minterrupts, enbl : Minterrupts,
       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);
+      print_platform(" 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));
+      print_platform("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()
     }
   }
@@ -893,7 +893,7 @@ $endif
 function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
                     -> xlenbits = {
   rvfi_trap();
-  print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
+  print_platform("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
 
   match (del_priv) {
     Machine => {
@@ -908,7 +908,7 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        cur_privilege   = del_priv;
 
-       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
+       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
 
        cancel_reservation();
 
@@ -933,7 +933,7 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        cur_privilege   = del_priv;
 
-       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
+       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
 
        cancel_reservation();
 
@@ -952,8 +952,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
   match (cur_priv, ctl) {
     (_, CTL_TRAP(e)) => {
       let del_priv = exception_delegatee(e.trap, cur_priv);
-      print("trapping from " ^ cur_priv ^ " to " ^ del_priv
-            ^ " to handle " ^ e.trap);
+      print_platform("trapping from " ^ cur_priv ^ " to " ^ del_priv
+                     ^ " to handle " ^ e.trap);
       handle_trap(del_priv, false, e.trap, pc, e.excinfo)
     },
     (_, CTL_MRET())  => {
@@ -963,8 +963,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = privLevel_of_bits(mstatus.MPP());
       mstatus->MPP()  = privLevel_to_bits(User);
 
-      print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
-      print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
+      print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
+      print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
 
       cancel_reservation();
       mepc & pc_alignment_mask()
@@ -976,8 +976,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
       mstatus->SPP()  = false;
 
-      print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
-      print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
+      print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
+      print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
 
       cancel_reservation();
       sepc & pc_alignment_mask()
@@ -1033,7 +1033,7 @@ function init_sys() -> unit = {
   minstret_written   = false;
 
   // log compatibility with spike
-  print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
+  print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
 }
 
 /* memory access exceptions, defined here for use by the platform model. */
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 7e29ef3c..4d012e0c 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -164,7 +164,7 @@ function wX (r, v) = {
   if (r != 0) then {
      rvfi_wX(r,v);
      // Xs[r] = v;
-     print("x" ^ string_of_int(r) ^ " <- " ^ BitStr(v));
+     print_reg("x" ^ string_of_int(r) ^ " <- " ^ BitStr(v));
   }
 }