diff --git a/cores/wb/wb_timer/formal/formal_wb_timer.v b/cores/wb/wb_timer/formal/formal_wb_timer.v
index 0a1250c..931dd27 100644
--- a/cores/wb/wb_timer/formal/formal_wb_timer.v
+++ b/cores/wb/wb_timer/formal/formal_wb_timer.v
@@ -17,9 +17,7 @@ module formal_wb_timer;
 
     assign i_wb_rst = 1'b0;
 
-    wb_countdown_timer #(
-        .FORMAL(1)
-    ) dut (
+    wb_countdown_timer dut (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .o_irq(o_irq),
diff --git a/cores/wb/wb_timer/rtl/wb_timer.v b/cores/wb/wb_timer/rtl/wb_timer.v
index ff37dbc..87f559c 100644
--- a/cores/wb/wb_timer/rtl/wb_timer.v
+++ b/cores/wb/wb_timer/rtl/wb_timer.v
@@ -1,8 +1,7 @@
 `timescale 1ns/1ps
 
 module wb_countdown_timer #(
-    parameter address = 32'h00000000, // Base address of peripheral
-    parameter FORMAL = 0
+    parameter address = 32'h00000000 // Base address of peripheral
 )(
     input  wire         i_clk,
     input  wire         i_rst,
@@ -98,91 +97,91 @@ module wb_countdown_timer #(
         end
     end
 
+`ifdef FORMAL
     // Formal verification
-    if(FORMAL) begin
-        reg f_past_valid = 1'b0;
-        wire cnt_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h0);
-        wire pld_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h4);
-        wire ack_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h8);
-        reg [31:0] past_counter;
+    reg f_past_valid = 1'b0;
+    wire cnt_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h0);
+    wire pld_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h4);
+    wire ack_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h8);
+    reg [31:0] past_counter;
 
-        always @(posedge i_clk) begin
-            f_past_valid <= 1'b1;
-            past_counter <= counter;
-
-            // R1: Reset clears all timer state on the following cycle.
-            // Check counter, preload, wb_ack, o_wb_dat, irq_fired,
-            // counter_started, counter_running, and prev_counter_running.
-            if(f_past_valid && $past(i_rst)) begin
-                R1s1: assert(counter==0);
-                R1s2: assert(preload==0);
-                R1s3: assert(!wb_ack);
-                R1s4: assert(o_wb_dat==0);
-                R1s5: assert(!irq_fired);
-                R1s6: assert(!counter_started);
-                R1s7: assert(!counter_running);
-            end
-
-            // R2: irq_fired is sticky until reset or a write to BASE+8 clears it.
-            // -> if last cycle was irq and last cycle was not reset and not ack write then now still irq
-            if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(!ack_write))
-                R2: assert(irq_fired);
-
-            // R3: A write to BASE+8 clears irq_fired on the following cycle.
-            // -> if last cycle was ack write and irq was high it must be low now
-            if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(ack_write))
-                R3: assert(!irq_fired);
-
-            // R4: While the timer is running and no counter write overrides it,
-            // counter decrements by exactly one each cycle.
-            if(f_past_valid && $past(!i_rst) && $past(counter>1) && $past(counter_started) && $past(!cnt_write))
-                R4: assert(counter == $past(counter)-1);
-
-            // R5: When counter reaches zero with preload > 0 and the timer is started,
-            // the counter reloads from preload.
-            if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && $past(counter_started) && $past(!cnt_write))
-                R5: assert(counter == $past(preload));
-
-            // R6: When counter == 0 and preload == 0, the timer stops
-            // (counter_started deasserts unless a write rearms it).
-            if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload==0) && $past(!cnt_write) && $past(!pld_write)) begin
-                R6s1: assert(counter==0);
-                R6s2: assert(counter_started==0);
-            end
-
-            // R7: A write to BASE+0 or BASE+4 arms the timer
-            // (counter_started asserts on the following cycle).
-            if(f_past_valid && $past(!i_rst) && ($past(cnt_write) || $past(pld_write)))
-                R7: assert(counter_started==1);
-
-            // R8: o_irq always reflects irq_fired.
-            R8: assert(o_irq == irq_fired);
-
-            // R9: Interrupt only fired after counter was 0 two clock cycles ago
-            if(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired)
-                R9: assert($past(past_counter) == 0);
-
-            // C1: Cover a counter write that starts the timer.
-            C1s1: cover(f_past_valid && !i_rst && cnt_write);
-            if(f_past_valid && $past(!i_rst) && $past(cnt_write))
-                C1s2: cover(counter_started);
-
-            // C2: Cover a preload write.
-            C2: cover(f_past_valid && !i_rst && pld_write);
-
-            // C3: Cover the counter decrementing at least once.
-            C3: cover(f_past_valid && $past(!i_rst) && $past(counter)==counter-1 && $past(!cnt_write) && $past(!pld_write));
-
-            // C4: Cover the counter reloading from preload.
-            C4: cover(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && counter>0 && $past(!cnt_write) && $past(!pld_write));
-
-            // C5: Cover irq_fired asserting when the timer expires.
-            C5: cover(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired && $past(counter==0));
-
-            // C6: Cover irq_fired being cleared by a write to BASE+8.
-            C6: cover(f_past_valid && $past(!i_rst) && $past(irq_fired) && !irq_fired && $past(ack_write));
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+        past_counter <= counter;
 
