joppe/fpga_modem
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Made timer synthesizable

Browse Source
This commit is contained in:
Joppe Blondel
2026-03-01 21:11:08 +01:00
parent 5b940758b6
commit a6a5c6ea3f
3 changed files with 89 additions and 87 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
cores/wb/wb_timer/formal/formal_wb_timer.v
View File

@@ -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),

167
cores/wb/wb_timer/rtl/wb_timer.v
View File

@@ -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

5
cores/wb/wb_timer/wb_timer.core
View File

@@ -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