diff --git a/picorv32.v b/picorv32.v
index e6fde6d..b6c8707 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -34,7 +34,7 @@
   `define assert(assert_expr) assert(assert_expr)
 `else
   `define FORMAL_KEEP
-  `define assert(assert_expr)
+  `define assert(assert_expr) empty_statement
 `endif
 
 /***************************************************************
@@ -176,6 +176,12 @@ module picorv32 #(
 		end
 	end
 
+	task empty_statement;
+		// This task is used by the `assert directive in non-formal mode to
+		// avoid empty statement (which are unsupported by plain Verilog syntax).
+		begin end
+	endtask
+
 `ifdef DEBUGREGS
 	wire [31:0] dbg_reg_x0  = cpuregs[0];
 	wire [31:0] dbg_reg_x1  = cpuregs[1];
diff --git a/testbench.v b/testbench.v
index 84a2fd0..e113265 100644
--- a/testbench.v
+++ b/testbench.v
@@ -12,7 +12,6 @@ module testbench #(
 	parameter AXI_TEST = 0,
 	parameter VERBOSE = 0
 );
-
 	reg clk = 1;
 	reg resetn = 0;
 	wire trap;
@@ -75,8 +74,6 @@ module picorv32_wrapper #(
 	output trace_valid,
 	output [35:0] trace_data
 );
-
-	wire trap;
 	wire tests_passed;
 	reg [31:0] irq;
 
@@ -234,7 +231,6 @@ module axi4_memory #(
 
 	output reg tests_passed
 );
-
 	reg [31:0]   memory [0:64*1024/4-1] /* verilator public */;
 	reg verbose;
 	initial verbose = $test$plusargs("verbose") || VERBOSE;