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

@@ -0,0 +1,95 @@
+#!/bin/sh
+
+# Add or remove cores here. Each entry should be a full FuseSoC VLNV.
+CORES="
+joppeb:wb:wb_mem32
+joppeb:wb:wb_gpio
+joppeb:wb:wb_gpio_banks
+joppeb:wb:jtag_wb_bridge
+joppeb:wb:wb_timer
+"
+
+if [ -n "$1" ]; then
+	CORES="$1"
+fi
+
+# Add or remove formal tasks here.
+TASKS="
+bmc
+cover
+prove
+"
+
+total=0
+passed=0
+failed=0
+passed_runs=""
+failed_runs=""
+
+run_task() {
+	core="$1"
+	task="$2"
+	label="$core [$task]"
+	log_file=""
+	total=$((total + 1))
+
+	printf '\n[%d] Running formal %s for %s\n' "$total" "$task" "$core"
+
+	log_file=$(mktemp /tmp/check_formal.XXXXXX) || exit 2
+
+	if \
+		FUSESOC_CORE="$core" \
+		FUSESOC_TASK="$task" \
+		script -qefc 'fusesoc run --target formal "$FUSESOC_CORE" --taskname "$FUSESOC_TASK"' "$log_file" \
+			>/dev/null 2>&1
+	then
+		passed=$((passed + 1))
+		passed_runs="$passed_runs
+$label"
+		printf 'Result: PASS (%s)\n' "$label"
+		rm -f "$log_file"
+		return 0
+	else
+		failed=$((failed + 1))
+		failed_runs="$failed_runs
+$label"
+		printf 'Result: FAIL (%s)\n' "$label"
+		printf 'Captured log for %s:\n' "$label"
+		cat "$log_file" #| grep summary
+		rm -f "$log_file"
+		return 1
+	fi
+}
+
+for core in $CORES; do
+	for task in $TASKS; do
+		run_task "$core" "$task"
+	done
+done
+
+printf '\nFormal run summary\n'
+printf '  Total:   %d\n' "$total"
+printf '  Passed:  %d\n' "$passed"
+printf '  Failed:  %d\n' "$failed"
+
+if [ -n "$passed_runs" ]; then
+	printf '\nPassed runs:\n'
+	printf '%s\n' "$passed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ -n "$failed_runs" ]; then
+	printf '\nFailed runs:\n'
+	printf '%s\n' "$failed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ "$failed" -ne 0 ]; then
+	exit 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,17 +57,42 @@ 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);
+
+        // C1: We eventually initiate a request
+        C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+
+        // C2: We eventually get an ACK during an active request
+        C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+
+        // 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.
+        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
+        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-C6: Read and write both occur (even if only once each)
+        C5: 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);
+
+        // C7: A transfer completes and the master drops CYC sometime after
+        C7: cover(f_past_valid && !i_rst && !i_wb_rst &&
+            $past(i_wb_cyc && i_wb_stb && o_wb_ack) && !i_wb_cyc);
+
     end
 
     wire unused = &{1'b0, o_wb_rdt};

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,6 +1,9 @@
 `timescale 1ns/1ps
 
-module formal_wb_slave_checker (
+module formal_wb_slave_checker #(
+    parameter combinatorial_ack = 0,
+    parameter expect_wait_state = 0
+) (
     input wire        i_clk,
     input wire        i_rst,
     input wire        i_wb_rst,
@@ -22,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(
@@ -61,7 +64,37 @@ module formal_wb_slave_checker (
             !$past(i_wb_stb) &&
             !i_wb_stb
         )
-            assert(!o_wb_ack);
+            R4: assert(!o_wb_ack);
+
+        // C1: A request occurs at all
+        C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+
+        // C2-C3: A request with write and with read occur
+        C2: 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);
+
+        // C4: ACK happens during a request (basic progress)
+        C4: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+
+        // C5-C7: Exercise the expected ACK timing style for this slave.
+        if (combinatorial_ack) begin
+            C5: cover(f_past_valid && !i_rst && !i_wb_rst &&
+                (i_wb_cyc && i_wb_stb) && o_wb_ack);
+        end else begin
+            C6: cover(f_past_valid && !i_rst && !i_wb_rst &&
+                $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
+
+            // C7: Optional wait-state behavior for slaves that intentionally stall.
+            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
+
+        // C8: Master ends a cycle (CYC drops) after at least one request
+        C8: cover(f_past_valid && !i_rst && !i_wb_rst &&
+            $past(i_wb_cyc && i_wb_stb) && !i_wb_cyc);
+            
     end
 
     wire unused = &{1'b0, o_wb_rdt};

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 16
+cover: mode cover
+cover: depth 16
+prove: mode prove
 
 [engines]
-abc pdr
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 {{"-formal"|gen_reads}}

cores/wb/wb_gpio/formal/wb_gpio.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
 
 [engines]
-smtbmc z3 parallel.enable=true parallel.threads.max=8
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 {{"-formal"|gen_reads}}

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_gpio_banks/formal/formal_wb_gpio_banks.v

@@ -0,0 +1,53 @@
+`timescale 1ns/1ps
+
+module formal_wb_gpio_banks #(
+    parameter integer NUM_BANKS = 2,
+    parameter [31:0] BASE_ADDR = 32'h00000000
+);
+    (* gclk *) reg                  i_wb_clk;
+    (* anyseq *) reg                i_rst;
+    (* anyseq *) reg                i_wb_rst;
+    (* anyseq *) reg [31:0]         i_wb_adr;
+    (* anyseq *) reg [31:0]         i_wb_dat;
+    (* anyseq *) reg [3:0]          i_wb_sel;
+    (* anyseq *) reg                i_wb_we;
+    (* anyseq *) reg                i_wb_stb;
+    (* anyseq *) reg [NUM_BANKS*32-1:0] i_gpio;
+    wire [31:0]                     o_wb_rdt;
+    wire                            o_wb_ack;
+    wire [NUM_BANKS*32-1:0]         o_gpio;
+    wire                            i_wb_cyc;
+
+    assign i_wb_cyc = i_wb_stb || o_wb_ack;
+
+    wb_gpio_banks #(
+        .NUM_BANKS(NUM_BANKS),
+        .BASE_ADDR(BASE_ADDR)
+    ) dut (
+        .i_wb_clk(i_wb_clk),
+        .i_wb_rst(i_wb_rst),
+        .i_wb_adr(i_wb_adr),
+        .i_wb_dat(i_wb_dat),
+        .i_wb_sel(i_wb_sel),
+        .i_wb_we(i_wb_we),
+        .i_wb_stb(i_wb_stb),
+        .i_gpio(i_gpio),
+        .o_wb_rdt(o_wb_rdt),
+        .o_wb_ack(o_wb_ack),
+        .o_gpio(o_gpio)
+    );
+
+    formal_wb_slave_checker wb_checker (
+        .i_clk(i_wb_clk),
+        .i_rst(i_rst),
+        .i_wb_rst(i_wb_rst),
+        .i_wb_adr(i_wb_adr),
+        .i_wb_dat(i_wb_dat),
+        .i_wb_sel(i_wb_sel),
+        .i_wb_we(i_wb_we),
+        .i_wb_stb(i_wb_stb),
+        .i_wb_cyc(i_wb_cyc),
+        .o_wb_rdt(o_wb_rdt),
+        .o_wb_ack(o_wb_ack)
+    );
+endmodule

cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby

@@ -0,0 +1,23 @@
+[tasks]
+prove
+cover
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
+
+[engines]
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
+
+[script]
+{{"-formal"|gen_reads}}
+prep -top {{top_level}}
+
+[files]
+{{files}}

cores/wb/wb_gpio_banks/wb_gpio_banks.core

@@ -10,6 +10,16 @@ filesets:
         files:
             - rtl/wb_gpio_banks.v
         file_type: verilogSource
+    formal_rtl:
+        depend:
+            - joppeb:wb:formal_checker
+        files:
+            - formal/formal_wb_gpio_banks.v
+        file_type: verilogSource
+    formal_cfg:
+        files:
+            - formal/wb_gpio_banks.sby
+        file_type: sbyConfigTemplate
 
 targets:
     default:
@@ -19,6 +29,16 @@ targets:
         parameters:
             - NUM_BANKS
             - BASE_ADDR
+    formal:
+        default_tool: symbiyosys
+        filesets:
+            - rtl
+            - formal_rtl
+            - formal_cfg
+        toplevel: formal_wb_gpio_banks
+        parameters:
+            - NUM_BANKS
+            - BASE_ADDR
 
 parameters:
     NUM_BANKS:

cores/wb/wb_mem32/formal/wb_mem32.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
 
 [engines]
