Merge branch 'rvfi-dii' into sail2

(except without the accidentally committed aarch64 files from the branch)

8 files changed, 448 insertions, 6 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index e6bbbd5c..a49ba6e3 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -6,9 +6,11 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 
 # non-instruction sources
 SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+SAIL_OTHER_RVFI_SRCS = prelude.sail rvfi_dii.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 
 SAIL_SRCS      = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
 SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
+SAIL_RVFI_SRCS = $(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
 
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
@@ -73,6 +75,12 @@ riscv_model.c: $(SAIL_SRCS) main.sail Makefile
 riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
 	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_model.c riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
 
+riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) main_rvfi.sail Makefile
+	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) main_rvfi.sail 1> $@
+
+riscv_rvfi: riscv_rvfi_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
+	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_rvfi_model.c -DRVFI_DII riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
+
 latex: $(SAIL_SRCS) Makefile
 	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
 
@@ -141,5 +149,6 @@ clean:
 	-rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v
 	-rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v
 	-rm -f riscv.c riscv_model.c riscv_sim
+	-rm -f riscv_rvfi_model.c riscv_rvfi
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/riscv/main_rvfi.sail b/riscv/main_rvfi.sail
new file mode 100644
index 00000000..0ba4acfc
--- /dev/null
+++ b/riscv/main_rvfi.sail
@@ -0,0 +1,108 @@
+// Alternative fetch and step for RVFI DII mode.
+
+val rvfi_fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg}
+
+function rvfi_fetch() =
+  /* check for legal PC */
+  if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC()))))
+  then F_Error(E_Fetch_Addr_Align, PC)
+  else {
+    let i = rvfi_instruction.rvfi_insn();
+    rvfi_exec->rvfi_order() = minstret;
+    rvfi_exec->rvfi_pc_rdata() = PC;
+    rvfi_exec->rvfi_insn() = zero_extend(i,64);
+    /* TODO: should we write these even if they're not really registers? */
+    rvfi_exec->rvfi_rs1_data() = X(i[19 .. 15]);
+    rvfi_exec->rvfi_rs2_data() = X(i[24 .. 20]);
+    rvfi_exec->rvfi_rs1_addr() = zero_extend(i[19 .. 15],8);
+    rvfi_exec->rvfi_rs2_addr() = zero_extend(i[24 .. 20],8);
+    if (i[1 .. 0] == 0b11)
+    then F_Base(i)
+    else F_RVC(i[15 .. 0])
+  }
+
+// This should be kept in sync with the normal step - at the moment the only
+// changes are to replace fetch by rvfi_fetch and record the next PC.
+
+/* returns whether to increment the step count in the trace */
+val rvfi_step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function rvfi_step(step_no) = {
+  minstret_written = false;     /* see note for minstret */
+  let (retired, stepped) : (bool, bool) =
+    match curInterrupt(cur_privilege, mip, mie, mideleg) {
+      Some(intr, priv) => {
+        print_bits("Handling interrupt: ", intr);
+        handle_interrupt(intr, priv);
+        (false, false)
+      },
+      None() => {
+        match rvfi_fetch() {
+          F_Error(e, addr) => {
+            handle_mem_exception(addr, e);
+            (false, false)
+          },
+          F_RVC(h) => {
+            match decodeCompressed(h) {
+              None() => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
+                instbits = EXTZ(h);
+                handle_illegal();
+                (false, true)
+              },
+              Some(ast) => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+                nextPC = PC + 2;
+                (execute(ast), true)
+              }
+            }
+          },
+          F_Base(w) => {
+            match decode(w) {
+              None() => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
+                instbits = EXTZ(w);
+                handle_illegal();
+                (false, true)
+              },
+              Some(ast) => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+                nextPC = PC + 4;
+                (execute(ast), true)
+              }
+            }
+          }
+        }
+      }
+    };
+  PC = nextPC;
+  rvfi_exec->rvfi_pc_wdata() = PC;
+//print_rvfi_exec();
+  if retired then retire_instruction();
+  stepped
+}
+
+
+/* Dummy to make sure that sail doesn't throw functions away */
+
+val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+
+function main () = {
+
+  // PC = __GetSlice_int(64, elf_entry(), 0);
+  rvfi_set_instr_packet(0x0000000000000000);
+  print_bits("", rvfi_get_cmd());
+  let _ = rvfi_step(0);
+  rvfi_zero_exec_packet();
+  rvfi_halt_exec_packet();
+  let _ = rvfi_get_exec_packet();
+  PC = zero_extend(0x1000, 64);
+  print_bits("PC = ", PC);
+  try {
+    init_platform();
+    init_sys();
+    loop()
+  } catch {
+    Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
+    Error_internal_error() => print("Error: internal error")
+  }
+}
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 434f79d5..37824ff4 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -40,10 +40,34 @@ function MEMr_reserved                (addr, width) = checked_mem_read(Data, add
 function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width, true, false, true)
 function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true)
 
