Added everything from the other system

.gitignore

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

.gitmodules

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

check_formal.sh

@@ -1,95 +0,0 @@
-#!/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,9 +44,7 @@ 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];
@@ -110,16 +108,12 @@ module mcu_peripherals (
     assign wbs_dat_r[0*32 +: 32] = gpio_wbs_dat_r;
     assign wbs_ack[0] = gpio_wbs_ack;
 
-    wb_countdown_timer #(
-        .address(TIMER_BASE_ADDR)
-    ) timer (
+    wb_countdown_timer 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,8 +1,7 @@
 `timescale 1ns/1ps
 
 module toplevel #(
-    parameter sim = 0,
-    parameter memfile = "sweep.hex"
+    parameter sim = 0
 )(
     input wire aclk,
     input wire aresetn,
@@ -58,7 +57,7 @@ module toplevel #(
     wire test;
 
     mcu #(
-        .memfile(memfile),
+        .memfile("../sw/sweep/sweep.hex"),
         .sim(sim),
         .jtag(1)
     ) mcu (

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

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

cores/system/test/tb/tb_toplevel.v

@@ -1,37 +0,0 @@
-`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,14 +13,10 @@ filesets:
         files:
             - rtl/toplevel.v
         file_type: verilogSource
-    tb:
-        files:
-            - tb/tb_toplevel.v
-        file_type: verilogSource
 
     sw:
         files:
-            - sw/sweep/sweep.hex : {copyto : sweep.hex}
+            - sw/sweep/sweep.hex
         file_type: user
 
     mimas:
@@ -33,13 +29,6 @@ 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)
-            A1: assume(
+            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)
-            A2: assume(!o_wb_ack);
+            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
         )
-            A3: assume(!o_wb_ack);
+            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
-            R1: assert(!i_wb_cyc);
-            R2: assert(!i_wb_stb);
+            assert(!i_wb_cyc);
+            assert(!i_wb_stb);
         end
 
-        // R3: STB never high without CYC
+        // R2: STB never high without CYC
         if(i_wb_stb)
-            R3: assert(i_wb_cyc);
+            assert(i_wb_cyc);
 
