diff --git a/Makefile b/Makefile
index 0e8a862..72bf32f 100644
--- a/Makefile
+++ b/Makefile
@@ -49,7 +49,7 @@ testbench_sp.vvp: testbench.v picorv32.v
 	chmod -x testbench_sp.vvp
 
 testbench_synth.vvp: testbench.v synth.v
-	iverilog -o testbench_synth.vvp testbench.v synth.v
+	iverilog -o testbench_synth.vvp -DSYNTH_TEST testbench.v synth.v
 	chmod -x testbench_synth.vvp
 
 synth.v: picorv32.v scripts/yosys/synth_sim.ys
diff --git a/picorv32.v b/picorv32.v
index 04d845f..11f03e3 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -113,6 +113,7 @@ module picorv32 #(
 	output reg [31:0] rvfi_pre_rs2,
 	output reg [31:0] rvfi_post_pc,
 	output reg [31:0] rvfi_post_rd,
+	output reg        rvfi_post_trap,
 `endif
 
 	// Trace Interface
@@ -249,7 +250,7 @@ module picorv32 #(
 		);
 	end else begin
 		assign pcpi_mul_wr = 0;
-		assign pcpi_mul_rd = 1'bx;
+		assign pcpi_mul_rd = 32'bx;
 		assign pcpi_mul_wait = 0;
 		assign pcpi_mul_ready = 0;
 	end endgenerate
@@ -269,14 +270,14 @@ module picorv32 #(
 		);
 	end else begin
 		assign pcpi_div_wr = 0;
-		assign pcpi_div_rd = 1'bx;
+		assign pcpi_div_rd = 32'bx;
 		assign pcpi_div_wait = 0;
 		assign pcpi_div_ready = 0;
 	end endgenerate
 
 	always @* begin
 		pcpi_int_wr = 0;
-		pcpi_int_rd = 1'bx;
+		pcpi_int_rd = 32'bx;
 		pcpi_int_wait  = |{ENABLE_PCPI && pcpi_wait,  (ENABLE_MUL || ENABLE_FAST_MUL) && pcpi_mul_wait,  ENABLE_DIV && pcpi_div_wait};
 		pcpi_int_ready = |{ENABLE_PCPI && pcpi_ready, (ENABLE_MUL || ENABLE_FAST_MUL) && pcpi_mul_ready, ENABLE_DIV && pcpi_div_ready};
 
@@ -361,18 +362,18 @@ module picorv32 #(
 				mem_la_wdata = {2{reg_op2[15:0]}};
 				mem_la_wstrb = reg_op1[1] ? 4'b1100 : 4'b0011;
 				case (reg_op1[1])
-					1'b0: mem_rdata_word = mem_rdata[15: 0];
-					1'b1: mem_rdata_word = mem_rdata[31:16];
+					1'b0: mem_rdata_word = {16'b0, mem_rdata[15: 0]};
+					1'b1: mem_rdata_word = {16'b0, mem_rdata[31:16]};
 				endcase
 			end
 			2: begin
 				mem_la_wdata = {4{reg_op2[7:0]}};
 				mem_la_wstrb = 4'b0001 << reg_op1[1:0];
 				case (reg_op1[1:0])
-					2'b00: mem_rdata_word = mem_rdata[ 7: 0];
-					2'b01: mem_rdata_word = mem_rdata[15: 8];
-					2'b10: mem_rdata_word = mem_rdata[23:16];
-					2'b11: mem_rdata_word = mem_rdata[31:24];
+					2'b00: mem_rdata_word = {24'b0, mem_rdata[ 7: 0]};
+					2'b01: mem_rdata_word = {24'b0, mem_rdata[15: 8]};
+					2'b10: mem_rdata_word = {24'b0, mem_rdata[23:16]};
+					2'b11: mem_rdata_word = {24'b0, mem_rdata[31:24]};
 				endcase
 			end
 		endcase
@@ -390,14 +391,14 @@ module picorv32 #(
 					case (mem_rdata_latched[15:13])
 						3'b000: begin // C.ADDI4SPN
 							mem_rdata_q[14:12] <= 3'b000;
-							mem_rdata_q[31:20] <= {mem_rdata_latched[10:7], mem_rdata_latched[12:11], mem_rdata_latched[5], mem_rdata_latched[6], 2'b00};
+							mem_rdata_q[31:20] <= {2'b0, mem_rdata_latched[10:7], mem_rdata_latched[12:11], mem_rdata_latched[5], mem_rdata_latched[6], 2'b00};
 						end
 						3'b010: begin // C.LW
-							mem_rdata_q[31:20] <= {mem_rdata_latched[5], mem_rdata_latched[12:10], mem_rdata_latched[6], 2'b00};
+							mem_rdata_q[31:20] <= {5'b0, mem_rdata_latched[5], mem_rdata_latched[12:10], mem_rdata_latched[6], 2'b00};
 							mem_rdata_q[14:12] <= 3'b 010;
 						end
 						3'b 110: begin // C.SW
-							{mem_rdata_q[31:25], mem_rdata_q[11:7]} <= {mem_rdata_latched[5], mem_rdata_latched[12:10], mem_rdata_latched[6], 2'b00};
+							{mem_rdata_q[31:25], mem_rdata_q[11:7]} <= {5'b0, mem_rdata_latched[5], mem_rdata_latched[12:10], mem_rdata_latched[6], 2'b00};
 							mem_rdata_q[14:12] <= 3'b 010;
 						end
 					endcase
@@ -463,7 +464,7 @@ module picorv32 #(
 							mem_rdata_q[14:12] <= 3'b 001;
 						end
 						3'b010: begin // C.LWSP
-							mem_rdata_q[31:20] <= {mem_rdata_latched[3:2], mem_rdata_latched[12], mem_rdata_latched[6:4], 2'b00};
+							mem_rdata_q[31:20] <= {4'b0, mem_rdata_latched[3:2], mem_rdata_latched[12], mem_rdata_latched[6:4], 2'b00};
 							mem_rdata_q[14:12] <= 3'b 010;
 						end
 						3'b100: begin
@@ -485,7 +486,7 @@ module picorv32 #(
 							end
 						end
 						3'b110: begin // C.SWSP
-							{mem_rdata_q[31:25], mem_rdata_q[11:7]} <= {mem_rdata_latched[8:7], mem_rdata_latched[12:9], 2'b00};
+							{mem_rdata_q[31:25], mem_rdata_q[11:7]} <= {4'b0, mem_rdata_latched[8:7], mem_rdata_latched[12:9], 2'b00};
 							mem_rdata_q[14:12] <= 3'b 010;
 						end
 					endcase
@@ -1863,13 +1864,14 @@ module picorv32 #(
 
 `ifdef RISCV_FORMAL
 	always @(posedge clk) begin
