diff --git a/Makefile b/Makefile
index 268e36b9b..1a434aa5d 100644
--- a/Makefile
+++ b/Makefile
@@ -267,11 +267,11 @@ c_preserve_fns=-c_preserve _set_Misa_C
 
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c
-	$(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
+	$(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_default_callbacks.c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
 
 generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c2
-	$(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 $(SAIL_SRCS) -o $(basename $@)
+	$(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 -c_include riscv_default_callbacks.c $(SAIL_SRCS) -o $(basename $@)
 
 $(SOFTFLOAT_LIBS):
 	$(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR)
@@ -299,6 +299,10 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
   -c_preserve rvfi_get_int_data \
   -c_preserve rvfi_zero_exec_packet \
   -c_preserve rvfi_halt_exec_packet \
+  -c_preserve rvfi_write \
+  -c_preserve rvfi_read \
+  -c_preserve rvfi_mem_exception \
+  -c_preserve rvfi_wX \
   -c_preserve print_rvfi_exec \
   -c_preserve print_instr_packet \
   -c_preserve print_rvfi_exec
@@ -306,7 +310,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c
-	$(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
+	$(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) -c_include riscv_rvfi_callbacks.c model/main.sail -o $(basename $@)
 	sed -e '/^[[:space:]]*$$/d' $@ > $@.new
 	mv $@.new $@
 
diff --git a/c_emulator/riscv_config.h b/c_emulator/riscv_config.h
index f8f3eb30d..285ff0421 100644
--- a/c_emulator/riscv_config.h
+++ b/c_emulator/riscv_config.h
@@ -5,3 +5,4 @@ extern bool config_print_instr;
 extern bool config_print_reg;
 extern bool config_print_mem_access;
 extern bool config_print_platform;
+extern bool rv_enable_callbacks;
diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c
new file mode 100644
index 000000000..fd7fa3e84
--- /dev/null
+++ b/c_emulator/riscv_default_callbacks.c
@@ -0,0 +1,11 @@
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { }
+int xreg_write_callback(unsigned reg, uint64_t value) { }
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }
diff --git a/c_emulator/riscv_rvfi_callbacks.c b/c_emulator/riscv_rvfi_callbacks.c
new file mode 100644
index 000000000..77cd37e8e
--- /dev/null
+++ b/c_emulator/riscv_rvfi_callbacks.c
@@ -0,0 +1,37 @@
+#include "riscv_config.h"
+
+int zrvfi_write(uint64_t addr, int64_t width, lbits value);
+int zrvfi_read(uint64_t addr, sail_int width, lbits value);
+int zrvfi_mem_exception(uint64_t addr);
+int zrvfi_wX(int64_t reg, uint64_t value);
+
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value)
+{
+  if (rv_enable_callbacks)
+    zrvfi_write(addr, width, value);
+}
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value)
+{
+  if (rv_enable_callbacks) {
+    sail_int len;
+    CREATE(sail_int)(&len);
+    CONVERT_OF(sail_int, mach_int)(&len, width);
+    zrvfi_read(addr, len, value);
+    KILL(sail_int)(&len);
+  }
+}
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception)
+{
+  if (rv_enable_callbacks)
+    zrvfi_mem_exception(addr);
+}
+int xreg_write_callback(unsigned reg, uint64_t value)
+{
+  if (rv_enable_callbacks)
+    zrvfi_wX(reg, value);
+}
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }
diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h
index da29c2ba9..e7247fc58 100644
--- a/c_emulator/riscv_sail.h
+++ b/c_emulator/riscv_sail.h
@@ -50,6 +50,20 @@ extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
 extern bool have_exception;
 