+$ifdef RVFI_DII
+val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult(bits(8 * 'n))) -> unit effect {wreg}
+function rvfi_read (addr, width, result) = {
+  rvfi_exec->rvfi_mem_addr() = addr;
+  match result {
+  MemValue(v) =>
+    if width <= 8
+    then {
+      rvfi_exec->rvfi_mem_wdata() = zero_extend(v,64);
+      rvfi_exec->rvfi_mem_wmask() = to_bits(8,width)
+    } else (),
+  MemException(_) => ()
+  };
+}
+$else
+val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult(bits(8 * 'n))) -> unit
+function rvfi_read (addr, width, value) = ()
+$endif
+
 /* NOTE: The rreg effect is due to MMIO. */
+$ifdef RVFI_DII
+val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+$else
 val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+$endif
 
 function mem_read (addr, width, aq, rl, res) = {
+ let result : MemoryOpResult(bits(8 * 'n)) =
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_Load_Addr_Align)
   else match (aq, rl, res) {
@@ -55,7 +79,9 @@ function mem_read (addr, width, aq, rl, res) = {
     (true,  true,  false) => MEMr_strong_acquire(addr, width),
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
     (true,  true,  true)  => MEMr_reserved_strong_acquire(addr, width)
-  }
+  };
+ rvfi_read(addr, width, result);
+ result
 }
 
 val MEMea = {lem: "MEMea", coq: "MEMea", _: "memea"} : forall 'n.
@@ -118,10 +144,26 @@ function MEMval_conditional                (addr, width, data) = checked_mem_wri
 function MEMval_conditional_release        (addr, width, data) = checked_mem_write(addr, width, data)
 function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data)
 
+
+$ifdef RVFI_DII
+val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg}
+function rvfi_write (addr, width, value) = {
+  rvfi_exec->rvfi_mem_addr() = addr;
+  if width <= 8 then {
+    rvfi_exec->rvfi_mem_wdata() = zero_extend(value,64);
+    rvfi_exec->rvfi_mem_wmask() = to_bits(8,width);
+  }
+}
+$else
+val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit
+function rvfi_write (addr, width, value) = ()
+$endif
+
 /* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
 val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape}
 
 function mem_write_value (addr, width, value, aq, rl, con) = {
+  rvfi_write(addr, width, value);
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_SAMO_Addr_Align)
   else match (aq, rl, con) {
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
index f2569b3b..424b64b0 100644
--- a/riscv/riscv_sail.h
+++ b/riscv/riscv_sail.h
@@ -6,6 +6,9 @@ typedef int unit;
 #define UNIT 0
 typedef uint64_t mach_bits;
 
+struct zMisa {mach_bits zMisa_chunk_0;};
+struct zMisa zmisa;
+
 void model_init(void);
 void model_fini(void);
 
@@ -14,6 +17,16 @@ unit zinit_sys(unit);
 bool zstep(sail_int);
 unit ztick_clock(unit);
 unit ztick_platform(unit);
+unit z_set_Misa_C(struct zMisa*, mach_bits);
+
+#ifdef RVFI_DII
+unit zrvfi_set_instr_packet(mach_bits);
+mach_bits zrvfi_get_cmd(unit);
+bool zrvfi_step(sail_int);
+unit zrvfi_zzero_exec_packet(unit);
+unit zrvfi_halt_exec_packet(unit);
+void zrvfi_get_exec_packet(sail_bits *rop, unit);
+#endif
 
 extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
@@ -39,6 +52,3 @@ struct zMcause {mach_bits zMcause_chunk_0;};
 struct zMcause zmcause, zscause;
 
 extern mach_bits zminstret;
-
-struct zMisa {mach_bits zMisa_chunk_0;};
-struct zMisa zmisa;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index f518f20e..0a5fec70 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -6,6 +6,8 @@
 #include <sys/types.h>
 #include <sys/stat.h>
 #include <sys/mman.h>
+#include <sys/socket.h>
+#include <netinet/ip.h>
 #include <fcntl.h>
 
 #include "elf.h"
@@ -40,11 +42,17 @@ struct tv_spike_t;
 #define CSR_MIP 0x344
 
 static bool do_dump_dts = false;
+static bool disable_compressed = false;
 struct tv_spike_t *s = NULL;
 char *term_log = NULL;
 char *dtb_file = NULL;
 unsigned char *dtb = NULL;
 size_t dtb_len = 0;
+#ifdef RVFI_DII
+static bool rvfi_dii = false;
+static int rvfi_dii_port;
+static int rvfi_dii_sock;
+#endif
 
 unsigned char *spike_dtb = NULL;
 size_t spike_dtb_len = 0;
@@ -53,17 +61,25 @@ static struct option options[] = {
   {"enable-dirty",                no_argument,       0, 'd'},
   {"enable-misaligned",           no_argument,       0, 'm'},
   {"ram-size",                    required_argument, 0, 'z'},
+  {"disable-compressed",          no_argument,       0, 'C'},
   {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'},
   {"dump-dts",                    no_argument,       0, 's'},
   {"device-tree-blob",            required_argument, 0, 'b'},
   {"terminal-log",                required_argument, 0, 't'},
+#ifdef RVFI_DII
+  {"rvfi-dii",                    required_argument, 0, 'r'},
+#endif
   {"help",                        no_argument,       0, 'h'},
   {0, 0, 0, 0}
 };
 
 static void print_usage(const char *argv0, int ec)
 {
+#ifdef RVFI_DII
+  fprintf(stdout, "Usage: %s [options] <elf_file>\n       %s [options] -r <port>\n", argv0, argv0);
+#else
   fprintf(stdout, "Usage: %s [options] <elf_file>\n", argv0);
+#endif
   struct option *opt = options;
   while (opt->name) {
     fprintf(stdout, "\t -%c\t %s\n", (char)opt->val, opt->name);
@@ -125,7 +141,7 @@ char *process_args(int argc, char **argv)
   int c, idx = 1;
   uint64_t ram_size = 0;
   while(true) {
-    c = getopt_long(argc, argv, "dmsz:b:t:v:h", options, &idx);
+    c = getopt_long(argc, argv, "dmCsz:b:t:v:hr:", options, &idx);
     if (c == -1) break;
     switch (c) {
     case 'd':
@@ -136,6 +152,9 @@ char *process_args(int argc, char **argv)
       fprintf(stderr, "enabling misaligned access.\n");
       rv_enable_misaligned = true;
       break;
+    case 'C':
+      disable_compressed = true;
+      break;
     case 'i':
       rv_mtval_has_illegal_inst_bits = true;
     case 's':
@@ -157,16 +176,29 @@ char *process_args(int argc, char **argv)
     case 'h':
       print_usage(argv[0], 0);
       break;
+#ifdef RVFI_DII
+    case 'r':
+      rvfi_dii = true;
+      rvfi_dii_port = atoi(optarg);
+      break;
+#endif
     default:
       fprintf(stderr, "Unrecognized optchar %c\n", c);
       print_usage(argv[0], 1);
     }
   }
   if (do_dump_dts) dump_dts();
+#ifdef RVFI_DII
+  if (idx > argc || (idx == argc && !rvfi_dii)) print_usage(argv[0], 0);
+#else
   if (idx >= argc) print_usage(argv[0], 0);
+#endif
   if (term_log == NULL) term_log = strdup("term.log");
   if (dtb_file) read_dtb(dtb_file);
 
+#ifdef RVFI_DII
+  if (!rvfi_dii)
+#endif
   fprintf(stdout, "Running file %s.\n", argv[optind]);
   return argv[optind];
 }
@@ -316,7 +348,18 @@ void init_sail(uint64_t elf_entry)
   model_init();
   zinit_platform(UNIT);
   zinit_sys(UNIT);
+#ifdef RVFI_DII
+  if (rvfi_dii) {
+    rv_ram_base = UINT64_C(0x80000000);
+    rv_ram_size = UINT64_C(0x10000);
+    rv_rom_base = UINT64_C(0);
+    rv_rom_size = UINT64_C(0);
+    zPC = elf_entry;
+  } else
+#endif
   init_sail_reset_vector(elf_entry);
+  if (disable_compressed)
+    z_set_Misa_C(&zmisa, 0);
 }
 
 int init_check(struct tv_spike_t *s)
@@ -405,6 +448,26 @@ void flush_logs(void)
   fflush(stdout);
 }
 
+#ifdef RVFI_DII
+void rvfi_send_trace(void) {
+  sail_bits packet;
+  CREATE(lbits)(&packet);
+  zrvfi_get_exec_packet(&packet, UNIT);
+  if (packet.len % 8 != 0) {
+    fprintf(stderr, "RVFI-DII trace packet not byte aligned: %d\n", (int)packet.len);
+    exit(1);
+  }
+  unsigned char bytes[packet.len / 8];
+  /* mpz_export might not write all of the null bytes */
+  memset(bytes, 0, sizeof(bytes));
+  mpz_export(bytes, NULL, -1, 1, 0, 0, *(packet.bits));
+  if (write(rvfi_dii_sock, bytes, packet.len / 8) == -1) {
+    fprintf(stderr, "Writing RVFI DII trace failed: %s", strerror(errno));
+    exit(1);
+  }
+}
+#endif
+
 void run_sail(void)
 {
   bool spike_done;
@@ -414,8 +477,47 @@ void run_sail(void)
   /* initialize the step number */
   mach_int step_no = 0;
   int insn_cnt = 0;
+#ifdef RVFI_DII
+  bool need_instr = true;
+#endif
 
   while (!zhtif_done) {
+#ifdef RVFI_DII
+    if (rvfi_dii) {
+      if (need_instr) {
+        mach_bits instr_bits;
+        if (read(rvfi_dii_sock, &instr_bits, sizeof(instr_bits)) == -1) {
+          fprintf(stderr, "Reading RVFI DII command failed: %s", strerror(errno));
+          exit(1);
+        }
+        zrvfi_set_instr_packet(instr_bits);
+        zrvfi_zzero_exec_packet(UNIT);
+        mach_bits cmd = zrvfi_get_cmd(UNIT);
+        switch (cmd) {
+        case 0: /* EndOfTrace */
+          zrvfi_halt_exec_packet(UNIT);
+          rvfi_send_trace();
+          return;
+        case 1: /* Instruction */
+          break;
+        default:
+          fprintf(stderr, "Unknown RVFI-DII command: %d\n", (int)cmd);
+          exit(1);
+        }
+      }
+      sail_int sail_step;
+      CREATE(sail_int)(&sail_step);
+      CONVERT_OF(sail_int, mach_int)(&sail_step, step_no);
+      stepped = zrvfi_step(sail_step);
+      if (have_exception) goto step_exception;
+      flush_logs();
+      if (stepped) {
+        need_instr = true;
+        rvfi_send_trace();
+      } else
+        need_instr = false;
+    } else
+#endif
     { /* run a Sail step */
       sail_int sail_step;
       CREATE(sail_int)(&sail_step);
@@ -503,7 +605,46 @@ int main(int argc, char **argv)
   char *file = process_args(argc, argv);
   init_logs();
 
+#ifdef RVFI_DII
+  uint64_t entry;
+  if (rvfi_dii) {
+    entry = 0x80000000;
+    int listen_sock = socket(AF_INET, SOCK_STREAM, 0);
+    if (listen_sock == -1) {
+      fprintf(stderr, "Unable to create socket: %s", strerror(errno));
+      return 1;
+    }
+    int opt = 1;
+    if (setsockopt(listen_sock, SOL_SOCKET, SO_REUSEADDR, &opt, sizeof(opt)) == -1) {
+      fprintf(stderr, "Unable to set reuseaddr on socket: %s", strerror(errno));
+      return 1;
+    }
+    struct sockaddr_in addr = {
+      .sin_family = AF_INET,
+      .sin_addr.s_addr = INADDR_ANY,
+      .sin_port = htons(rvfi_dii_port)
+    };
+    if (bind(listen_sock, (struct sockaddr *)&addr, sizeof(addr)) == -1) {
+      fprintf(stderr, "Unable to set bind socket: %s", strerror(errno));
+      return 1;
+    }
+    if (listen(listen_sock, 1) == -1) {
+      fprintf(stderr, "Unable to listen on socket: %s", strerror(errno));
+      return 1;
+    }
+    printf("Waiting for connection\n");
+    rvfi_dii_sock = accept(listen_sock, NULL, NULL);
+    if (rvfi_dii_sock == -1) {
+      fprintf(stderr, "Unable to accept connection on socket: %s", strerror(errno));
+      return 1;
+    }
+    close(listen_sock);
+    printf("Connected\n");
+  } else
+    entry = load_sail(file);
+#else
   uint64_t entry = load_sail(file);
+#endif
 
   /* initialize spike before sail so that we can access the device-tree blob,
    * until we roll our own.
@@ -513,6 +654,18 @@ int main(int argc, char **argv)
 
   if (!init_check(s)) finish(1);
 
-  run_sail();
+  do {
+    run_sail();
+#ifndef RVFI_DII
+  } while (0);
+#else
+    if (rvfi_dii) {
+      /* Reset for next test; currently we only quit when the connection breaks
+         and we crash due to SIGPIPE. */
+      model_fini();
+      init_sail(entry);
+    }
+  } while (rvfi_dii);
+#endif
   flush_logs();
 }
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 9c49d9e5..81871f91 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -874,10 +874,20 @@ union ctl_result = {
 /* TODO: CTL_URET */
 }
 
+$ifdef RVFI_DII
+val rvfi_trap : unit -> unit effect {wreg}
+function rvfi_trap () =
+  rvfi_exec->rvfi_trap() = 0x01
+$else
+val rvfi_trap : unit -> unit
+function rvfi_trap () = ()
+$endif
+
 /* handle exceptional ctl flow by updating nextPC and operating privilege */
 
 function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
                     -> xlenbits = {
+  rvfi_trap();
   print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
 
   match (del_priv) {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 4cbc6f87..7e29ef3c 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -114,6 +114,17 @@ function rX r = match r {
   31 => x31
 }
 
+$ifdef RVFI_DII
+val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+function rvfi_wX (r,v) = {
+  rvfi_exec->rvfi_rd_wdata() = v;
+  rvfi_exec->rvfi_rd_addr() = to_bits(8,r);
+}
+$else
+val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
+function rvfi_wX (r,v) = ()
+$endif
+
 val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
 function wX (r, v) = {
   match r {
@@ -151,6 +162,7 @@ function wX (r, v) = {
     31 => x31 = v
   };
   if (r != 0) then {
+     rvfi_wX(r,v);
      // Xs[r] = v;
      print("x" ^ string_of_int(r) ^ " <- " ^ BitStr(v));
   }
diff --git a/riscv/rvfi_dii.sail b/riscv/rvfi_dii.sail
new file mode 100644
index 00000000..9680ab49
--- /dev/null
+++ b/riscv/rvfi_dii.sail
@@ -0,0 +1,98 @@
+// "RISC-V Formal Interface - Direct Instruction Injection" support
+// For use with https://github.com/CTSRD-CHERI/TestRIG
+
+$define RVFI_DII
+
+bitfield RVFI_DII_Instruction_Packet : bits(64) = {
+   padding   : 63 .. 56, // [7]
+   rvfi_cmd  : 55 .. 48, // [6] This token is a trace command.  For example, reset device under test.
+   rvfi_time : 47 .. 32, // [5 - 4] Time to inject token.  The difference between this and the previous
+                         // instruction time gives a delay before injecting this instruction.
+                         // This can be ignored for models but gives repeatability for implementations
+                         // while shortening counterexamples.
+   rvfi_insn : 31 ..  0, // [0 - 3] Instruction word: 32-bit instruction or command. The lower 16-bits
+                         // may decode to a 16-bit compressed instruction.
+}
+
+register rvfi_instruction : RVFI_DII_Instruction_Packet
+
+val rvfi_set_instr_packet : bits(64) -> unit effect {wreg}
+
+function rvfi_set_instr_packet(p) =
+  rvfi_instruction = Mk_RVFI_DII_Instruction_Packet(p)
+
+val rvfi_get_cmd : unit -> bits(8) effect {rreg}
+
+function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd()
+
+val print_instr_packet : bits(64) -> unit
+
+function print_instr_packet(bs) = {
+  let p = Mk_RVFI_DII_Instruction_Packet(bs);
+  print_bits("command", p.rvfi_cmd());
+  print_bits("instruction", p.rvfi_insn())
+}
+
+bitfield RVFI_DII_Execution_Packet : bits(704) = {
+   rvfi_intr      : 703 .. 696, // [87] Trap handler:            Set for first instruction in trap handler.
+   rvfi_halt      : 695 .. 688, // [86] Halt indicator:          Marks the last instruction retired 
+                                //                                      before halting execution.
+   rvfi_trap      : 687 .. 680, // [85] Trap indicator:          Invalid decode, misaligned access or
+                                //                                      jump command to misaligned address.
+   rvfi_rd_addr   : 679 .. 672, // [84]      Write register address:  MUST be 0 if not used.
+   rvfi_rs2_addr  : 671 .. 664, // [83]                          otherwise set as decoded.
+   rvfi_rs1_addr  : 663 .. 656, // [82]      Read register addresses: Can be arbitrary when not used,
+   rvfi_mem_wmask : 655 .. 648, // [81]      Write mask:              Indicates valid bytes written. 0 if unused.
+   rvfi_mem_rmask : 647 .. 640, // [80]      Read mask:               Indicates valid bytes read. 0 if unused.
+   rvfi_mem_wdata : 639 .. 576, // [72 - 79] Write data:              Data written to memory by this command.
+   rvfi_mem_rdata : 575 .. 512, // [64 - 71] Read data:               Data read from mem_addr (i.e. before write)
+   rvfi_mem_addr  : 511 .. 448, // [56 - 63] Memory access addr:      Points to byte address (aligned if define
+                                //                                      is set). *Should* be straightforward.
+                                //                                      0 if unused.
+   rvfi_rd_wdata  : 447 .. 384, // [48 - 55] Write register value:    MUST be 0 if rd_ is 0.
+   rvfi_rs2_data  : 383 .. 320, // [40 - 47]                          above. Must be 0 if register ID is 0.
+   rvfi_rs1_data  : 319 .. 256, // [32 - 39] Read register values:    Values as read from registers named
+   rvfi_insn      : 255 .. 192, // [24 - 31] Instruction word:        32-bit command value.
+   rvfi_pc_wdata  : 191 .. 128, // [16 - 23] PC after instr:          Following PC - either PC + 4 or jump/trap target.
+   rvfi_pc_rdata  : 127 ..  64, // [08 - 15] PC before instr:         PC for current instruction
+   rvfi_order     :  63 ..   0, // [00 - 07] Instruction number:      INSTRET value after completion.
+}
+
+register rvfi_exec : RVFI_DII_Execution_Packet
+
+val rvfi_zero_exec_packet : unit -> unit effect {wreg}
+
+function rvfi_zero_exec_packet () =
+  rvfi_exec = Mk_RVFI_DII_Execution_Packet(zero_extend(0b0,704))
+
+val rvfi_halt_exec_packet : unit -> unit effect {wreg}
+
+function rvfi_halt_exec_packet () =
+  rvfi_exec->rvfi_halt() = 0x01
+
+val rvfi_get_exec_packet : unit -> bits(704) effect {rreg}
+
+function rvfi_get_exec_packet() = rvfi_exec.bits()
+
+val print_rvfi_exec : unit -> unit effect {rreg}
+
+function print_rvfi_exec () = {
+  print_bits("rvfi_intr     : ", rvfi_exec.rvfi_intr());
+  print_bits("rvfi_halt     : ", rvfi_exec.rvfi_halt());
+  print_bits("rvfi_trap     : ", rvfi_exec.rvfi_trap());
+  print_bits("rvfi_rd_addr  : ", rvfi_exec.rvfi_rd_addr());
+  print_bits("rvfi_rs2_addr : ", rvfi_exec.rvfi_rs2_addr());
+  print_bits("rvfi_rs1_addr : ", rvfi_exec.rvfi_rs1_addr());
+  print_bits("rvfi_mem_wmask: ", rvfi_exec.rvfi_mem_wmask());
+  print_bits("rvfi_mem_rmask: ", rvfi_exec.rvfi_mem_rmask());
+  print_bits("rvfi_mem_wdata: ", rvfi_exec.rvfi_mem_wdata());
+  print_bits("rvfi_mem_rdata: ", rvfi_exec.rvfi_mem_rdata());
+  print_bits("rvfi_mem_addr : ", rvfi_exec.rvfi_mem_addr());
+  print_bits("rvfi_rd_wdata : ", rvfi_exec.rvfi_rd_wdata());
+  print_bits("rvfi_rs2_data : ", rvfi_exec.rvfi_rs2_data());
+  print_bits("rvfi_rs1_data : ", rvfi_exec.rvfi_rs1_data());
+  print_bits("rvfi_insn     : ", rvfi_exec.rvfi_insn());
+  print_bits("rvfi_pc_wdata : ", rvfi_exec.rvfi_pc_wdata());
+  print_bits("rvfi_pc_rdata : ", rvfi_exec.rvfi_pc_rdata());
+  print_bits("rvfi_order    : ", rvfi_exec.rvfi_order());
+}