implemented bool for writing to destination register into the rvfi ou…

…tput
CTSRD-CHERI · Dec 13, 2024 · 1b067f8 · 1b067f8
1 parent c93d5ef
commit 1b067f8
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git 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
@@ -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,17 +141,21 @@ 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));
   }
 }
 
 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 () = {