+/* Callbacks for state-changing events */
+
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception);
+int xreg_write_callback(unsigned reg, uint64_t value);
+int freg_write_callback(unsigned reg, uint64_t value);
+int csr_write_callback(unsigned reg, uint64_t value);
+int csr_read_callback(unsigned reg, uint64_t value);
+int vreg_write_callback(unsigned reg, lbits value);
+int pc_write_callback(uint64_t value);
+
 /* machine state */
 
 extern uint32_t zcur_privilege;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 913543144..dccb57775 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -89,6 +89,7 @@ bool config_print_reg = true;
 bool config_print_mem_access = true;
 bool config_print_platform = true;
 bool config_print_rvfi = false;
+bool rv_enable_callbacks = true;
 
 void set_config_print(char *var, bool val)
 {
@@ -98,6 +99,7 @@ void set_config_print(char *var, bool val)
     config_print_reg = val;
     config_print_platform = val;
     config_print_rvfi = val;
+    rv_enable_callbacks = val;
   } else if (strcmp("instr", var) == 0) {
     config_print_instr = val;
   } else if (strcmp("reg", var) == 0) {
diff --git a/model/prelude.sail b/model/prelude.sail
index 45d49c0ed..e44326e40 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -71,18 +71,15 @@ val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
 
 val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
 val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
 val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
 val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
 val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
 
 val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
-function get_config_print_reg () = false
 function get_config_print_mem () = false
 function get_config_print_platform () = false
 
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index 63652da88..de6118b75 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -193,11 +193,8 @@ function wF (r : regno, in_v : flenbits) -> unit = {
   };
 
   dirty_fd_context();
-
-  if   get_config_print_reg()
-  then
-      /* TODO: will only print bits; should we print in floating point format? */
-      print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
+  
+  freg_write_callback(regno_to_regidx(r), in_v);
 }
 
 function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index 9ffb56eff..bf8b63591 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -154,7 +154,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
               if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
               else {
                 vl = to_bits(sizeof(xlen), i);
-                print_reg("CSR vl <- " ^ BitStr(vl));
+                csr_write_callback(csr_name_map("vl"), vl);
                 trimmed = true
               }
             },
@@ -163,7 +163,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                 if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
                 else {
                   vl = to_bits(sizeof(xlen), i);
-                  print_reg("CSR vl <- " ^ BitStr(vl));
+                  csr_write_callback(csr_name_map("vl"), vl);
                   trimmed = true
                 }
               } else match translateAddr(vaddr, Read(Data)) {
@@ -171,7 +171,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                   if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
                   else {
                     vl = to_bits(sizeof(xlen), i);
-                    print_reg("CSR vl <- " ^ BitStr(vl));
+                    csr_write_callback(csr_name_map("vl"), vl);
                     trimmed = true
                   }
                 },
@@ -182,7 +182,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                       if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
                       else {
                         vl = to_bits(sizeof(xlen), i);
-                        print_reg("CSR vl <- " ^ BitStr(vl));
+                        csr_write_callback(csr_name_map("vl"), vl);
                         trimmed = true
                       }
                     }
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index 16adf2806..774f27522 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -51,8 +51,8 @@ function handle_illegal_vtype() = {
    */
   vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
   vl = zeros();
-  print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
-  print_reg("CSR vl <- " ^ BitStr(vl))
+  csr_write_callback(csr_name_map("vtype"), vtype.bits);
+  csr_write_callback(csr_name_map("vl"), vl);
 }
 
 val calculate_new_vl : (int, int) -> xlenbits
@@ -106,9 +106,9 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
   /* reset vstart to 0 */
   vstart = zeros();
 
-  print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
-  print_reg("CSR vl <- " ^ BitStr(vl));
-  print_reg("CSR vstart <- " ^ BitStr(vstart));
+  csr_write_callback(csr_name_map("vtype"), vtype.bits);
+  csr_write_callback(csr_name_map("vl"), vl);
+  csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
   RETIRE_SUCCESS
 }
