diff --git a/Makefile b/Makefile
index 1655bdf..00f4cc7 100644
--- a/Makefile
+++ b/Makefile
@@ -47,15 +47,15 @@ test_synth: testbench_synth.vvp firmware/firmware.hex
 	vvp -N $<
 
 testbench.vvp: testbench.v picorv32.v
-	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL $^
+	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
 	chmod -x $@
 
 testbench_wb.vvp: testbench_wb.v picorv32.v
-	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL $^
+	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
 	chmod -x $@
 
 testbench_sp.vvp: testbench.v picorv32.v
-	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL -DSP_TEST $^
+	iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DSP_TEST $^
 	chmod -x $@
 
 testbench_synth.vvp: testbench.v synth.v
diff --git a/picorv32.v b/picorv32.v
index 8c7b5b8..a1eebbd 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -2386,6 +2386,26 @@ module picorv32_axi #(
 	input  [31:0] irq,
 	output [31:0] eoi,
 
+`ifdef RISCV_FORMAL
+	output        rvfi_valid,
+	output [ 7:0] rvfi_order,
+	output [31:0] rvfi_insn,
+	output        rvfi_trap,
+	output [ 4:0] rvfi_rs1_addr,
+	output [ 4:0] rvfi_rs2_addr,
+	output [31:0] rvfi_rs1_rdata,
+	output [31:0] rvfi_rs2_rdata,
+	output [ 4:0] rvfi_rd_addr,
+	output [31:0] rvfi_rd_wdata,
+	output [31:0] rvfi_pc_rdata,
+	output [31:0] rvfi_pc_wdata,
+	output [31:0] rvfi_mem_addr,
+	output [ 3:0] rvfi_mem_rmask,
+	output [ 3:0] rvfi_mem_wmask,
+	output [31:0] rvfi_mem_rdata,
+	output [31:0] rvfi_mem_wdata,
+`endif
+
 	// Trace Interface
 	output        trace_valid,
 	output [35:0] trace_data
@@ -2478,6 +2498,26 @@ module picorv32_axi #(
 		.irq(irq),
 		.eoi(eoi),
 
+`ifdef RISCV_FORMAL
+		.rvfi_valid    (rvfi_valid    ),
+		.rvfi_order    (rvfi_order    ),
+		.rvfi_insn     (rvfi_insn     ),
+		.rvfi_trap     (rvfi_trap     ),
+		.rvfi_rs1_addr (rvfi_rs1_addr ),
+		.rvfi_rs2_addr (rvfi_rs2_addr ),
+		.rvfi_rs1_rdata(rvfi_rs1_rdata),
+		.rvfi_rs2_rdata(rvfi_rs2_rdata),
+		.rvfi_rd_addr  (rvfi_rd_addr  ),
+		.rvfi_rd_wdata (rvfi_rd_wdata ),
+		.rvfi_pc_rdata (rvfi_pc_rdata ),
+		.rvfi_pc_wdata (rvfi_pc_wdata ),
+		.rvfi_mem_addr (rvfi_mem_addr ),
+		.rvfi_mem_rmask(rvfi_mem_rmask),
+		.rvfi_mem_wmask(rvfi_mem_wmask),
+		.rvfi_mem_rdata(rvfi_mem_rdata),
+		.rvfi_mem_wdata(rvfi_mem_wdata),
+`endif
+
 		.trace_valid(trace_valid),
 		.trace_data (trace_data)
 	);
@@ -2628,6 +2668,26 @@ module picorv32_wb #(
 	input  [31:0] irq,
 	output [31:0] eoi,
 
+`ifdef RISCV_FORMAL
+	output        rvfi_valid,
+	output [ 7:0] rvfi_order,
+	output [31:0] rvfi_insn,
+	output        rvfi_trap,
+	output [ 4:0] rvfi_rs1_addr,
+	output [ 4:0] rvfi_rs2_addr,
+	output [31:0] rvfi_rs1_rdata,
+	output [31:0] rvfi_rs2_rdata,
+	output [ 4:0] rvfi_rd_addr,
+	output [31:0] rvfi_rd_wdata,
+	output [31:0] rvfi_pc_rdata,
+	output [31:0] rvfi_pc_wdata,
+	output [31:0] rvfi_mem_addr,
+	output [ 3:0] rvfi_mem_rmask,
+	output [ 3:0] rvfi_mem_wmask,
+	output [31:0] rvfi_mem_rdata,
+	output [31:0] rvfi_mem_wdata,
+`endif
+
 	// Trace Interface
 	output        trace_valid,
 	output [35:0] trace_data,
@@ -2698,6 +2758,26 @@ module picorv32_wb #(
 		.irq(irq),
 		.eoi(eoi),
 
