From 1145294ece56f687410d2a9fe087ff69375edeb2 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 25 Jun 2018 16:22:52 +0100
Subject: mips: add optional tracing of register writes (commented out).

---
 mips/mips_prelude.sail | 8 ++++++--
 mips/prelude.sail      | 1 +
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 7ec4fdfe..fbbe74ee 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -327,8 +327,12 @@ function rGPR idx = {
 /* Write numbered GP reg. (writes to r0 ignored) */
 val wGPR : (bits(5), bits(64)) -> unit effect {wreg}
 function wGPR (idx, v) = {
-         let i as atom(_) = unsigned(idx) in
-         if i == 0 then () else GPR[i] = v
+  let i as atom(_) = unsigned(idx) in
+  if i != 0 then {
+    /*prerr_string(string_of_int(i));
+    prerr_bits(" <- ", v);*/
+    GPR[i] = v;
+  };
 }
 
 val MEMr = {lem: "MEMr"} : forall 'n, 'n >= 0.
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 76638c68..6821469e 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -51,6 +51,7 @@ val print = "print_endline" : string -> unit
 
 val "prerr_endline" : string -> unit
 
+val "prerr_string" : string -> unit
 
 val putchar = {c:"sail_putchar", _:"putchar"} : forall ('a : Type). 'a -> unit
 
-- 
cgit v1.2.3