From 1b067f884700d25f91192418ac79b6cbb4195815 Mon Sep 17 00:00:00 2001
From: Franz Fuchs <franz.fuchs@cl.cam.ac.uk>
Date: Mon, 31 Oct 2022 10:26:19 +0000
Subject: [PATCH] implemented bool for writing to destination register into the
 rvfi output

---
 src/cheri_insts.sail |  2 +-
 src/cheri_regs.sail  | 14 +++++++++-----
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail
index e093b64..9541837 100644
--- a/src/cheri_insts.sail
+++ b/src/cheri_insts.sail
@@ -707,7 +707,7 @@ function clause execute (CClear(q, m)) = {
       if q_u == 0 & i == 0 then
         DDC = null_cap
       else
-        C(8 * q_u + i) = null_cap;
+        wC (false, 8 * q_u + i, null_cap);
   RETIRE_SUCCESS
 }
 
diff --git a/src/cheri_regs.sail b/src/cheri_regs.sail
index 17d3a7c..eb063be 100644
--- a/src/cheri_regs.sail
+++ b/src/cheri_regs.sail
@@ -103,8 +103,8 @@ function rC r = {
 }
 
 /* writes a register with a capability value */
-val wC : forall 'n, 0 <= 'n < 32. (regno('n), regtype) -> unit effect {wreg, escape}
-function wC (r, v) = {
+val wC : forall 'n, 0 <= 'n < 32. (bool, regno('n), regtype) -> unit effect {wreg, escape}
+function wC (b, r, v) = {
   match r {
     0  => (),
     1  => x1 = v,
@@ -141,7 +141,8 @@ function wC (r, v) = {
     _  => internal_error(__FILE__, __LINE__, "Invalid capability register")
   };
   if (r != 0) then {
-     rvfi_wX(r, v.address);
+     if b then
+       rvfi_wX(r, v.address);
      if get_config_print_reg() then
        print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
   }
@@ -149,9 +150,12 @@ function wC (r, v) = {
 
 function rC_bits(r: bits(5)) -> regtype = rC(unsigned(r))
 
-function wC_bits(r: bits(5), v: regtype) -> unit = wC(unsigned(r), v)
+function wC_bits(r: bits(5), v: regtype) -> unit = wC (true, unsigned(r), v)
 
-overload C = {rC_bits, wC_bits, rC, wC}
+val wC_rvfi : forall 'n, 0 <= 'n < 32. (regno('n), regtype) -> unit effect {wreg, escape}
+function wC_rvfi (r, v) = wC (true, r, v)
+
+overload C = {rC_bits, wC_bits, rC, wC_rvfi}
 
 val ext_init_regs : unit -> unit effect {wreg}
 function ext_init_regs () = {