@@ -157,9 +157,9 @@ function clause execute VSETVL(rs2, rs1, rd) = {
   /* reset vstart to 0 */
   vstart = zeros();
 
-  print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
-  print_reg("CSR vl <- " ^ BitStr(vl));
-  print_reg("CSR vstart <- " ^ BitStr(vstart));
+  csr_write_callback(csr_name_map("vtype"), vtype.bits);
+  csr_write_callback(csr_name_map("vl"), vl);
+  csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
   RETIRE_SUCCESS
 }
@@ -193,9 +193,9 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
   /* reset vstart to 0 */
   vstart = zeros();
 
-  print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
-  print_reg("CSR vl <- " ^ BitStr(vl));
-  print_reg("CSR vstart <- " ^ BitStr(vstart));
+  csr_write_callback(csr_name_map("vtype"), vtype.bits);
+  csr_write_callback(csr_name_map("vl"), vl);
+  csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index f2980fb9e..4334df551 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -107,8 +107,7 @@ function readCSR csr : csreg -> xlenbits = {
                                     zero_extend(0x0) }
                    }
   };
-  if   get_config_print_reg()
-  then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
+  csr_read_callback(csr, res);
   res
 }
 
@@ -185,8 +184,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     _           => ext_write_CSR(csr, value)
   };
   match res {
-    Some(v) => if   get_config_print_reg()
-               then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
+    Some(v) => csr_write_callback(csr, v),
     None()  => print_bits("unhandled write to CSR ", csr)
   }
 }
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 82227ad7e..3468ce702 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -117,25 +117,6 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
-$ifdef RVFI_DII
-val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
-function rvfi_read (addr, width, result) = {
-  rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
-  rvfi_mem_data_present = true;
-  match result {
-    /* TODO: report tag bit for capability writes and extend mask by one bit. */
-    MemValue(v, _) => if width <= 16
-                       then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256);
-                              rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) }
-                       else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") },
-    MemException(_) => ()
-  };
-}
-$else
-val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
-function rvfi_read (addr, width, result) = ()
-$endif
-
 val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
 val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
 val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
@@ -151,7 +132,10 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = {
       (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
       (_, _, _)             => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta)
     };
-  rvfi_read(paddr, width, result);
+  match result {
+    MemValue(value, _) => mem_read_callback(paddr, width, value),
+    MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e))
+  };
   result
 }
 
@@ -172,28 +156,6 @@ function mem_write_ea (addr, width, aq, rl, con) =
   then MemException(E_SAMO_Addr_Align())
   else MemValue(write_ram_ea(write_kind_of_flags(aq, rl, con), addr, width))
 
-$ifdef RVFI_DII
-val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
-function rvfi_write (addr, width, value, meta, result) = {
-  rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
-  rvfi_mem_data_present = true;
-  match result {
-    /* Log only the memory address (without the value) if the write fails. */
-    MemValue(_) => if width <= 16 then {
-        /* TODO: report tag bit for capability writes and extend mask by one bit. */
-        rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256);
-        rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width);
-      } else {
-        internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!");
-      },
-    MemException(_) => ()
-  }
-}
-$else
-val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
-function rvfi_write (addr, width, value, meta, result) = ()
-$endif
-
 // only used for actual memory regions, to avoid MMIO effects
 function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
   let result = MemValue(write_ram(wk, paddr, width, data, meta));
@@ -243,7 +205,10 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl
   then MemException(E_SAMO_Addr_Align())
   else {
     let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con);
