Made timer synthesizable

check_formal.sh

@@ -55,7 +55,7 @@ $label"
 $label"
 		printf 'Result: FAIL (%s)\n' "$label"
 		printf 'Captured log for %s:\n' "$label"
-		cat "$log_file" | grep summary
+		cat "$log_file" #| grep summary
 		rm -f "$log_file"
 		return 1
 	fi

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -32,7 +32,7 @@ module formal_wb_timer;
     );
 
     formal_wb_slave_checker #(
-        .combinatorial_ack(0)
+        .combinatorial_ack(0),
     ) wb_checker (
         .i_clk(i_clk),
         .i_rst(i_rst),

cores/wb/wb_timer/rtl/wb_timer.v

@@ -97,4 +97,91 @@ module wb_countdown_timer #(
         end
     end
 
+`ifdef FORMAL
+    // Formal verification
+    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));
+
+    end
+`endif
+
 endmodule

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