Made timer synthesizable

.gitignore

@@ -1 +1,2 @@
 build/
+out/

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "fusesoc_libraries/serv"]
 	path = fusesoc_libraries/serv
-	url = https://github.com/Jojojoppe/serv/tree/xilinx_ise
+	url = git@github.com:Jojojoppe/serv.git
 [submodule "fusesoc_libraries/fusesoc-cores"]
 	path = fusesoc_libraries/fusesoc-cores
 	url = https://github.com/fusesoc/fusesoc-cores

check_formal.sh

@@ -9,6 +9,10 @@ joppeb:wb:jtag_wb_bridge
 joppeb:wb:wb_timer
 "
 
+if [ -n "$1" ]; then
+	CORES="$1"
+fi
+
 # Add or remove formal tasks here.
 TASKS="
 bmc
@@ -51,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/system/mcu/rtl/mcu_peripherals.v

@@ -44,7 +44,9 @@ module mcu_peripherals (
     wire [31:0] gpio_wbs_dat_r;
     wire gpio_wbs_ack;
 
+    wire [31:0] timer_wbs_adr = wbs_adr[1*32 +: 32];
     wire [31:0] timer_wbs_dat_w = wbs_dat_w[1*32 +: 32];
+    wire [3:0] timer_wbs_sel = wbs_sel[1*4 +: 4];
     wire timer_wbs_we = wbs_we[1];
     wire timer_wbs_cyc = wbs_cyc[1];
     wire timer_wbs_stb = wbs_stb[1];
@@ -108,12 +110,16 @@ module mcu_peripherals (
     assign wbs_dat_r[0*32 +: 32] = gpio_wbs_dat_r;
     assign wbs_ack[0] = gpio_wbs_ack;
 
-    wb_countdown_timer timer (
+    wb_countdown_timer #(
+        .address(TIMER_BASE_ADDR)
+    ) timer (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .o_irq(o_timer_irq),
+        .i_wb_adr(timer_wbs_adr),
         .i_wb_dat(timer_wbs_dat_w),
         .o_wb_dat(timer_wbs_dat_r),
+        .i_wb_sel(timer_wbs_sel),
         .i_wb_we(timer_wbs_we),
         .i_wb_cyc(timer_wbs_cyc),
         .i_wb_stb(timer_wbs_stb),

cores/system/test/rtl/toplevel.v

@@ -1,7 +1,8 @@
 `timescale 1ns/1ps
 
 module toplevel #(
-    parameter sim = 0
+    parameter sim = 0,
+    parameter memfile = "sweep.hex"
 )(
     input wire aclk,
     input wire aresetn,
@@ -57,7 +58,7 @@ module toplevel #(
     wire test;
 
     mcu #(
-        .memfile("../sw/sweep/sweep.hex"),
+        .memfile(memfile),
         .sim(sim),
         .jtag(1)
     ) mcu (

cores/system/test/sw/sweep/sweep.c

@@ -6,7 +6,9 @@ static volatile uint32_t * const LEDS       = (volatile uint32_t *)(GPIO_BASE+4)
 static volatile uint32_t * const LEDGR      = (volatile uint32_t *)(GPIO_BASE+8);
 
 #define TIMER_BASE  0x40010000u
-static volatile uint32_t * const TIMER      = (volatile uint32_t *)(TIMER_BASE+0);
+static volatile uint32_t * const TIMER_CNT  = (volatile uint32_t *)(TIMER_BASE+0);
+static volatile uint32_t * const TIMER_LD   = (volatile uint32_t *)(TIMER_BASE+4);
+static volatile uint32_t * const TIMER_ACK  = (volatile uint32_t *)(TIMER_BASE+8);
 
 #define MSTATUS_MIE (1u << 3)
 #define MIE_MTIE    (1u << 7)
@@ -25,21 +27,21 @@ static inline void irq_init() {
 }
 
 void timer_isr(){
-    static int set = 0;
+    *TIMER_ACK = 1;
-    *TIMER = 1840000*8;
     *LEDGR = ~(*LEDGR);
 }
 
 void main(){
     irq_init();
 
-    *LEDGR = 3;
+    *LEDGR = 1;
-    *TIMER = 1840000*2;
+    *TIMER_LD = 2 * 15000000/1000;
 
     for(;;){
-        for(int i=1000; i<10000; i++){
+        for(int i=1000; i<10000; i+=10){
             *R_FREQ = i;
-            for(int j=0; j<80; j++) asm volatile("nop");
+            *LEDS = i>>4;
+            // for(int j=0; j<80; j++) asm volatile("nop");
         }
     }
 }

cores/system/test/tb/tb_toplevel.v

@@ -0,0 +1,37 @@
+`timescale 1ns/1ps
+
+module tb_toplevel;
+    reg        aclk;
+    reg        aresetn;
+    wire       led_green;
+    wire       led_red;
+    wire [5:0] r2r;
+    wire [7:0] LED;
+
+    toplevel #(
+        .sim(1)
+    ) dut (
+        .aclk(aclk),
+        .aresetn(aresetn),
+        .led_green(led_green),
+        .led_red(led_red),
+        .r2r(r2r),
+        .LED(LED)
+    );
+
+    initial aclk = 1'b0;
+    always #33.33 aclk = ~aclk;
+
+    initial begin
+        $dumpfile("toplevel.vcd");
+        $dumpvars(1, tb_toplevel);
+
+        aresetn = 1'b0;
+        #100;
+        aresetn = 1'b1;
+
+        #10_000_000;
+
+        $finish;
+    end
+endmodule

cores/system/test/test.core

@@ -13,10 +13,14 @@ filesets:
         files:
             - rtl/toplevel.v
         file_type: verilogSource
+    tb:
+        files:
+            - tb/tb_toplevel.v
+        file_type: verilogSource
 
     sw:
         files:
-            - sw/sweep/sweep.hex
+            - sw/sweep/sweep.hex : {copyto : sweep.hex}
         file_type: user
 
     mimas:
@@ -29,6 +33,13 @@ targets:
         filesets:
             - rtl
         toplevel: toplevel
+    sim:
+        default_tool: icarus
+        filesets:
+            - rtl
+            - sw
+            - tb
+        toplevel: tb_toplevel
 
     mimas:
         filesets:

cores/wb/formal_checker/formal/formal_wb_master_checker.v

@@ -22,14 +22,14 @@ module formal_wb_master_checker (
 
         // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
         if(o_wb_ack)
-            assume(
+            A1: assume(
                 (i_wb_cyc && i_wb_stb) ||
                 (f_past_valid && $past(i_wb_cyc && i_wb_stb))
             );
 
         // A2: Slave must not ACK outside an active cycle
         if(!i_wb_cyc)
-            assume(!o_wb_ack);
+            A2: assume(!o_wb_ack);
 
         // A3: Once STB has been low for a full cycle, slave ACK must be low
         if(
@@ -37,19 +37,19 @@ module formal_wb_master_checker (
             !$past(i_wb_stb) &&
             !i_wb_stb
         )
-            assume(!o_wb_ack);
+            A3: assume(!o_wb_ack);
 
         // R1: Reset must leave the master initialized on the following cycle
         if(f_past_valid && $past(i_rst || i_wb_rst)) begin
-            assert(!i_wb_cyc);
+            R1: assert(!i_wb_cyc);
-            assert(!i_wb_stb);
+            R2: assert(!i_wb_stb);
         end
 
-        // R2: STB never high without CYC
+        // R3: STB never high without CYC
         if(i_wb_stb)
-            assert(i_wb_cyc);
+            R3: assert(i_wb_cyc);
 
-        // R3: Once a request starts, hold it stable until the slave responds
+        // R4-R9: Once a request starts, hold it stable until the slave responds
         if(
             f_past_valid &&
             !$past(i_rst || i_wb_rst) &&
@@ -57,40 +57,40 @@ module formal_wb_master_checker (
             !o_wb_ack &&
             !(i_rst || i_wb_rst)
         ) begin
-            assert(i_wb_cyc);
+            R4: assert(i_wb_cyc);
-            assert(i_wb_stb);
+            R5: assert(i_wb_stb);
-            assert(i_wb_adr == $past(i_wb_adr));
+            R6: assert(i_wb_adr == $past(i_wb_adr));
-            assert(i_wb_dat == $past(i_wb_dat));
+            R7: assert(i_wb_dat == $past(i_wb_dat));
-            assert(i_wb_sel == $past(i_wb_sel));
+            R8: assert(i_wb_sel == $past(i_wb_sel));
-            assert(i_wb_we == $past(i_wb_we));
+            R9: assert(i_wb_we == $past(i_wb_we));
         end
 
-        // R4: Once CYC is low, STB must also be low
+        // R10: Once CYC is low, STB must also be low
         if(!i_wb_cyc)
-            assert(!i_wb_stb);
+            R10: assert(!i_wb_stb);
 
-        // C0: We eventually initiate a request
+        // C1: We eventually initiate a request
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+        C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
 
-        // C1: We eventually get an ACK during an active request
+        // C2: We eventually get an ACK during an active request
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+        C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
 
-        // C2: A delayed ACK occurs for a request issued in a previous cycle.
+        // C3: A delayed ACK occurs for a request issued in a previous cycle.
         // This does not require the request to drop in the ACK cycle.
-        cover(f_past_valid && !i_rst && !i_wb_rst &&
+        C3: cover(f_past_valid && !i_rst && !i_wb_rst &&
             $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
 
         // C4: A “wait state” happens: request asserted, no ACK for at least 1 cycle
-        cover(f_past_valid && !i_rst && !i_wb_rst &&
+        C4: cover(f_past_valid && !i_rst && !i_wb_rst &&
             $past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
             (i_wb_cyc && i_wb_stb && !o_wb_ack));
 
-        // C5: Read and write both occur (even if only once each)
+        // C5-C6: Read and write both occur (even if only once each)
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
+        C5: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
+        C6: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
 
-        // C6: A transfer completes and the master drops CYC sometime after
+        // C7: A transfer completes and the master drops CYC sometime after
-        cover(f_past_valid && !i_rst && !i_wb_rst &&
+        C7: cover(f_past_valid && !i_rst && !i_wb_rst &&
             $past(i_wb_cyc && i_wb_stb && o_wb_ack) && !i_wb_cyc);
 
     end

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,7 +1,8 @@
 `timescale 1ns/1ps
 
 module formal_wb_slave_checker #(
-    parameter combinatorial_ack = 0
+    parameter combinatorial_ack = 0,
+    parameter expect_wait_state = 0
 ) (
     input wire        i_clk,
     input wire        i_rst,
@@ -24,38 +25,38 @@ module formal_wb_slave_checker #(
 
         // A1: Reset forces cyc=0, stb=0
         if (i_rst) begin
-            assume(!i_wb_cyc);
+            A1: assume(!i_wb_cyc);
-            assume(!i_wb_stb);
+            A2: assume(!i_wb_stb);
         end
 
-        // A2: std->cyc, stb never high without cyc
+        // A3: std->cyc, stb never high without cyc
         if(i_wb_stb)
-            assume(i_wb_cyc);
+            A3: assume(i_wb_cyc);
 
-        // A3: once a request starts, hold it stable until the slave responds
+        // A4-A9: once a request starts, hold it stable until the slave responds
         if(f_past_valid && $past(i_wb_cyc && i_wb_stb && !o_wb_ack)) begin
-            assume(i_wb_cyc);
+            A4: assume(i_wb_cyc);
-            assume(i_wb_stb);
+            A5: assume(i_wb_stb);
-            assume(i_wb_adr == $past(i_wb_adr));
+            A6: assume(i_wb_adr == $past(i_wb_adr));
-            assume(i_wb_dat == $past(i_wb_dat));
+            A7: assume(i_wb_dat == $past(i_wb_dat));
-            assume(i_wb_sel == $past(i_wb_sel));
+            A8: assume(i_wb_sel == $past(i_wb_sel));
-            assume(i_wb_we == $past(i_wb_we));
+            A9: assume(i_wb_we == $past(i_wb_we));
         end
 
         // R1: ACK must correspond to either a same-cycle or previous-cycle request
         if(o_wb_ack)
-            assert(
+            R1: assert(
                 (i_wb_cyc && i_wb_stb) ||
                 (f_past_valid && $past(i_wb_cyc && i_wb_stb))
             );
 
         // R2: !CYC->!ACK : no ghost acks
         if(!i_wb_cyc)
-            assert(!o_wb_ack);
+            R2: assert(!o_wb_ack);
 
         // R3: Reset must leave the slave initialized on the following cycle
         if(f_past_valid && $past(i_rst || i_wb_rst))
-            assert(!o_wb_ack);
+            R3: assert(!o_wb_ack);
 
         // R4: once STB has been dropped for a full cycle, ACK must be low
         if(
@@ -63,34 +64,35 @@ module formal_wb_slave_checker #(
             !$past(i_wb_stb) &&
             !i_wb_stb
         )
-            assert(!o_wb_ack);
+            R4: assert(!o_wb_ack);
 
-        // C0: A request occurs at all
+        // C1: A request occurs at all
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+        C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
 
-        // C1: A request with write and with read occur
+        // C2-C3: A request with write and with read occur
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
+        C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
+        C3: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
 
-        // C2: ACK happens during a request (basic progress)
+        // C4: ACK happens during a request (basic progress)
-        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+        C4: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
 
-        // C3: Exercise the expected ACK timing style for this slave.
+        // C5-C7: Exercise the expected ACK timing style for this slave.
         if (combinatorial_ack) begin
-            cover(f_past_valid && !i_rst && !i_wb_rst &&
+            C5: cover(f_past_valid && !i_rst && !i_wb_rst &&
                 (i_wb_cyc && i_wb_stb) && o_wb_ack);
         end else begin
-            cover(f_past_valid && !i_rst && !i_wb_rst &&
+            C6: cover(f_past_valid && !i_rst && !i_wb_rst &&
                 $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
 
-            // C4: Wait-state behavior for registered/non-zero-wait slaves.
+            // C7: Optional wait-state behavior for slaves that intentionally stall.
-            cover(f_past_valid && !i_rst && !i_wb_rst &&
+            if (expect_wait_state)
+                C7: cover(f_past_valid && !i_rst && !i_wb_rst &&
                     $past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
                     (i_wb_cyc && i_wb_stb && !o_wb_ack));
         end
 
-        // C5: Master ends a cycle (CYC drops) after at least one request
+        // C8: Master ends a cycle (CYC drops) after at least one request
-        cover(f_past_valid && !i_rst && !i_wb_rst &&
+        C8: cover(f_past_valid && !i_rst && !i_wb_rst &&
             $past(i_wb_cyc && i_wb_stb) && !i_wb_cyc);
             
     end

cores/wb/wb_gpio/formal/wb_gpio/config.sby

@@ -1,13 +0,0 @@
-[options]
-mode prove
-depth 8
-
-[engines]
-smtbmc z3 parallel.enable=true parallel.threads.max=8
-
-[script]
-{{"-formal"|gen_reads}}
-prep -top {{top_level}}
-
-[files]
-{{files}}

cores/wb/wb_gpio/formal/wb_gpio/logfile.txt

@@ -1,2 +0,0 @@
-SBY 17:32:33 [cores/wb/wb_gpio/formal/wb_gpio] Removing directory '/data/joppe/projects/fusesoc_test/cores/wb/wb_gpio/formal/wb_gpio'.
-SBY 17:32:33 [cores/wb/wb_gpio/formal/wb_gpio] Copy '/data/joppe/projects/fusesoc_test/{{files}}' to '/data/joppe/projects/fusesoc_test/cores/wb/wb_gpio/formal/wb_gpio/src/{{files}}'.

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -1,9 +1,6 @@
 `timescale 1ns/1ps
 
-module formal_wb_timer #(
+module formal_wb_timer;
-    parameter WIDTH = 8,
-    parameter DIVIDER = 0
-);
     (* gclk *) reg        i_clk;
     (* anyseq *) reg      i_rst;
     (* anyseq *) reg [31:0] i_wb_adr;
@@ -20,15 +17,14 @@ module formal_wb_timer #(
 
     assign i_wb_rst = 1'b0;
 
-    wb_countdown_timer #(
+    wb_countdown_timer dut (
-        .WIDTH(WIDTH),
-        .DIVIDER(DIVIDER)
-    ) dut (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .o_irq(o_irq),
+        .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
         .o_wb_dat(o_wb_dat),
+        .i_wb_sel(i_wb_sel),
         .i_wb_we(i_wb_we),
         .i_wb_cyc(i_wb_cyc),
         .i_wb_stb(i_wb_stb),
@@ -36,7 +32,7 @@ module formal_wb_timer #(
     );
 
     formal_wb_slave_checker #(
-        .combinatorial_ack(1)
+        .combinatorial_ack(0),
     ) wb_checker (
         .i_clk(i_clk),
         .i_rst(i_rst),

cores/wb/wb_timer/formal/wb_timer.sby

@@ -13,7 +13,7 @@ prove: mode prove
 [engines]
 bmc: smtbmc yices
 cover: smtbmc yices
-prove: abc pdr
+prove: smtbmc yices
 
 [script]
 {{"-formal"|gen_reads}}

cores/wb/wb_timer/rtl/wb_timer.v

@@ -1,74 +1,187 @@
 `timescale 1ns/1ps
 
 module wb_countdown_timer #(
-    parameter WIDTH   = 32,  // counter width (<=32 makes bus mapping easy)
+    parameter address = 32'h00000000 // Base address of peripheral
-    parameter DIVIDER = 0    // optional prescaler: tick every 2^DIVIDER cycles
 )(
     input  wire         i_clk,
     input  wire         i_rst,
-    output reg          o_irq,
+    output wire         o_irq,
 
+    input  wire [31:0]  i_wb_adr,
     input  wire [31:0]  i_wb_dat,
     output reg  [31:0]  o_wb_dat,
+    input  wire [3:0]   i_wb_sel,
     input  wire         i_wb_we,
     input  wire         i_wb_cyc,
     input  wire         i_wb_stb,
     output wire         o_wb_ack
 );
 
-    // One-cycle acknowledge on any valid WB access
+    // Registers
-    // (classic, zero-wait-state peripheral)
+    reg [31:0]       counter; // The actual counter. Generates an interrupt when it reaches 0
-    assign o_wb_ack = i_wb_cyc & i_wb_stb;
+    reg [31:0]       preload; // The value with which the counter gets loaded after it reaches 0. 0 to keep the timer off
 
-    // Internal countdown and prescaler
+    reg wb_ack = 0;
-    reg [WIDTH-1:0] counter;
+    reg irq_fired = 0;
-    reg [DIVIDER:0] presc;   // enough bits to count up to 2^DIVIDER-1
+    reg counter_started = 0;
-    wire tick = (DIVIDER == 0) ? 1'b1 : (presc[DIVIDER] == 1'b1);
+    reg counter_running = 0;
+    reg prev_counter_running = 0;
+    assign o_wb_ack = wb_ack;
 
-    // Readback: expose the current counter value
+    assign o_irq = irq_fired;
-    always @(*) begin
-        o_wb_dat = 32'd0;
-        o_wb_dat[WIDTH-1:0] = counter;
-    end
 
-    // Main logic
     always @(posedge i_clk) begin
-        if (i_rst) begin
+        if(i_rst) begin
-            counter <= {WIDTH{1'b0}};
+            counter <= 0;
-            presc   <= { (DIVIDER+1){1'b0} };
+            preload <= 0;
-            o_irq   <= 1'b0;
+            wb_ack <= 0;
+            o_wb_dat <= 0;
+            irq_fired <= 0;
+            counter_started <= 0;
+            counter_running <= 0;
+            prev_counter_running <= 0;
         end else begin
-            // Default prescaler behavior
+
-            if (DIVIDER != 0) begin
+            prev_counter_running <= counter_running;
-                if (counter != 0 && !o_irq)
+            counter_running <= counter>0;
-                    presc <= presc + 1'b1;
+
-                else
+            if(!irq_fired && prev_counter_running && !counter_running)
-                    presc <= { (DIVIDER+1){1'b0} };
+                irq_fired <= 1'b1;
+            if(counter>0 && counter_started)
+                counter <= counter - 1;
+
+            if(counter == 0 && preload>0 && counter_started)
+                counter <= preload;
+
+            if(counter == 0 && preload == 0)
+                counter_started <= 1'b0;
+
+            // Ack generation
+            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
+
+            // Read cycle
+            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
+                if(i_wb_adr[3:0] == 4'b0000) begin
+                    if(i_wb_sel[0]) o_wb_dat[7:0] <= counter[7:0];
+                    if(i_wb_sel[1]) o_wb_dat[15:8] <= counter[15:8];
+                    if(i_wb_sel[2]) o_wb_dat[23:16] <= counter[23:16];
+                    if(i_wb_sel[3]) o_wb_dat[31:24] <= counter[31:24];
+                end else if(i_wb_adr[3:0] == 4'b0100) begin
+                    if(i_wb_sel[0]) o_wb_dat[7:0] <= preload[7:0];
+                    if(i_wb_sel[1]) o_wb_dat[15:8] <= preload[15:8];
+                    if(i_wb_sel[2]) o_wb_dat[23:16] <= preload[23:16];
+                    if(i_wb_sel[3]) o_wb_dat[31:24] <= preload[31:24];
+                end
             end
 
-            // Wishbone write: load counter and clear IRQ
+            // write cycle
-            if (o_wb_ack && i_wb_we) begin
+            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
-                counter <= i_wb_dat[WIDTH-1:0];
+                if(i_wb_adr[3:0] == 4'b0000) begin
-                o_irq   <= 1'b0;
+                    if(i_wb_sel[0]) counter[7:0] <= i_wb_dat[7:0];
+                    if(i_wb_sel[1]) counter[15:8] <= i_wb_dat[15:8];
+                    if(i_wb_sel[2]) counter[23:16] <= i_wb_dat[23:16];
+                    if(i_wb_sel[3]) counter[31:24] <= i_wb_dat[31:24];
+                    counter_started <= 1'b1;
+                end else if(i_wb_adr[3:0] == 4'b0100) begin
+                    if(i_wb_sel[0]) preload[7:0] <= i_wb_dat[7:0];
+                    if(i_wb_sel[1]) preload[15:8] <= i_wb_dat[15:8];
+                    if(i_wb_sel[2]) preload[23:16] <= i_wb_dat[23:16];
+                    if(i_wb_sel[3]) preload[31:24] <= i_wb_dat[31:24];
+                    counter_started <= 1'b1;
+                end else if(i_wb_adr[3:0] == 4'b1000) begin
+                    // Any write to BASE+8 will ack the IRQ
+                    irq_fired <= 1'b0;
+                end
+            end
 
-                // reset prescaler on (re)start or stop
+        end
-                presc   <= { (DIVIDER+1){1'b0} };
+    end
 
-            end else begin
+`ifdef FORMAL
-                // Countdown when running (counter>0), not already IRQ'd
+    // Formal verification
-                if (!o_irq && counter != 0) begin
+    reg f_past_valid = 1'b0;
-                    if (tick) begin
+    wire cnt_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h0);
-                        if (counter == 1) begin
+    wire pld_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h4);
-                            counter <= {WIDTH{1'b0}};
+    wire ack_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h8);
-                            o_irq   <= 1'b1; // sticky until next write
+    reg [31:0] past_counter;
-                            presc   <= { (DIVIDER+1){1'b0} };
+
-                        end else begin
+    always @(posedge i_clk) begin
-                            counter <= counter - 1'b1;
+        f_past_valid <= 1'b1;
-                        end
+        past_counter <= counter;
-                    end
+
-                end
+        // 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/tb/tb_wb_timer.v

@@ -0,0 +1,143 @@
+`timescale 1ns/1ps
+
+module tb_wb_timer;
+    localparam ADDR_COUNTER = 32'h0000_0000;
+    localparam ADDR_PRELOAD = 32'h0000_0004;
+    localparam ADDR_ACK     = 32'h0000_0008;
+
+    reg         i_clk;
+    reg         i_rst;
+    reg [31:0]  i_wb_adr;
+    reg [31:0]  i_wb_dat;
+    reg [3:0]   i_wb_sel;
+    reg         i_wb_we;
+    reg         i_wb_stb;
+    reg         i_wb_cyc;
+    wire [31:0] o_wb_dat;
+    wire        o_wb_ack;
+    wire        o_irq;
+
+    reg [31:0] read_data;
+    integer cycle;
+
+    wb_countdown_timer dut (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .o_irq(o_irq),
+        .i_wb_adr(i_wb_adr),
+        .i_wb_dat(i_wb_dat),
+        .o_wb_dat(o_wb_dat),
+        .i_wb_sel(i_wb_sel),
+        .i_wb_we(i_wb_we),
+        .i_wb_cyc(i_wb_cyc),
+        .i_wb_stb(i_wb_stb),
+        .o_wb_ack(o_wb_ack)
+    );
+
+    initial i_clk = 1'b0;
+    always #5 i_clk = ~i_clk;
+
+    task automatic wb_write;
+        input [31:0] addr;
+        input [31:0] data;
+        input [3:0]  sel;
+        begin
+            @(negedge i_clk);
+            i_wb_adr <= addr;
+            i_wb_dat <= data;
+            i_wb_sel <= sel;
+            i_wb_we  <= 1'b1;
+            i_wb_stb <= 1'b1;
+            i_wb_cyc <= 1'b1;
+
+            while (!o_wb_ack)
+                @(posedge i_clk);
+
+            @(negedge i_clk);
+            i_wb_we  <= 1'b0;
+            i_wb_stb <= 1'b0;
+            i_wb_cyc <= 1'b0;
+            i_wb_sel <= 4'b0000;
+            i_wb_dat <= 32'h0000_0000;
+        end
+    endtask
+
+    task automatic wb_read;
+        input [31:0] addr;
+        output [31:0] data;
+        begin
+            @(negedge i_clk);
+            i_wb_adr <= addr;
+            i_wb_dat <= 32'h0000_0000;
+            i_wb_sel <= 4'b1111;
+            i_wb_we  <= 1'b0;
+            i_wb_stb <= 1'b1;
+            i_wb_cyc <= 1'b1;
+
+            while (!o_wb_ack)
+                @(posedge i_clk);
+
+            #1;
+            data = o_wb_dat;
+
+            @(negedge i_clk);
+            i_wb_stb <= 1'b0;
+            i_wb_cyc <= 1'b0;
+            i_wb_sel <= 4'b0000;
+        end
+    endtask
+
+    initial begin
+        $dumpfile("wb_timer.vcd");
+        $dumpvars(0, tb_wb_timer);
+
+        i_rst    = 1'b1;
+        i_wb_adr = 32'h0000_0000;
+        i_wb_dat = 32'h0000_0000;
+        i_wb_sel = 4'b0000;
+        i_wb_we  = 1'b0;
+        i_wb_stb = 1'b0;
+        i_wb_cyc = 1'b0;
+
+        repeat (2) @(posedge i_clk);
+        i_rst = 1'b0;
+
+        wb_write(ADDR_COUNTER, 5, 4'b1111);
+        wb_write(ADDR_PRELOAD, 0, 4'b1111);
+
+        for (cycle = 0; cycle < 40; cycle = cycle + 1) begin
+            @(posedge i_clk);
+            if(o_irq)
+                wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111);
+        end
+
+        for (cycle = 0; cycle < 8; cycle = cycle + 1)
+            @(posedge i_clk);
+
+        wb_write(ADDR_PRELOAD, 8, 4'b1111);
+
+        for (cycle = 0; cycle < 21; cycle = cycle + 1) begin
+            @(posedge i_clk);
+            if(o_irq)
+                wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111);
+        end
+
+        wb_write(ADDR_PRELOAD, 6, 4'b1111);
+
+        for (cycle = 0; cycle < 21; cycle = cycle + 1) begin
+            @(posedge i_clk);
+            if(o_irq)
+                wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111);
+        end
+
+        wb_write(ADDR_PRELOAD, 0, 4'b1111);
+
+        for (cycle = 0; cycle < 10; cycle = cycle + 1) begin
+            @(posedge i_clk);
+            if(o_irq)
+                wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111);
+        end
+
+        $finish;
+    end
+endmodule

cores/wb/wb_timer/wb_timer.core

@@ -8,6 +8,10 @@ filesets:
         files:
             - rtl/wb_timer.v
         file_type: verilogSource
+    tb:
+        files:
+            - tb/tb_wb_timer.v
+        file_type: verilogSource
     formal_rtl:
         depend:
             - joppeb:wb:formal_checker
@@ -25,8 +29,13 @@ targets:
             - rtl
         toplevel: wb_countdown_timer
         parameters:
-            - WIDTH
+            - address
-            - DIVIDER
+    sim:
+        default_tool: icarus
+        filesets:
+            - rtl
+            - tb
+        toplevel: tb_wb_timer
     formal:
         default_tool: symbiyosys
         filesets:
@@ -35,15 +44,15 @@ targets:
             - formal_cfg
         toplevel: formal_wb_timer
         parameters:
-            - WIDTH
+            - address
-            - DIVIDER
+            - FORMAL=true
 
 parameters:
-    WIDTH:
+    address:
         datatype: int
-        description: Counter width in bits
+        description: Base address of register set
-        paramtype: vlogparam
-    DIVIDER:
-        datatype: int
-        description: Prescaler divider as a power of two exponent
         paramtype: vlogparam
+    FORMAL:
+        datatype: bool
+        description: Enable in-module formal-only logic
+        paramtype: vlogdefine

xilinx_fusesoc.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+set -e
+
+. /opt/Xilinx/14.7/ISE_DS/settings64.sh /opt/Xilinx/14.7/ISE_DS
+
+echo fusesoc "$@"
+exec fusesoc "$@"