-    rvfi_write(paddr, width, value, meta, result);
+    match result {
+      MemValue(_) => mem_write_callback(paddr, width, value),
+      MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e))
+    };
     result
   }
 }
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
index a17e86d32..f69266328 100644
--- a/model/riscv_pc_access.sail
+++ b/model/riscv_pc_access.sail
@@ -28,5 +28,6 @@ function set_next_pc(pc) = {
 
 val tick_pc : unit -> unit
 function tick_pc() = {
+  pc_write_callback(PC);
   PC = nextPC
 }
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index 26faef210..6d18e468e 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -88,16 +88,6 @@ function rX (r : regno) -> xlenbits = {
   regval_from_reg(v)
 }
 
-$ifdef RVFI_DII
-function rvfi_wX (r : regno, v : xlenbits) -> unit = {
-  rvfi_int_data[rvfi_rd_wdata] = zero_extend(v);
-  rvfi_int_data[rvfi_rd_addr] = to_bits(8,r);
-  rvfi_int_data_present = true;
-}
-$else
-function rvfi_wX (r : regno, v : xlenbits) -> unit = ()
-$endif
-
 function wX (r : regno, in_v : xlenbits) -> unit = {
   let v = regval_into_reg(in_v);
   match r {
@@ -136,9 +126,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = {
     _  => assert(false, "invalid register number")
   };
   if (r != 0) then {
-     rvfi_wX(r, in_v);
-     if   get_config_print_reg()
-     then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
+    xreg_write_callback(regno_to_regidx(r), in_v);
   }
 }
 
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 4f7b3540b..ece9b1d3c 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -340,8 +340,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       if   get_config_print_reg()
-       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+       csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
 
        prepare_trap_vector(del_priv, mcause)
     },
@@ -365,8 +364,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       if   get_config_print_reg()
-       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+       csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
 
        prepare_trap_vector(del_priv, scause)
     },
@@ -385,8 +383,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       if   get_config_print_reg()
-       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+       csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
 
        prepare_trap_vector(del_priv, ucause)
     }
@@ -412,8 +409,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   cur_privilege != Machine
       then mstatus[MPRV] = 0b0;
 
-      if   get_config_print_reg()
-      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+      csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
@@ -428,8 +424,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   cur_privilege != Machine
       then mstatus[MPRV] = 0b0;
 
-      if   get_config_print_reg()
-      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+      csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv)
                           ^ " to " ^ to_str(cur_privilege));
@@ -442,8 +437,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       mstatus[UPIE] = 0b1;
       cur_privilege   = User;
 
-      if   get_config_print_reg()
-      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
+      csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
@@ -550,9 +544,7 @@ function init_sys() -> unit = {
   // PMP's L and A fields are set to 0 on reset.
   init_pmp();
 
-  // log compatibility with spike
-  if   get_config_print_reg()
-  then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")")
+  csr_write_callback(csr_name_map("mstatus"), mstatus.bits);
 }
 
 /* memory access exceptions, defined here for use by the platform model. */
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 166aee072..58178ae3a 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -43,6 +43,8 @@ type regno = range(0, 31)
 
 function regidx_to_regno (b : regidx) -> regno = unsigned(b)
 
+function regno_to_regidx (b : regno) -> regidx = to_bits(5, b)
+
 /* mapping RVC register indices into normal indices */
 val creg2reg_idx : cregidx -> regidx
 function creg2reg_idx(creg) = 0b01 @ creg
@@ -408,3 +410,16 @@ function report_invalid_width(f , l, w, k) -> 'a = {
   internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
      " with xlen=" ^ dec_str(sizeof(xlen)))
 }
