diff --git a/.gitignore b/.gitignore
index 487adcc..b80458f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,3 +35,4 @@
 /synth.log
 /synth.v
 .*.swp
+.vscode
diff --git a/Makefile b/Makefile
index d28b598..f9d7594 100644
--- a/Makefile
+++ b/Makefile
@@ -27,9 +27,6 @@ test: testbench.vvp firmware/firmware.hex
 test_vcd: testbench.vvp firmware/firmware.hex
 	$(VVP) -N $< +vcd +trace +noerror
 
-test_rvf: testbench_rvf.vvp firmware/firmware.hex
-	$(VVP) -N $< +vcd +trace +noerror
-
 test_wb: testbench_wb.vvp firmware/firmware.hex
 	$(VVP) -N $<
 
@@ -58,10 +55,6 @@ testbench.vvp: testbench.v picorv32.v
 	$(IVERILOG) -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
 	chmod -x $@
 
-testbench_rvf.vvp: testbench.v picorv32.v rvfimon.v
-	$(IVERILOG) -o $@ -D RISCV_FORMAL $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
-	chmod -x $@
-
 testbench_wb.vvp: testbench_wb.v picorv32.v
 	$(IVERILOG) -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
 	chmod -x $@
@@ -178,7 +171,7 @@ clean:
 	rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) check.smt2 check.vcd synth.v synth.log \
 		firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
 		testbench.vvp testbench_sp.vvp testbench_synth.vvp testbench_ez.vvp \
-		testbench_rvf.vvp testbench_wb.vvp testbench.vcd testbench.trace \
+		testbench_wb.vvp testbench.vcd testbench.trace \
 		testbench_verilator testbench_verilator_dir
 
 .PHONY: test test_vcd test_sp test_axi test_wb test_wb_vcd test_ez test_ez_vcd test_synth download-tools build-tools toc clean
diff --git a/picorv32.v b/picorv32.v
index cfc7ce0..90640ac 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -35,17 +35,8 @@
   `define debug(debug_command)
 `endif
 
-`ifdef FORMAL
-  `define FORMAL_KEEP (* keep *)
-  `define assert(assert_expr) assert(assert_expr)
-`else
-  `ifdef DEBUGNETS
-    `define FORMAL_KEEP (* keep *)
-  `else
-    `define FORMAL_KEEP
-  `endif
-  `define assert(assert_expr) empty_statement
-`endif
+`define assert(assert_expr) empty_statement
+`define FORMAL_KEEP
 
 // uncomment this for register file in extra module
 // `define PICORV32_REGS picorv32_regs
@@ -120,40 +111,6 @@ module picorv32 #(
 	input      [31:0] irq,
 	output reg [31:0] eoi,
 
-`ifdef RISCV_FORMAL
-	output reg        rvfi_valid,
-	output reg [63:0] rvfi_order,
-	output reg [31:0] rvfi_insn,
-	output reg        rvfi_trap,
-	output reg        rvfi_halt,
-	output reg        rvfi_intr,
-	output reg [ 1:0] rvfi_mode,
-	output reg [ 1:0] rvfi_ixl,
-	output reg [ 4:0] rvfi_rs1_addr,
-	output reg [ 4:0] rvfi_rs2_addr,
-	output reg [31:0] rvfi_rs1_rdata,
-	output reg [31:0] rvfi_rs2_rdata,
-	output reg [ 4:0] rvfi_rd_addr,
-	output reg [31:0] rvfi_rd_wdata,
-	output reg [31:0] rvfi_pc_rdata,
-	output reg [31:0] rvfi_pc_wdata,
-	output reg [31:0] rvfi_mem_addr,
-	output reg [ 3:0] rvfi_mem_rmask,
-	output reg [ 3:0] rvfi_mem_wmask,
-	output reg [31:0] rvfi_mem_rdata,
-	output reg [31:0] rvfi_mem_wdata,
-
-	output reg [63:0] rvfi_csr_mcycle_rmask,
-	output reg [63:0] rvfi_csr_mcycle_wmask,
-	output reg [63:0] rvfi_csr_mcycle_rdata,
-	output reg [63:0] rvfi_csr_mcycle_wdata,
-
-	output reg [63:0] rvfi_csr_minstret_rmask,
-	output reg [63:0] rvfi_csr_minstret_wmask,
-	output reg [63:0] rvfi_csr_minstret_rdata,
-	output reg [63:0] rvfi_csr_minstret_wdata,
-`endif
-
 	// Trace Interface
 	output reg        trace_valid,
 	output reg [35:0] trace_data
