Merge branch 'master' into gdbgdb

1 files changed, 19 insertions, 2 deletions

diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 9ff83b3..d9674f7 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -10,5 +10,22 @@ This function is called after above when running rvfi and allows the model
 to be initialised differently (e.g. CHERI cap regs are initialised
 to omnipotent instead of null).
  */
-val ext_rvfi_init : unit -> unit effect {wreg}
-function ext_rvfi_init () = ()
+val ext_rvfi_init : unit -> unit effect {rreg, wreg}
+function ext_rvfi_init () = {
+  x1 = x1 // to avoid hook being optimized out
+}
+
+
+/*!
+THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
+at Privilege level priv. It should return true if the access is allowed.
+*/
+val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+function ext_check_CSR (csrno, p, isWrite) = true
+
+/*!
+THIS is called if ext_check_CSR returns false. It should
+cause an appropriate RISCV exception.
+ */
+val ext_check_CSR_fail : unit->unit
+function ext_check_CSR_fail () = ()