+
+/* Callbacks for state-changing events */
+
+/* Defaults for these functions in riscv_default_callbacks.c and platform_impl.ml */
+
+val mem_write_callback = pure {ocaml: "Platform.mem_write_callback", c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+val mem_exception_callback = pure {ocaml: "Platform.mem_exception_callback", c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ xlenbits, /* num_of_ExceptionType */ int('n)) -> unit
+val pc_write_callback = pure {ocaml: "Platform.pc_write_callback", c: "pc_write_callback"} : xlenbits -> unit
+val xreg_write_callback = pure {ocaml: "Platform.xreg_write_callback", c: "xreg_write_callback"} : (regidx, xlenbits) -> unit
+val freg_write_callback = pure {ocaml: "Platform.freg_write_callback", c: "freg_write_callback"} : (regidx, flenbits) -> unit
+val csr_write_callback = pure {ocaml: "Platform.csr_write_callback", c: "csr_write_callback"} : (csreg, xlenbits) -> unit
+val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (csreg, xlenbits) -> unit
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 8d96f12a0..60198d4ae 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -169,8 +169,7 @@ function wV (r : regno, in_v : vregtype) -> unit = {
 
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < VLEN & VLEN <= sizeof(vlenmax));
-  if   get_config_print_reg()
-  then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
+  vreg_write_callback(regno_to_regidx(r), v);
 }
 
 function rV_bits(i: regidx) -> vregtype = rV(unsigned(i))
diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail
index 2ab211b8c..5ab69305a 100755
--- a/model/riscv_vreg_type.sail
+++ b/model/riscv_vreg_type.sail
@@ -146,3 +146,8 @@ enum fwffunct6    = { FWF_VADD, FWF_VSUB }
 enum fvfmfunct6   = { VFM_VMFEQ, VFM_VMFLE, VFM_VMFLT, VFM_VMFNE, VFM_VMFGT, VFM_VMFGE }
 
 enum vmlsop       = { VLM, VSM }
+
+/* Callbacks for vregs state-changing events */
+
+/* Default for this function in riscv_default_callbacks.c and platform_impl.ml */
+val vreg_write_callback = pure {ocaml: "Platform.vreg_write_callback", c: "vreg_write_callback"} : (regidx, vregtype) -> unit
diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail
index d1ad480df..99b88a70e 100644
--- a/model/rvfi_dii.sail
+++ b/model/rvfi_dii.sail
@@ -325,3 +325,47 @@ function print_rvfi_exec () = {
   print_bits("rvfi_pc_rdata : ", rvfi_pc_data[rvfi_pc_rdata]);
   print_bits("rvfi_order    : ", rvfi_inst_data[rvfi_order]);
 }
+
+/* RVFI records */
+
+val internal_error : forall ('a : Type). (string, int, string) -> 'a
+
+val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n)) -> unit
+function rvfi_write (addr, width, value) = {
+  rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
+  rvfi_mem_data_present = true;
+  if width <= 16 then {
+    /* TODO: report tag bit for capability writes and extend mask by one bit. */
+    rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value, 256);
+    rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width);
+  } else {
+    internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!");
+  };
+}
+
+val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> unit
+function rvfi_read (addr, width, value) = {
+  rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
+  rvfi_mem_data_present = true;
+  if width <= 16 then {
+    /* TODO: report tag bit for capability writes and extend mask by one bit. */
+    rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(value, 256);
+    rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width)
+  } else {
+    internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!")
+  };
+}
+
+val rvfi_mem_exception : xlenbits -> unit
+function rvfi_mem_exception (addr) = {
+  /* Log only the memory address (without the value) if the write fails. */
+  rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
+  rvfi_mem_data_present = true;
+}
+
+val rvfi_wX : forall 'n, 0 <= 'n < 32. (int('n), xlenbits) -> unit
+function rvfi_wX (r,v) = {
+  rvfi_int_data[rvfi_rd_wdata] = zero_extend(v);
+  rvfi_int_data[rvfi_rd_addr] = to_bits(8, r);
+  rvfi_int_data_present = true;
+}
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index d10029a8b..0c8422641 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -23,6 +23,18 @@ let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x
 
 let platform_arch = ref P.RV64
 
+(* Defaults for callbacks functions.
+   The model assumes that these functions do not change the state of the model. *)
+let mem_write_callback (addr, width, value) = ()
+let mem_read_callback (addr, width, value) = ()
+let mem_exception_callback (addr, num_of_exception) = ()
+let pc_write_callback value = ()
+let xreg_write_callback (reg, value) = ()
+let freg_write_callback (reg, value) = ()
+let csr_write_callback (reg, value) = ()
+let csr_read_callback (reg, value) = ()
+let vreg_write_callback (reg, value) = ()
+
 (* logging *)
 
 let config_print_instr       = ref true
diff --git a/test/run_tests.sh b/test/run_tests.sh
old mode 100755
new mode 100644