-		rvfi_valid <= resetn && launch_next_insn && dbg_valid_insn;
+		rvfi_valid <= resetn && (launch_next_insn || trap) && dbg_valid_insn;
 		rvfi_insn <= dbg_insn_opcode;
 		rvfi_rs1 <= dbg_rs1val_valid ? dbg_insn_rs1 : 0;
 		rvfi_rs2 <= dbg_rs2val_valid ? dbg_insn_rs2 : 0;
 		rvfi_pre_pc <= dbg_insn_addr;
 		rvfi_pre_rs1 <= dbg_rs1val_valid ? dbg_rs1val : 0;
 		rvfi_pre_rs2 <= dbg_rs2val_valid ? dbg_rs2val : 0;
+		rvfi_post_trap <= trap;
 
 		if (!resetn) begin
 			rvfi_rd <= 0;
diff --git a/scripts/yosys/synth_sim.ys b/scripts/yosys/synth_sim.ys
index b64e7e1..ded89d9 100644
--- a/scripts/yosys/synth_sim.ys
+++ b/scripts/yosys/synth_sim.ys
@@ -1,7 +1,8 @@
 # yosys synthesis script for post-synthesis simulation (make test_synth)
 
 read_verilog picorv32.v
-chparam -set ENABLE_IRQ 1 -set ENABLE_MUL 1 picorv32_axi
+chparam -set COMPRESSED_ISA 1 -set ENABLE_MUL 1 -set ENABLE_DIV 1 \
+        -set ENABLE_IRQ 1 -set ENABLE_TRACE 1 picorv32_axi
 hierarchy -top picorv32_axi
 synth
 write_verilog synth.v
diff --git a/testbench.v b/testbench.v
index 18cce40..84a2fd0 100644
--- a/testbench.v
+++ b/testbench.v
@@ -139,6 +139,7 @@ module picorv32_wrapper #(
 	);
 
 	picorv32_axi #(
+`ifndef SYNTH_TEST
 `ifdef SP_TEST
 		.ENABLE_REGS_DUALPORT(0),
 `endif
@@ -149,6 +150,7 @@ module picorv32_wrapper #(
 		.ENABLE_DIV(1),
 		.ENABLE_IRQ(1),
 		.ENABLE_TRACE(1)
+`endif
 	) uut (
 		.clk            (clk            ),
 		.resetn         (resetn         ),