-        // R4-R9: Once a request starts, hold it stable until the slave responds
+        // R3: Once a request starts, hold it stable until the slave responds
         if(
             f_past_valid &&
             !$past(i_rst || i_wb_rst) &&
@@ -57,42 +57,17 @@ module formal_wb_master_checker (
             !o_wb_ack &&
             !(i_rst || i_wb_rst)
         ) begin
-            R4: assert(i_wb_cyc);
-            R5: assert(i_wb_stb);
-            R6: assert(i_wb_adr == $past(i_wb_adr));
-            R7: assert(i_wb_dat == $past(i_wb_dat));
-            R8: assert(i_wb_sel == $past(i_wb_sel));
-            R9: assert(i_wb_we == $past(i_wb_we));
+            assert(i_wb_cyc);
+            assert(i_wb_stb);
+            assert(i_wb_adr == $past(i_wb_adr));
+            assert(i_wb_dat == $past(i_wb_dat));
+            assert(i_wb_sel == $past(i_wb_sel));
+            assert(i_wb_we == $past(i_wb_we));
         end
 
-        // R10: Once CYC is low, STB must also be low
+        // R4: Once CYC is low, STB must also be low
         if(!i_wb_cyc)
-            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);
-
+            assert(!i_wb_stb);
     end
 
     wire unused = &{1'b0, o_wb_rdt};

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,9 +1,6 @@
 `timescale 1ns/1ps
 
-module formal_wb_slave_checker #(
-    parameter combinatorial_ack = 0,
-    parameter expect_wait_state = 0
-) (
+module formal_wb_slave_checker (
     input wire        i_clk,
     input wire        i_rst,
     input wire        i_wb_rst,
@@ -25,38 +22,38 @@ module formal_wb_slave_checker #(
 
         // A1: Reset forces cyc=0, stb=0
         if (i_rst) begin
-            A1: assume(!i_wb_cyc);
-            A2: assume(!i_wb_stb);
+            assume(!i_wb_cyc);
+            assume(!i_wb_stb);
         end
 
-        // A3: std->cyc, stb never high without cyc
+        // A2: std->cyc, stb never high without cyc
         if(i_wb_stb)
-            A3: assume(i_wb_cyc);
+            assume(i_wb_cyc);
 
-        // A4-A9: once a request starts, hold it stable until the slave responds
+        // A3: 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
-            A4: assume(i_wb_cyc);
-            A5: assume(i_wb_stb);
-            A6: assume(i_wb_adr == $past(i_wb_adr));
-            A7: assume(i_wb_dat == $past(i_wb_dat));
-            A8: assume(i_wb_sel == $past(i_wb_sel));
-            A9: assume(i_wb_we == $past(i_wb_we));
+            assume(i_wb_cyc);
+            assume(i_wb_stb);
+            assume(i_wb_adr == $past(i_wb_adr));
+            assume(i_wb_dat == $past(i_wb_dat));
+            assume(i_wb_sel == $past(i_wb_sel));
+            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)
-            R1: assert(
+            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)
-            R2: assert(!o_wb_ack);
+            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))
-            R3: assert(!o_wb_ack);
+            assert(!o_wb_ack);
 
         // R4: once STB has been dropped for a full cycle, ACK must be low
         if(
@@ -64,37 +61,7 @@ module formal_wb_slave_checker #(
             !$past(i_wb_stb) &&
             !i_wb_stb
         )
-            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);
-            
+            assert(!o_wb_ack);
     end
 
     wire unused = &{1'b0, o_wb_rdt};

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby

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

cores/wb/wb_gpio/formal/wb_gpio.sby

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

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

@@ -0,0 +1,13 @@
+[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

@@ -0,0 +1,2 @@
+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

@@ -1,53 +0,0 @@
-`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

@@ -1,23 +0,0 @@
-[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,16 +10,6 @@ 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:
@@ -29,16 +19,6 @@ 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,19 +1,9 @@
-[tasks]
-prove
-cover
-bmc
-
 [options]
-bmc: mode bmc
-bmc: depth 50
-cover: mode cover
-cover: depth 50
-prove: mode prove
+mode prove
+depth 8
 
 [engines]
-bmc: smtbmc yices
-cover: smtbmc yices
-prove: abc pdr
+smtbmc z3 parallel.enable=true parallel.threads.max=8
 
 [script]
 read -formal clog2.vh

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -1,62 +0,0 @@
-`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

@@ -1,23 +0,0 @@
-[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,187 +1,74 @@
 `timescale 1ns/1ps
 
 module wb_countdown_timer #(
-    parameter address = 32'h00000000 // Base address of peripheral
+    parameter WIDTH   = 32,  // counter width (<=32 makes bus mapping easy)
+    parameter DIVIDER = 0    // optional prescaler: tick every 2^DIVIDER cycles
 )(
     input  wire         i_clk,
     input  wire         i_rst,
-    output wire         o_irq,
+    output reg          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
 );
 
-    // Registers
-    reg [31:0]       counter; // The actual counter. Generates an interrupt when it reaches 0
-    reg [31:0]       preload; // The value with which the counter gets loaded after it reaches 0. 0 to keep the timer off
+    // One-cycle acknowledge on any valid WB access
+    // (classic, zero-wait-state peripheral)
+    assign o_wb_ack = i_wb_cyc & i_wb_stb;
 
-    reg wb_ack = 0;
-    reg irq_fired = 0;
-    reg counter_started = 0;
-    reg counter_running = 0;
-    reg prev_counter_running = 0;
-    assign o_wb_ack = wb_ack;
+    // Internal countdown and prescaler
+    reg [WIDTH-1:0] counter;
+    reg [DIVIDER:0] presc;   // enough bits to count up to 2^DIVIDER-1
+    wire tick = (DIVIDER == 0) ? 1'b1 : (presc[DIVIDER] == 1'b1);
 
-    assign o_irq = irq_fired;
+    // Readback: expose the current counter value
+    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
-            counter <= 0;
-            preload <= 0;
-            wb_ack <= 0;
-            o_wb_dat <= 0;
-            irq_fired <= 0;
-            counter_started <= 0;
-            counter_running <= 0;
-            prev_counter_running <= 0;
+            counter <= {WIDTH{1'b0}};
+            presc   <= { (DIVIDER+1){1'b0} };
+            o_irq   <= 1'b0;
         end else begin
-
-            prev_counter_running <= counter_running;
-            counter_running <= counter>0;
-
-            if(!irq_fired && prev_counter_running && !counter_running)
-                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
+            // Default prescaler behavior
+            if (DIVIDER != 0) begin
+                if (counter != 0 && !o_irq)
+                    presc <= presc + 1'b1;
+                else
+                    presc <= { (DIVIDER+1){1'b0} };
             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;
+            // Wishbone write: load counter and clear IRQ
+            if (o_wb_ack && i_wb_we) begin
+                counter <= i_wb_dat[WIDTH-1:0];
+                o_irq   <= 1'b0;
+
+                // reset prescaler on (re)start or stop
+                presc   <= { (DIVIDER+1){1'b0} };
+
+            end else begin
+                // Countdown when running (counter>0), not already IRQ'd
+                if (!o_irq && counter != 0) begin
+                    if (tick) begin
+                        if (counter == 1) begin
+                            counter <= {WIDTH{1'b0}};
+                            o_irq   <= 1'b1; // sticky until next write
+                            presc   <= { (DIVIDER+1){1'b0} };
+                        end else begin
+                            counter <= counter - 1'b1;
                         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

@@ -1,143 +0,0 @@
-`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,20 +8,6 @@ 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:
@@ -29,30 +15,15 @@ targets:
             - rtl
         toplevel: wb_countdown_timer
         parameters:
-            - address
-    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
+            - WIDTH
+            - DIVIDER
 
 parameters:
-    address:
+    WIDTH:
         datatype: int
-        description: Base address of register set
+        description: Counter width in bits
+        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

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