+        // R1: Reset clears all timer state on the following cycle.
+        // Check counter, preload, wb_ack, o_wb_dat, irq_fired,
+        // counter_started, counter_running, and prev_counter_running.
+        if(f_past_valid && $past(i_rst)) begin
+            R1s1: assert(counter==0);
+            R1s2: assert(preload==0);
+            R1s3: assert(!wb_ack);
+            R1s4: assert(o_wb_dat==0);
+            R1s5: assert(!irq_fired);
+            R1s6: assert(!counter_started);
+            R1s7: assert(!counter_running);
         end
-    end;
+
+        // R2: irq_fired is sticky until reset or a write to BASE+8 clears it.
+        // -> if last cycle was irq and last cycle was not reset and not ack write then now still irq
+        if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(!ack_write))
+            R2: assert(irq_fired);
+
+        // R3: A write to BASE+8 clears irq_fired on the following cycle.
+        // -> if last cycle was ack write and irq was high it must be low now
+        if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(ack_write))
+            R3: assert(!irq_fired);
+
+        // R4: While the timer is running and no counter write overrides it,
+        // counter decrements by exactly one each cycle.
+        if(f_past_valid && $past(!i_rst) && $past(counter>1) && $past(counter_started) && $past(!cnt_write))
+            R4: assert(counter == $past(counter)-1);
+
+        // R5: When counter reaches zero with preload > 0 and the timer is started,
+        // the counter reloads from preload.
+        if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && $past(counter_started) && $past(!cnt_write))
+            R5: assert(counter == $past(preload));
+
+        // R6: When counter == 0 and preload == 0, the timer stops
+        // (counter_started deasserts unless a write rearms it).
+        if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload==0) && $past(!cnt_write) && $past(!pld_write)) begin
+            R6s1: assert(counter==0);
+            R6s2: assert(counter_started==0);
+        end
+
+        // R7: A write to BASE+0 or BASE+4 arms the timer
+        // (counter_started asserts on the following cycle).
+        if(f_past_valid && $past(!i_rst) && ($past(cnt_write) || $past(pld_write)))
+            R7: assert(counter_started==1);
+
+        // R8: o_irq always reflects irq_fired.
+        R8: assert(o_irq == irq_fired);
+
+        // R9: Interrupt only fired after counter was 0 two clock cycles ago
+        if(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired)
+            R9: assert($past(past_counter) == 0);
+
+        // C1: Cover a counter write that starts the timer.
+        C1s1: cover(f_past_valid && !i_rst && cnt_write);
+        if(f_past_valid && $past(!i_rst) && $past(cnt_write))
+            C1s2: cover(counter_started);
+
+        // C2: Cover a preload write.
+        C2: cover(f_past_valid && !i_rst && pld_write);
+
+        // C3: Cover the counter decrementing at least once.
+        C3: cover(f_past_valid && $past(!i_rst) && $past(counter)==counter-1 && $past(!cnt_write) && $past(!pld_write));
+
+        // C4: Cover the counter reloading from preload.
+        C4: cover(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && counter>0 && $past(!cnt_write) && $past(!pld_write));
+
+        // C5: Cover irq_fired asserting when the timer expires.
+        C5: cover(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired && $past(counter==0));
+
+        // C6: Cover irq_fired being cleared by a write to BASE+8.
+        C6: cover(f_past_valid && $past(!i_rst) && $past(irq_fired) && !irq_fired && $past(ack_write));
+
+    end
+`endif
 
 endmodule
diff --git a/cores/wb/wb_timer/wb_timer.core b/cores/wb/wb_timer/wb_timer.core
index 91a294b..193254f 100644
--- a/cores/wb/wb_timer/wb_timer.core
+++ b/cores/wb/wb_timer/wb_timer.core
@@ -45,9 +45,14 @@ targets:
         toplevel: formal_wb_timer
         parameters:
             - address
+            - FORMAL=true
 
 parameters:
     address:
         datatype: int
         description: Base address of register set
         paramtype: vlogparam
+    FORMAL:
+        datatype: bool
+        description: Enable in-module formal-only logic
+        paramtype: vlogdefine