@@ -217,41 +174,6 @@ module picorv32 #(
 		begin end
 	endtask
 
-`ifdef DEBUGREGS
-	wire [31:0] dbg_reg_x0  = 0;
-	wire [31:0] dbg_reg_x1  = cpuregs[1];
-	wire [31:0] dbg_reg_x2  = cpuregs[2];
-	wire [31:0] dbg_reg_x3  = cpuregs[3];
-	wire [31:0] dbg_reg_x4  = cpuregs[4];
-	wire [31:0] dbg_reg_x5  = cpuregs[5];
-	wire [31:0] dbg_reg_x6  = cpuregs[6];
-	wire [31:0] dbg_reg_x7  = cpuregs[7];
-	wire [31:0] dbg_reg_x8  = cpuregs[8];
-	wire [31:0] dbg_reg_x9  = cpuregs[9];
-	wire [31:0] dbg_reg_x10 = cpuregs[10];
-	wire [31:0] dbg_reg_x11 = cpuregs[11];
-	wire [31:0] dbg_reg_x12 = cpuregs[12];
-	wire [31:0] dbg_reg_x13 = cpuregs[13];
-	wire [31:0] dbg_reg_x14 = cpuregs[14];
-	wire [31:0] dbg_reg_x15 = cpuregs[15];
-	wire [31:0] dbg_reg_x16 = cpuregs[16];
-	wire [31:0] dbg_reg_x17 = cpuregs[17];
-	wire [31:0] dbg_reg_x18 = cpuregs[18];
-	wire [31:0] dbg_reg_x19 = cpuregs[19];
-	wire [31:0] dbg_reg_x20 = cpuregs[20];
-	wire [31:0] dbg_reg_x21 = cpuregs[21];
-	wire [31:0] dbg_reg_x22 = cpuregs[22];
-	wire [31:0] dbg_reg_x23 = cpuregs[23];
-	wire [31:0] dbg_reg_x24 = cpuregs[24];
-	wire [31:0] dbg_reg_x25 = cpuregs[25];
-	wire [31:0] dbg_reg_x26 = cpuregs[26];
-	wire [31:0] dbg_reg_x27 = cpuregs[27];
-	wire [31:0] dbg_reg_x28 = cpuregs[28];
-	wire [31:0] dbg_reg_x29 = cpuregs[29];
-	wire [31:0] dbg_reg_x30 = cpuregs[30];
-	wire [31:0] dbg_reg_x31 = cpuregs[31];
-`endif
-
 	// Internal PCPI Cores
 
 	wire        pcpi_mul_wr;
@@ -687,6 +609,7 @@ module picorv32 #(
 	assign is_rdcycle_rdcycleh_rdinstr_rdinstrh = |{instr_rdcycle, instr_rdcycleh, instr_rdinstr, instr_rdinstrh};
 
 	reg [63:0] new_ascii_instr;
+
 	`FORMAL_KEEP reg [63:0] dbg_ascii_instr;
 	`FORMAL_KEEP reg [31:0] dbg_insn_imm;
 	`FORMAL_KEEP reg [4:0] dbg_insn_rs1;
@@ -696,6 +619,7 @@ module picorv32 #(
 	`FORMAL_KEEP reg [31:0] dbg_rs2val;
 	`FORMAL_KEEP reg dbg_rs1val_valid;
 	`FORMAL_KEEP reg dbg_rs2val_valid;
