diff --git a/.gitmodules b/.gitmodules
index a87c55f..58c58a9 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -8,5 +8,5 @@
 	path = scripts
 	url = https://github.com/Wren6991/fpgascripts
 [submodule "test/formal/riscv-formal"]
-	path = test/formal/riscv-formal
+	path = test/formal/riscv-formal/riscv-formal
 	url = https://github.com/Wren6991/riscv-formal.git
diff --git a/sourceme b/sourceme
index dc87120..94e4e76 100644
--- a/sourceme
+++ b/sourceme
@@ -1 +1,3 @@
 export PATH="$PATH:$PWD/scripts"
+export PROJ_ROOT=$PWD
+export HDL=$PROJ_ROOT/hdl
diff --git a/test/formal/riscv-formal b/test/formal/riscv-formal
deleted file mode 160000
index 7dd18d8..0000000
--- a/test/formal/riscv-formal
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 7dd18d861e76e01c6ce27adce1c9cc2f5b36e4c1
diff --git a/test/formal/riscv-formal/riscv-formal b/test/formal/riscv-formal/riscv-formal
new file mode 160000
index 0000000..8bede6c
--- /dev/null
+++ b/test/formal/riscv-formal/riscv-formal
@@ -0,0 +1 @@
+Subproject commit 8bede6ceb93ac66641bbd74a99d65a80140bc31c
diff --git a/test/formal/riscv-formal/tb/hazard3_rvfi.f b/test/formal/riscv-formal/tb/hazard3_rvfi.f
new file mode 100644
index 0000000..77a5b35
--- /dev/null
+++ b/test/formal/riscv-formal/tb/hazard3_rvfi.f
@@ -0,0 +1,4 @@
+file hazard3_rvfi_wrapper.v
+include .
+file $PROJ_ROOT/test/formal/common/ahbl_slave_assumptions.v
+list $HDL/hazard3.f
diff --git a/hdl/hazard3_rvfi_monitor.vh b/test/formal/riscv-formal/tb/hazard3_rvfi_monitor.vh
similarity index 100%
rename from hdl/hazard3_rvfi_monitor.vh
rename to test/formal/riscv-formal/tb/hazard3_rvfi_monitor.vh
diff --git a/hdl/hazard3_rvfi_wrapper.v b/test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
similarity index 92%
rename from hdl/hazard3_rvfi_wrapper.v
rename to test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
index fd2e6fa..5069fda 100644
--- a/hdl/hazard3_rvfi_wrapper.v
+++ b/test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
@@ -87,7 +87,12 @@ ahbl_slave_assumptions #(
 // Device Under Test
 // ----------------------------------------------------------------------------
 
-(* keep *) `rvformal_rand_reg [15:0] irq;
+// FIXME IRQs are tied off because riscv-formal doesn't accept the
+// nonsequential pc_wdata when an instruction is followed by an interrupt
+// (and the rvfi_intr signal doesn't do anything)
+
+wire [15:0] irq = 0;
+// (* keep *) `rvformal_rand_reg [15:0] irq;
 
 hazard3_cpu_2port #(
 	.RESET_VECTOR  (0),