+`ifdef RISCV_FORMAL
+		.rvfi_valid    (rvfi_valid    ),
+		.rvfi_order    (rvfi_order    ),
+		.rvfi_insn     (rvfi_insn     ),
+		.rvfi_trap     (rvfi_trap     ),
+		.rvfi_rs1_addr (rvfi_rs1_addr ),
+		.rvfi_rs2_addr (rvfi_rs2_addr ),
+		.rvfi_rs1_rdata(rvfi_rs1_rdata),
+		.rvfi_rs2_rdata(rvfi_rs2_rdata),
+		.rvfi_rd_addr  (rvfi_rd_addr  ),
+		.rvfi_rd_wdata (rvfi_rd_wdata ),
+		.rvfi_pc_rdata (rvfi_pc_rdata ),
+		.rvfi_pc_wdata (rvfi_pc_wdata ),
+		.rvfi_mem_addr (rvfi_mem_addr ),
+		.rvfi_mem_rmask(rvfi_mem_rmask),
+		.rvfi_mem_wmask(rvfi_mem_wmask),
+		.rvfi_mem_rdata(rvfi_mem_rdata),
+		.rvfi_mem_wdata(rvfi_mem_wdata),
+`endif
+
 		.trace_valid(trace_valid),
 		.trace_data (trace_data)
 	);
diff --git a/testbench.v b/testbench.v
index 9380445..1eb2e01 100644
--- a/testbench.v
+++ b/testbench.v
@@ -135,6 +135,26 @@ module picorv32_wrapper #(
 		.tests_passed    (tests_passed    )
 	);
 
+`ifdef RISCV_FORMAL
+	wire        rvfi_valid;
+	wire [7:0]  rvfi_order;
+	wire [31:0] rvfi_insn;
+	wire        rvfi_trap;
+	wire [4:0]  rvfi_rs1_addr;
+	wire [4:0]  rvfi_rs2_addr;
+	wire [31:0] rvfi_rs1_rdata;
+	wire [31:0] rvfi_rs2_rdata;
+	wire [4:0]  rvfi_rd_addr;
+	wire [31:0] rvfi_rd_wdata;
+	wire [31:0] rvfi_pc_rdata;
+	wire [31:0] rvfi_pc_wdata;
+	wire [31:0] rvfi_mem_addr;
+	wire [3:0]  rvfi_mem_rmask;
+	wire [3:0]  rvfi_mem_wmask;
+	wire [31:0] rvfi_mem_rdata;
+	wire [31:0] rvfi_mem_wdata;
+`endif
+
 	picorv32_axi #(
 `ifndef SYNTH_TEST
 `ifdef SP_TEST
@@ -170,10 +190,53 @@ module picorv32_wrapper #(
 		.mem_axi_rready (mem_axi_rready ),
 		.mem_axi_rdata  (mem_axi_rdata  ),
 		.irq            (irq            ),
+`ifdef RISCV_FORMAL
+		.rvfi_valid     (rvfi_valid     ),
+		.rvfi_order     (rvfi_order     ),
+		.rvfi_insn      (rvfi_insn      ),
+		.rvfi_trap      (rvfi_trap      ),
+		.rvfi_rs1_addr  (rvfi_rs1_addr  ),
+		.rvfi_rs2_addr  (rvfi_rs2_addr  ),
+		.rvfi_rs1_rdata (rvfi_rs1_rdata ),
+		.rvfi_rs2_rdata (rvfi_rs2_rdata ),
+		.rvfi_rd_addr   (rvfi_rd_addr   ),
+		.rvfi_rd_wdata  (rvfi_rd_wdata  ),
+		.rvfi_pc_rdata  (rvfi_pc_rdata  ),
+		.rvfi_pc_wdata  (rvfi_pc_wdata  ),
+		.rvfi_mem_addr  (rvfi_mem_addr  ),
+		.rvfi_mem_rmask (rvfi_mem_rmask ),
+		.rvfi_mem_wmask (rvfi_mem_wmask ),
+		.rvfi_mem_rdata (rvfi_mem_rdata ),
+		.rvfi_mem_wdata (rvfi_mem_wdata ),
+`endif
 		.trace_valid    (trace_valid    ),
 		.trace_data     (trace_data     )
 	);
 
+`ifdef RISCV_FORMAL
+	riscv_formal_monitor_rv32ic rvfi_monitor (
+		.clock         (clk           ),
+		.reset         (!resetn       ),
+		.rvfi_valid    (rvfi_valid    ),
+		.rvfi_order    (rvfi_order    ),
+		.rvfi_insn     (rvfi_insn     ),
+		.rvfi_trap     (rvfi_trap     ),
+		.rvfi_rs1_addr (rvfi_rs1_addr ),
+		.rvfi_rs2_addr (rvfi_rs2_addr ),
+		.rvfi_rs1_rdata(rvfi_rs1_rdata),
+		.rvfi_rs2_rdata(rvfi_rs2_rdata),
+		.rvfi_rd_addr  (rvfi_rd_addr  ),
+		.rvfi_rd_wdata (rvfi_rd_wdata ),
+		.rvfi_pc_rdata (rvfi_pc_rdata ),
+		.rvfi_pc_wdata (rvfi_pc_wdata ),
+		.rvfi_mem_addr (rvfi_mem_addr ),
+		.rvfi_mem_rmask(rvfi_mem_rmask),
+		.rvfi_mem_wmask(rvfi_mem_wmask),
+		.rvfi_mem_rdata(rvfi_mem_rdata),
+		.rvfi_mem_wdata(rvfi_mem_wdata)
+	);
+`endif
+
 	reg [1023:0] firmware_file;
 	initial begin
 		if (!$value$plusargs("firmware=%s", firmware_file))