From 5b940758b633e77311b8e487ccd1ab8812ac6813 Mon Sep 17 00:00:00 2001 From: Joppe Blondel Date: Sun, 1 Mar 2026 21:00:57 +0100 Subject: [PATCH] Added formal verification set to timer internally --- check_formal.sh | 2 +- cores/wb/wb_timer/formal/formal_wb_timer.v | 6 +- cores/wb/wb_timer/rtl/wb_timer.v | 90 +++++++++++++++++++++- 3 files changed, 94 insertions(+), 4 deletions(-) diff --git a/check_formal.sh b/check_formal.sh index 9155dd7..302fbf3 100755 --- a/check_formal.sh +++ b/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 diff --git a/cores/wb/wb_timer/formal/formal_wb_timer.v b/cores/wb/wb_timer/formal/formal_wb_timer.v index ee82a09..0a1250c 100644 --- a/cores/wb/wb_timer/formal/formal_wb_timer.v +++ b/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), diff --git a/cores/wb/wb_timer/rtl/wb_timer.v b/cores/wb/wb_timer/rtl/wb_timer.v index 0370c3a..ff37dbc 100644 --- a/cores/wb/wb_timer/rtl/wb_timer.v +++ b/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