+	`FORMAL_KEEP reg [127:0] dbg_ascii_state;
 
 	always @* begin
 		new_ascii_instr = "";
@@ -1176,8 +1100,6 @@ module picorv32 #(
 	reg [7:0] cpu_state;
 	reg [1:0] irq_state;
 
-	`FORMAL_KEEP reg [127:0] dbg_ascii_state;
-
 	always @* begin
 		dbg_ascii_state = "";
 		if (cpu_state == cpu_state_trap)   dbg_ascii_state = "trap";
@@ -1968,197 +1890,6 @@ module picorv32 #(
 		end
 		current_pc = 'bx;
 	end
-
-`ifdef RISCV_FORMAL
-	reg dbg_irq_call;
-	reg dbg_irq_enter;
-	reg [31:0] dbg_irq_ret;
-	always @(posedge clk) begin
-		rvfi_valid <= resetn && (launch_next_insn || trap) && dbg_valid_insn;
-		rvfi_order <= resetn ? rvfi_order + rvfi_valid : 0;
-
-		rvfi_insn <= dbg_insn_opcode;
-		rvfi_rs1_addr <= dbg_rs1val_valid ? dbg_insn_rs1 : 0;
-		rvfi_rs2_addr <= dbg_rs2val_valid ? dbg_insn_rs2 : 0;
-		rvfi_pc_rdata <= dbg_insn_addr;
-		rvfi_rs1_rdata <= dbg_rs1val_valid ? dbg_rs1val : 0;
-		rvfi_rs2_rdata <= dbg_rs2val_valid ? dbg_rs2val : 0;
-		rvfi_trap <= trap;
-		rvfi_halt <= trap;
-		rvfi_intr <= dbg_irq_enter;
-		rvfi_mode <= 3;
-		rvfi_ixl <= 1;
-
-		if (!resetn) begin
-			dbg_irq_call <= 0;
-			dbg_irq_enter <= 0;
-		end else
-		if (rvfi_valid) begin
-			dbg_irq_call <= 0;
-			dbg_irq_enter <= dbg_irq_call;
-		end else
-		if (irq_state == 1) begin
-			dbg_irq_call <= 1;
-			dbg_irq_ret <= next_pc;
-		end
-
-		if (!resetn) begin
-			rvfi_rd_addr <= 0;
-			rvfi_rd_wdata <= 0;
-		end else
-		if (cpuregs_write && !irq_state) begin
-`ifdef PICORV32_TESTBUG_003
-			rvfi_rd_addr <= latched_rd ^ 1;
-`else
-			rvfi_rd_addr <= latched_rd;
-`endif
-`ifdef PICORV32_TESTBUG_004
-			rvfi_rd_wdata <= latched_rd ? cpuregs_wrdata ^ 1 : 0;
-`else
-			rvfi_rd_wdata <= latched_rd ? cpuregs_wrdata : 0;
-`endif
-		end else
-		if (rvfi_valid) begin
-			rvfi_rd_addr <= 0;
-			rvfi_rd_wdata <= 0;
-		end
-
-		casez (dbg_insn_opcode)
-			32'b 0000000_?????_000??_???_?????_0001011: begin // getq
-				rvfi_rs1_addr <= 0;
-				rvfi_rs1_rdata <= 0;
-			end
-			32'b 0000001_?????_?????_???_000??_0001011: begin // setq
-				rvfi_rd_addr <= 0;
-				rvfi_rd_wdata <= 0;
-			end
-			32'b 0000010_?????_00000_???_00000_0001011: begin // retirq
-				rvfi_rs1_addr <= 0;
-				rvfi_rs1_rdata <= 0;
-			end
-		endcase
-
-		if (!dbg_irq_call) begin
-			if (dbg_mem_instr) begin
-				rvfi_mem_addr <= 0;
-				rvfi_mem_rmask <= 0;
-				rvfi_mem_wmask <= 0;
-				rvfi_mem_rdata <= 0;
-				rvfi_mem_wdata <= 0;
-			end else
-			if (dbg_mem_valid && dbg_mem_ready) begin
-				rvfi_mem_addr <= dbg_mem_addr;
-				rvfi_mem_rmask <= dbg_mem_wstrb ? 0 : ~0;
-				rvfi_mem_wmask <= dbg_mem_wstrb;
-				rvfi_mem_rdata <= dbg_mem_rdata;
-				rvfi_mem_wdata <= dbg_mem_wdata;
-			end
-		end
-	end
-
-	always @* begin
-`ifdef PICORV32_TESTBUG_005
-		rvfi_pc_wdata = (dbg_irq_call ? dbg_irq_ret : dbg_insn_addr) ^ 4;
-`else
-		rvfi_pc_wdata = dbg_irq_call ? dbg_irq_ret : dbg_insn_addr;
-`endif
-
-		rvfi_csr_mcycle_rmask = 0;
-		rvfi_csr_mcycle_wmask = 0;
-		rvfi_csr_mcycle_rdata = 0;
-		rvfi_csr_mcycle_wdata = 0;
-
-		rvfi_csr_minstret_rmask = 0;
-		rvfi_csr_minstret_wmask = 0;
-		rvfi_csr_minstret_rdata = 0;
-		rvfi_csr_minstret_wdata = 0;
-
-		if (rvfi_valid && rvfi_insn[6:0] == 7'b 1110011 && rvfi_insn[13:12] == 3'b010) begin
-			if (rvfi_insn[31:20] == 12'h C00) begin
-				rvfi_csr_mcycle_rmask = 64'h 0000_0000_FFFF_FFFF;
-				rvfi_csr_mcycle_rdata = {32'h 0000_0000, rvfi_rd_wdata};
-			end
-			if (rvfi_insn[31:20] == 12'h C80) begin
-				rvfi_csr_mcycle_rmask = 64'h FFFF_FFFF_0000_0000;
-				rvfi_csr_mcycle_rdata = {rvfi_rd_wdata, 32'h 0000_0000};
-			end
-			if (rvfi_insn[31:20] == 12'h C02) begin
-				rvfi_csr_minstret_rmask = 64'h 0000_0000_FFFF_FFFF;
-				rvfi_csr_minstret_rdata = {32'h 0000_0000, rvfi_rd_wdata};
-			end
-			if (rvfi_insn[31:20] == 12'h C82) begin
-				rvfi_csr_minstret_rmask = 64'h FFFF_FFFF_0000_0000;
-				rvfi_csr_minstret_rdata = {rvfi_rd_wdata, 32'h 0000_0000};
-			end
-		end
-	end
-`endif
-
-	// Formal Verification
-`ifdef FORMAL
-	reg [3:0] last_mem_nowait;
-	always @(posedge clk)
-		last_mem_nowait <= {last_mem_nowait, mem_ready || !mem_valid};
-
-	// stall the memory interface for max 4 cycles
-	restrict property (|last_mem_nowait || mem_ready || !mem_valid);
-
-	// resetn low in first cycle, after that resetn high
-	restrict property (resetn != $initstate);
-
-	// this just makes it much easier to read traces. uncomment as needed.
-	// assume property (mem_valid || !mem_ready);
-
-	reg ok;
-	always @* begin
-		if (resetn) begin
-			// instruction fetches are read-only
-			if (mem_valid && mem_instr)
-				assert (mem_wstrb == 0);
-
-			// cpu_state must be valid
-			ok = 0;
-			if (cpu_state == cpu_state_trap)   ok = 1;
-			if (cpu_state == cpu_state_fetch)  ok = 1;
-			if (cpu_state == cpu_state_ld_rs1) ok = 1;
-			if (cpu_state == cpu_state_ld_rs2) ok = !ENABLE_REGS_DUALPORT;
-			if (cpu_state == cpu_state_exec)   ok = 1;
-			if (cpu_state == cpu_state_shift)  ok = 1;
-			if (cpu_state == cpu_state_stmem)  ok = 1;
-			if (cpu_state == cpu_state_ldmem)  ok = 1;
-			assert (ok);
-		end
-	end
-
-	reg last_mem_la_read = 0;
-	reg last_mem_la_write = 0;
-	reg [31:0] last_mem_la_addr;
-	reg [31:0] last_mem_la_wdata;
-	reg [3:0] last_mem_la_wstrb = 0;
-
-	always @(posedge clk) begin
-		last_mem_la_read <= mem_la_read;
-		last_mem_la_write <= mem_la_write;
-		last_mem_la_addr <= mem_la_addr;
-		last_mem_la_wdata <= mem_la_wdata;
-		last_mem_la_wstrb <= mem_la_wstrb;
-
-		if (last_mem_la_read) begin
-			assert(mem_valid);
-			assert(mem_addr == last_mem_la_addr);
-			assert(mem_wstrb == 0);
-		end
-		if (last_mem_la_write) begin
-			assert(mem_valid);
-			assert(mem_addr == last_mem_la_addr);
-			assert(mem_wdata == last_mem_la_wdata);
-			assert(mem_wstrb == last_mem_la_wstrb);
-		end
-		if (mem_la_read || mem_la_write) begin
-			assert(!mem_valid || mem_ready);
-		end
-	end
-`endif
 endmodule
 
 // This is a simple example implementation of PICORV32_REGS.
@@ -2577,28 +2308,6 @@ module picorv32_axi #(
 	input  [31:0] irq,
 	output [31:0] eoi,
 
-`ifdef RISCV_FORMAL
-	output        rvfi_valid,
-	output [63:0] rvfi_order,
-	output [31:0] rvfi_insn,
-	output        rvfi_trap,
-	output        rvfi_halt,
-	output        rvfi_intr,
-	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
@@ -2690,29 +2399,6 @@ 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_halt     (rvfi_halt     ),
-		.rvfi_intr     (rvfi_intr     ),
-		.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)
 	);
@@ -2863,28 +2549,6 @@ module picorv32_wb #(
 	input  [31:0] irq,
 	output [31:0] eoi,
 
-`ifdef RISCV_FORMAL
-	output        rvfi_valid,
-	output [63:0] rvfi_order,
-	output [31:0] rvfi_insn,
-	output        rvfi_trap,
-	output        rvfi_halt,
-	output        rvfi_intr,
-	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,
@@ -2955,28 +2619,6 @@ 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_halt     (rvfi_halt     ),
-		.rvfi_intr     (rvfi_intr     ),
-		.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 9d8e249..04c1946 100644
--- a/testbench.v
+++ b/testbench.v
@@ -138,28 +138,6 @@ module picorv32_wrapper #(
 		.tests_passed    (tests_passed    )
 	);
 
-`ifdef RISCV_FORMAL
-	wire        rvfi_valid;
-	wire [63:0] rvfi_order;
-	wire [31:0] rvfi_insn;
-	wire        rvfi_trap;
-	wire        rvfi_halt;
-	wire        rvfi_intr;
-	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
@@ -195,57 +173,10 @@ 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_halt      (rvfi_halt      ),
-		.rvfi_intr      (rvfi_intr      ),
-		.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
-	picorv32_rvfimon rvfi_monitor (
-		.clock          (clk           ),
-		.reset          (!resetn       ),
-		.rvfi_valid     (rvfi_valid    ),
-		.rvfi_order     (rvfi_order    ),
-		.rvfi_insn      (rvfi_insn     ),
-		.rvfi_trap      (rvfi_trap     ),
-		.rvfi_halt      (rvfi_halt     ),
-		.rvfi_intr      (rvfi_intr     ),
-		.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))