Added formal verification set to timer internally

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

@@ -17,7 +17,9 @@ module formal_wb_timer;
 
     assign i_wb_rst = 1'b0;
 
-    wb_countdown_timer dut (
+    wb_countdown_timer #(
+        .FORMAL(1)
+    ) dut (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .o_irq(o_irq),
@@ -32,7 +34,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

@@ -1,7 +1,8 @@
 `timescale 1ns/1ps
 
 module wb_countdown_timer #(
-    parameter address = 32'h00000000 // Base address of peripheral
+    parameter address = 32'h00000000, // Base address of peripheral
+    parameter FORMAL = 0
 )(
     input  wire         i_clk,
     input  wire         i_rst,
@@ -97,4 +98,91 @@ module wb_countdown_timer #(
         end
     end
 
+    // 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;
+
+        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
+    end;
+
 endmodule