-smtbmc z3 parallel.enable=true parallel.threads.max=8
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 read -formal clog2.vh

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -0,0 +1,62 @@
+`timescale 1ns/1ps
+
+module formal_wb_timer;
+    (* gclk *) reg        i_clk;
+    (* anyseq *) reg      i_rst;
+    (* anyseq *) reg [31:0] i_wb_adr;
+    (* anyseq *) reg [31:0] i_wb_dat;
+    (* anyseq *) reg [3:0]  i_wb_sel;
+    (* anyseq *) reg      i_wb_we;
+    (* anyseq *) reg      i_wb_cyc;
+    (* anyseq *) reg      i_wb_stb;
+    wire [31:0]           o_wb_dat;
+    wire                  o_wb_ack;
+    wire                  o_irq;
+    wire                  i_wb_rst;
+    reg                   f_past_valid;
+
+    assign i_wb_rst = 1'b0;
+
+    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)
+    );
+
+    formal_wb_slave_checker #(
+        .combinatorial_ack(0),
+    ) wb_checker (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .i_wb_rst(i_wb_rst),
+        .i_wb_adr(i_wb_adr),
+        .i_wb_dat(i_wb_dat),
+        .i_wb_sel(i_wb_sel),
+        .i_wb_we(i_wb_we),
+        .i_wb_stb(i_wb_stb),
+        .i_wb_cyc(i_wb_cyc),
+        .o_wb_rdt(o_wb_dat),
+        .o_wb_ack(o_wb_ack)
+    );
+
+    initial f_past_valid = 1'b0;
+
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+
+        // Keep the bus idle on the first cycle after reset so the zero-wait ACK
+        // does not collide with the generic slave checker's post-reset rule.
+        if (f_past_valid && $past(i_rst)) begin
+            assume(!i_wb_cyc);
+            assume(!i_wb_stb);
+        end
+    end
+endmodule

cores/wb/wb_timer/formal/wb_timer.sby

@@ -0,0 +1,23 @@
+[tasks]
+prove
+cover
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
+
+[engines]
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: smtbmc yices
+
+[script]
+{{"-formal"|gen_reads}}
+prep -top {{top_level}}
+
+[files]
+{{files}}

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
-                if (counter != 0 && !o_irq)
-                    presc <= presc + 1'b1;
-                else
-                    presc <= { (DIVIDER+1){1'b0} };
-            end
 
-            // Wishbone write: load counter and clear IRQ
+            prev_counter_running <= counter_running;
-            if (o_wb_ack && i_wb_we) begin
+            counter_running <= counter>0;
-                counter <= i_wb_dat[WIDTH-1:0];
-                o_irq   <= 1'b0;
 
-                // reset prescaler on (re)start or stop
+            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;
 
-            end else begin
+            if(counter == 0 && preload>0 && counter_started)
-                // Countdown when running (counter>0), not already IRQ'd
+                counter <= preload;
-                if (!o_irq && counter != 0) begin
+
-                    if (tick) begin
+            if(counter == 0 && preload == 0)
-                        if (counter == 1) begin
+                counter_started <= 1'b0;
-                            counter <= {WIDTH{1'b0}};
+
-                            o_irq   <= 1'b1; // sticky until next write
+            // Ack generation
-                            presc   <= { (DIVIDER+1){1'b0} };
+            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
-                        end else begin
+
-                            counter <= counter - 1'b1;
+            // Read cycle
-                        end
+            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
-                    end
+                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
+
+            // write 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]) 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
+
         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/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,20 @@ 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
+        files:
+            - formal/formal_wb_timer.v
+        file_type: verilogSource
+    formal_cfg:
+        files:
+            - formal/wb_timer.sby
+        file_type: sbyConfigTemplate
 
 targets:
     default:
@@ -15,15 +29,30 @@ 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:
+            - rtl
+            - formal_rtl
+            - formal_cfg
+        toplevel: formal_wb_timer
+        parameters:
+            - address
+            - 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 "$@"