Added everything from the other system

2026-02-28 21:46:59 +01:00
62 changed files with 408 additions and 11064 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1 @@
-build/
+build/
 out/
 *__pycache__*
--- a/.gitmodules
+++ b/.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
--- a/capture1.png
+++ b/capture1.png
--- a/capture2.csv
+++ b/capture2.csv
--- a/capture2.png
+++ b/capture2.png
--- a/check_formal.sh
+++ b/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
--- a/cores/primitive/lvds_comparator/lvds_comparator.core
+++ b/cores/primitive/lvds_comparator/lvds_comparator.core
@@ -1,26 +0,0 @@
 CAPI=2:
 name: joppeb:primitive:lvds_comparator:1.0
 description: LVDS comparator wrapper
 filesets:
    wrapper:
        files:
            - lvds_comparator.v
        file_type: verilogSource
    generic:
        files:
            - lvds_comparator_generic_impl.v
        file_type: verilogSource
    spartan6:
        files:
            - lvds_comparator_spartan6.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - wrapper
            - generic
            - spartan6
        toplevel: lvds_comparator
--- a/cores/primitive/lvds_comparator/lvds_comparator.v
+++ b/cores/primitive/lvds_comparator/lvds_comparator.v
@@ -1,19 +0,0 @@
 module lvds_comparator(
    input wire a,
    input wire b,
    output wire o
 );
 `ifdef FPGA_SPARTAN6
    lvds_comparator_spartan6_impl impl_i (
        .a(a),
        .b(b),
        .o(o)
    );
 `else
    lvds_comparator_generic_impl impl_i (
        .a(a),
        .b(b),
        .o(o)
    );
 `endif
 endmodule
--- a/cores/primitive/lvds_comparator/lvds_comparator_generic_impl.v
+++ b/cores/primitive/lvds_comparator/lvds_comparator_generic_impl.v
@@ -1,7 +0,0 @@
 module lvds_comparator_generic_impl (
    input wire a,
    input wire b,
    output wire o
 );
    assign o = a;
 endmodule
--- a/cores/primitive/lvds_comparator/lvds_comparator_spartan6.v
+++ b/cores/primitive/lvds_comparator/lvds_comparator_spartan6.v
@@ -1,14 +0,0 @@
 module lvds_comparator_spartan6_impl (
    input wire a,
    input wire b,
    output wire o
 );
    IBUFDS #(
        .DIFF_TERM("FALSE"),
        .IOSTANDARD("LVDS_33")
    ) lvds_buf (
        .O(o),
        .I(a),
        .IB(b)
    );
 endmodule
--- a/cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.core
+++ b/cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.core
@@ -1,29 +0,0 @@
 CAPI=2:
 name: joppeb:signal:decimate_by_r_q15:1.0
 description: Q1.15 integer-rate decimator
 filesets:
    rtl:
        files:
            - decimate_by_r_q15.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - rtl
        toplevel: decimate_by_r_q15
        parameters:
            - R
            - CNT_W
 parameters:
    R:
        datatype: int
        description: Integer decimation ratio
        paramtype: vlogparam
    CNT_W:
        datatype: int
        description: Counter width for the decimation counter
        paramtype: vlogparam
--- a/cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.v
+++ b/cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.v
@@ -1,74 +0,0 @@
 `timescale 1ns/1ps
 // =============================================================================
 // Decimator by R
 // Reduces the effective sample rate by an integer factor R by selecting every
 // R-th input sample. Generates a one-cycle 'o_valid' pulse each time a new
 // decimated sample is produced.
 //
 // Implements:
 //      For each valid input sample:
 //          if (count == R-1):
 //              count     <= 0
 //              o_q15   <= i_q15
 //              o_valid <= 1
 //          else:
 //              count     <= count + 1
 //
 // parameters:
 //      -- R      : integer decimation factor (e.g., 400)
 //                   output sample rate = input rate / R
 //      -- CNT_W  : counter bit width, must satisfy 2^CNT_W > R
 //
 // inout:
 //      -- i_clk     : input clock (same rate as 'i_valid')
 //      -- i_rst_n   : active-low synchronous reset
 //      -- i_valid   : input data strobe; assert 1'b1 if input is always valid
 //      -- i_q15     : signed 16-bit Q1.15 input sample (full-rate)
 //      -- o_valid   : single-cycle pulse every R samples (decimated rate strobe)
 //      -- o_q15     : signed 16-bit Q1.15 output sample (decimated stream)
 //
 // Notes:
 //  - This module performs *pure downsampling* (sample selection only).
 //    It does not include any anti-alias filtering; high-frequency content
 //    above the new Nyquist limit (Fs_out / 2) will alias into the baseband.
 //  - For most applications, an anti-alias low-pass filter such as
 //    lpf_iir_q15 or a FIR stage should precede this decimator.
 //  - The output sample rate is given by:
 //          Fs_out = Fs_in / R
 //  - Typical usage: interface between high-rate sigma-delta or oversampled
 //    data streams and lower-rate processing stages.
 // =============================================================================
 module decimate_by_r_q15 #(
    parameter integer R      = 400, // decimation factor
    parameter integer CNT_W  = 10   // width so that 2^CNT_W > R (e.g., 10 for 750)
 )(
    input  wire        i_clk,
    input  wire        i_rst_n,
    input  wire        i_valid,          // assert 1'b1 if always valid
    input  wire signed [15:0] i_q15,     // Q1.15 sample at full rate
    output reg         o_valid,          // 1-cycle pulse every R samples
    output reg  signed [15:0] o_q15      // Q1.15 sample at decimated rate
 );
    reg [CNT_W-1:0] cnt;
    always @(posedge i_clk or negedge i_rst_n) begin
        if (!i_rst_n) begin
            cnt       <= {CNT_W{1'b0}};
            o_valid   <= 1'b0;
            o_q15     <= 16'sd0;
        end else begin
            o_valid <= 1'b0;
            if (i_valid) begin
                if (cnt == R-1) begin
                    cnt       <= {CNT_W{1'b0}};
                    o_q15     <= i_q15;
                    o_valid   <= 1'b1;
                end else begin
                    cnt <= cnt + 1'b1;
                end
            end
        end
    end
 endmodule
--- a/cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.core
+++ b/cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.core
@@ -1,24 +0,0 @@
 CAPI=2:
 name: joppeb:signal:lpf_iir_q15_k:1.0
 description: First-order Q1.15 IIR low-pass filter
 filesets:
    rtl:
        files:
            - lpf_iir_q15_k.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - rtl
        toplevel: lpf_iir_q15_k
        parameters:
            - K
 parameters:
    K:
        datatype: int
        description: Filter shift factor
        paramtype: vlogparam
--- a/cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.v
+++ b/cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.v
@@ -1,64 +0,0 @@
 `timescale 1ns/1ps
 // =============================================================================
 // Low-Pass IIR Filter (Q1.15)
 // Simple first-order infinite impulse response filter, equivalent to an
 // exponential moving average. Provides an adjustable smoothing factor based
 // on parameter K.
 //
 // Implements:
 //      Y[n+1] = Y[n] + (X[n] - Y[n]) / 2^K
 //
 // This is a purely digital one-pole low-pass filter whose time constant
 // approximates that of an analog RC filter, where alpha = 1 / 2^K.
 //
 // The larger K is, the slower the filter responds (stronger smoothing).
 // The smaller K is, the faster it reacts to changes.
 //
 // parameters:
 //      -- K : filter shift factor (integer, 4..14 typical)
 //              cutoff frequency ≈ Fs / (2π * 2^K)
 //              larger K → lower cutoff
 //
 // inout:
 //      -- i_clk   : input clock
 //      -- i_rst_n : active-low reset
 //      -- i_x_q15 : signed 16-bit Q1.15 input sample (e.g., 0..0x7FFF)
 //      -- o_y_q15 : signed 16-bit Q1.15 filtered output
 //
 // Notes:
 //  - The arithmetic right shift implements division by 2^K.
 //  - Internal arithmetic is Q1.15 fixed-point with saturation
 //    to [0, 0x7FFF] (for non-negative signals).
 //  - Useful for smoothing noisy ADC / sigma-delta data streams
 //    or modeling an RC envelope follower.
 // =============================================================================
 module lpf_iir_q15_k #( 
    parameter integer K = 10 // try 8..12; bigger = more smoothing 
 )( 
    input wire i_clk, 
    input wire i_rst_n, 
    input wire signed [15:0] i_x_q15, // Q1.15 input (e.g., 0..0x7FFF) 
    output reg signed [15:0] o_y_q15 // Q1.15 output 
 ); 
    wire signed [15:0] e_q15 = i_x_q15 - o_y_q15; 
    wire signed [15:0] delta_q15 = e_q15 >>> K; // arithmetic shift 
    wire signed [15:0] y_next = o_y_q15 + delta_q15; // clamp to [0, 0x7FFF] (handy if your signal is non-negative) 
    function signed [15:0] clamp01; 
        input signed [15:0] v; 
    begin
        if (v < 16'sd0) 
            clamp01 = 16'sd0; 
        else if (v > 16'sh7FFF) 
            clamp01 = 16'sh7FFF; 
        else 
            clamp01 = v; 
        end 
    endfunction 
    always @(posedge i_clk or negedge i_rst_n) begin 
        if (!i_rst_n) o_y_q15 <= 16'sd0; 
        else o_y_q15 <= clamp01(y_next); 
    end 
 endmodule
--- a/cores/signal/nco_q15/rtl/nco_q15.v
+++ b/cores/signal/nco_q15/rtl/nco_q15.v
@@ -8,23 +8,23 @@
 //      -- CLK_HZ : input clock frequency in Hz
 //      -- FS_HZ : output sample frequency in Hz
 // inout:
-//      -- i_clk : input clock
+//      -- clk : input clock
-//      -- i_rst_n : reset
+//      -- rst_n : reset
-//      -- i_freq_hz : decimal number of desired generated frequency in Hz, 0-FS/2
+//      -- freq_hz : decimal number of desired generated frequency in Hz, 0-FS/2
-//      -- o_sin_q15/o_cos_q15 : I and Q outputs
+//      -- sin_q15/cos_q15 : I and Q outputs
-//      -- o_clk_en : output valid strobe
+//      -- clk_en : output valid strobe
 // =============================================================================
 module nco_q15 #(
    parameter integer CLK_HZ = 120_000_000,         // input clock
    parameter integer FS_HZ = 40_000                // sample rate
 )(
-    input wire i_clk,                               // CLK_HZ domain
+    input wire clk,                                 // CLK_HZ domain
-    input wire i_rst_n,                             // async active-low reset
+    input wire rst_n,                               // async active-low reset
-    input wire [31:0] i_freq_hz,                    // desired output frequency (Hz), 0..FS_HZ/2
+    input wire [31:0] freq_hz,                      // desired output frequency (Hz), 0..FS_HZ/2
-    output reg signed [15:0] o_sin_q15,             // Q1.15 sine
+    output reg signed [15:0] sin_q15,               // Q1.15 sine
-    output reg signed [15:0] o_cos_q15,             // Q1.15 cosine
+    output reg signed [15:0] cos_q15,               // Q1.15 cosine
-    output reg o_clk_en                             // 1-cycle strobe @ FS_HZ
+    output reg clk_en                               // 1-cycle strobe @ FS_HZ
 );
    localparam integer PHASE_FRAC_BITS = 6;
    localparam integer QTR_ADDR_BITS = 6;
@@ -41,17 +41,17 @@ module nco_q15 #(
    endfunction
    reg [clog2(DIV)-1:0] tick_cnt;
-    always @(posedge i_clk or negedge i_rst_n) begin
+    always @(posedge clk or negedge rst_n) begin
-        if (!i_rst_n) begin tick_cnt <= 0; o_clk_en <= 1'b0; end
+        if (!rst_n) begin tick_cnt <= 0; clk_en <= 1'b0; end
        else begin
-        o_clk_en <= 1'b0;
+        clk_en <= 1'b0;
-        if (tick_cnt == DIV-1) begin tick_cnt <= 0; o_clk_en <= 1'b1; end
+        if (tick_cnt == DIV-1) begin tick_cnt <= 0; clk_en <= 1'b1; end
        else tick_cnt <= tick_cnt + 1'b1;
        end
    end
-    // 32-cycle shift-add multiply: prod = i_freq_hz * RECIP  (no multiplications themself)
+    // 32-cycle shift-add multiply: prod = freq_hz * RECIP  (no multiplications themself)
-	// Starts at o_clk_en, finishes in 32 cycles (<< available cycles per sample).
+	// Starts at clk_en, finishes in 32 cycles (<< available cycles per sample).
    reg        mul_busy;
    reg  [5:0] mul_i;           // 0..31
    reg [31:0] f_reg;
@@ -59,15 +59,15 @@ module nco_q15 #(
    wire [95:0] recip_shift = {{32{1'b0}}, RECIP} << mul_i; // shift constant by i
-    always @(posedge i_clk or negedge i_rst_n) begin
+    always @(posedge clk or negedge rst_n) begin
-        if (!i_rst_n) begin
+        if (!rst_n) begin
        mul_busy <= 1'b0; mul_i <= 6'd0; f_reg <= 32'd0; acc <= 96'd0;
        end else begin
-        if (o_clk_en && !mul_busy) begin
+        if (clk_en && !mul_busy) begin
            // kick off a new multiply this sample
            mul_busy <= 1'b1;
            mul_i    <= 6'd0;
-            f_reg    <= (i_freq_hz > (FS_HZ>>1)) ? (FS_HZ>>1) : i_freq_hz; // clamp to Nyquist
+            f_reg    <= (freq_hz > (FS_HZ>>1)) ? (FS_HZ>>1) : freq_hz; // clamp to Nyquist
            acc      <= 96'd0;
        end else if (mul_busy) begin
            // add shifted RECIP if bit is set
@@ -86,16 +86,16 @@ module nco_q15 #(
    wire [95:0] acc_round = acc + (96'd1 << (SHIFT-1));
    wire [PHASE_BITS-1:0] ftw_next = acc_round[SHIFT +: PHASE_BITS]; // >> SHIFT
-    always @(posedge i_clk or negedge i_rst_n) begin
+    always @(posedge clk or negedge rst_n) begin
-        if (!i_rst_n) ftw_q <= {PHASE_BITS{1'b0}};
+        if (!rst_n) ftw_q <= {PHASE_BITS{1'b0}};
        else if (!mul_busy) ftw_q <= ftw_next; // update once product ready
    end
    // Phase accumulator (advance at FS_HZ)
    reg [PHASE_BITS-1:0] phase;
-    always @(posedge i_clk or negedge i_rst_n) begin
+    always @(posedge clk or negedge rst_n) begin
-        if (!i_rst_n)        phase <= {PHASE_BITS{1'b0}};
+        if (!rst_n)      phase <= {PHASE_BITS{1'b0}};
-        else if (o_clk_en) phase <= phase + ftw_q;
+        else if (clk_en) phase <= phase + ftw_q;
    end
    // Cosine phase = sine phase + 90°
@@ -113,8 +113,8 @@ module nco_q15 #(
    // 64-entry quarter-wave LUT
    wire [7:0] mag_sin_u8, mag_cos_u8;
-    sine_qtr_lut64 u_lut_s (.i_addr(idx_sin), .o_dout(mag_sin_u8));
+    sine_qtr_lut64 u_lut_s (.addr(idx_sin), .dout(mag_sin_u8));
-    sine_qtr_lut64 u_lut_c (.i_addr(idx_cos), .o_dout(mag_cos_u8));
+    sine_qtr_lut64 u_lut_c (.addr(idx_cos), .dout(mag_cos_u8));
    // Scale to Q1.15 and apply sign
    wire signed [15:0] mag_sin_q15 = {1'b0, mag_sin_u8, 7'd0};
@@ -125,39 +125,39 @@ module nco_q15 #(
    wire signed [15:0] sin_next = sin_neg ? -mag_sin_q15 : mag_sin_q15;
    wire signed [15:0] cos_next = cos_neg ? -mag_cos_q15 : mag_cos_q15;
-    always @(posedge i_clk or negedge i_rst_n) begin
+    always @(posedge clk or negedge rst_n) begin
-        if (!i_rst_n) begin
+        if (!rst_n) begin
-        o_sin_q15 <= 16'sd0; o_cos_q15 <= 16'sd0;
+        sin_q15 <= 16'sd0; cos_q15 <= 16'sd0;
-        end else if (o_clk_en) begin
+        end else if (clk_en) begin
-        o_sin_q15 <= sin_next; o_cos_q15 <= cos_next;
+        sin_q15 <= sin_next; cos_q15 <= cos_next;
        end
    end
 endmodule
 module sine_qtr_lut64(
-    input wire [5:0] i_addr,
+    input wire [5:0] addr,
-    output reg [7:0] o_dout
+    output reg [7:0] dout
 );
    always @* begin
-        case (i_addr)
+        case (addr)
-            6'd0: o_dout = 8'd0;    6'd1: o_dout = 8'd6;    6'd2: o_dout = 8'd13;   6'd3: o_dout = 8'd19;
+            6'd0: dout = 8'd0;    6'd1: dout = 8'd6;    6'd2: dout = 8'd13;   6'd3: dout = 8'd19;
-            6'd4: o_dout = 8'd25;   6'd5: o_dout = 8'd31;   6'd6: o_dout = 8'd37;   6'd7: o_dout = 8'd44;
+            6'd4: dout = 8'd25;   6'd5: dout = 8'd31;   6'd6: dout = 8'd37;   6'd7: dout = 8'd44;
-            6'd8: o_dout = 8'd50;   6'd9: o_dout = 8'd56;   6'd10: o_dout = 8'd62;  6'd11: o_dout = 8'd68;
+            6'd8: dout = 8'd50;   6'd9: dout = 8'd56;   6'd10: dout = 8'd62;  6'd11: dout = 8'd68;
-            6'd12: o_dout = 8'd74;  6'd13: o_dout = 8'd80;  6'd14: o_dout = 8'd86;  6'd15: o_dout = 8'd92;
+            6'd12: dout = 8'd74;  6'd13: dout = 8'd80;  6'd14: dout = 8'd86;  6'd15: dout = 8'd92;
-            6'd16: o_dout = 8'd98;  6'd17: o_dout = 8'd103; 6'd18: o_dout = 8'd109; 6'd19: o_dout = 8'd115;
+            6'd16: dout = 8'd98;  6'd17: dout = 8'd103; 6'd18: dout = 8'd109; 6'd19: dout = 8'd115;
-            6'd20: o_dout = 8'd120; 6'd21: o_dout = 8'd126; 6'd22: o_dout = 8'd131; 6'd23: o_dout = 8'd136;
+            6'd20: dout = 8'd120; 6'd21: dout = 8'd126; 6'd22: dout = 8'd131; 6'd23: dout = 8'd136;
-            6'd24: o_dout = 8'd142; 6'd25: o_dout = 8'd147; 6'd26: o_dout = 8'd152; 6'd27: o_dout = 8'd157;
+            6'd24: dout = 8'd142; 6'd25: dout = 8'd147; 6'd26: dout = 8'd152; 6'd27: dout = 8'd157;
-            6'd28: o_dout = 8'd162; 6'd29: o_dout = 8'd167; 6'd30: o_dout = 8'd171; 6'd31: o_dout = 8'd176;
+            6'd28: dout = 8'd162; 6'd29: dout = 8'd167; 6'd30: dout = 8'd171; 6'd31: dout = 8'd176;
-            6'd32: o_dout = 8'd180; 6'd33: o_dout = 8'd185; 6'd34: o_dout = 8'd189; 6'd35: o_dout = 8'd193;
+            6'd32: dout = 8'd180; 6'd33: dout = 8'd185; 6'd34: dout = 8'd189; 6'd35: dout = 8'd193;
-            6'd36: o_dout = 8'd197; 6'd37: o_dout = 8'd201; 6'd38: o_dout = 8'd205; 6'd39: o_dout = 8'd208;
+            6'd36: dout = 8'd197; 6'd37: dout = 8'd201; 6'd38: dout = 8'd205; 6'd39: dout = 8'd208;
-            6'd40: o_dout = 8'd212; 6'd41: o_dout = 8'd215; 6'd42: o_dout = 8'd219; 6'd43: o_dout = 8'd222;
+            6'd40: dout = 8'd212; 6'd41: dout = 8'd215; 6'd42: dout = 8'd219; 6'd43: dout = 8'd222;
-            6'd44: o_dout = 8'd225; 6'd45: o_dout = 8'd228; 6'd46: o_dout = 8'd231; 6'd47: o_dout = 8'd233;
+            6'd44: dout = 8'd225; 6'd45: dout = 8'd228; 6'd46: dout = 8'd231; 6'd47: dout = 8'd233;
-            6'd48: o_dout = 8'd236; 6'd49: o_dout = 8'd238; 6'd50: o_dout = 8'd240; 6'd51: o_dout = 8'd242;
+            6'd48: dout = 8'd236; 6'd49: dout = 8'd238; 6'd50: dout = 8'd240; 6'd51: dout = 8'd242;
-            6'd52: o_dout = 8'd244; 6'd53: o_dout = 8'd246; 6'd54: o_dout = 8'd247; 6'd55: o_dout = 8'd249;
+            6'd52: dout = 8'd244; 6'd53: dout = 8'd246; 6'd54: dout = 8'd247; 6'd55: dout = 8'd249;
-            6'd56: o_dout = 8'd250; 6'd57: o_dout = 8'd251; 6'd58: o_dout = 8'd252; 6'd59: o_dout = 8'd253;
+            6'd56: dout = 8'd250; 6'd57: dout = 8'd251; 6'd58: dout = 8'd252; 6'd59: dout = 8'd253;
-            6'd60: o_dout = 8'd254; 6'd61: o_dout = 8'd254; 6'd62: o_dout = 8'd255; 6'd63: o_dout = 8'd255;
+            6'd60: dout = 8'd254; 6'd61: dout = 8'd254; 6'd62: dout = 8'd255; 6'd63: dout = 8'd255;
-            default: o_dout=8'd0;
+            default: dout=8'd0;
        endcase
    end
-endmodule
+endmodule
--- a/cores/signal/nco_q15/tb/tb_nco_q15.v
+++ b/cores/signal/nco_q15/tb/tb_nco_q15.v
@@ -15,12 +15,12 @@ module tb_nco_q15();
    wire out_en;
    nco_q15 #(.CLK_HZ(120_000_000), .FS_HZ(40_000)) nco (
-        .i_clk    (clk),
+        .clk    (clk),
-        .i_rst_n  (resetn),
+        .rst_n  (resetn),
-        .i_freq_hz(freq),
+        .freq_hz(freq),
-        .o_sin_q15(sin_q15),
+        .sin_q15(sin_q15),
-        .o_cos_q15(cos_q15),
+        .cos_q15(cos_q15),
-        .o_clk_en (out_en)
+        .clk_en (out_en)
    );
    initial begin
@@ -39,4 +39,4 @@ module tb_nco_q15();
        $finish;
    end;
-endmodule
+endmodule
--- a/cores/signal/sd_adc_q15/rtl/rc_alpha_q15.vh
+++ b/cores/signal/sd_adc_q15/rtl/rc_alpha_q15.vh
@@ -1,91 +0,0 @@
 // rc_alpha_q15.vh
 // Plain Verilog-2001 constant function: R(ohm), C(pF), Fs(Hz) -> alpha_q15 (Q1.15)
 // Uses fixed-point approximation: 1 - exp(-x) ≈ x - x^2/2 + x^3/6, where x = 1/(Fs*R*C)
 // All integer math; suitable for elaboration-time constant folding (e.g., XST).
 `ifndef RC_ALPHA_Q15_VH
 `define RC_ALPHA_Q15_VH
 function integer alpha_q15_from_rc;
    input integer R_OHM; // ohms
    input integer C_PF;  // picofarads
    input integer FS_HZ; // Hz
    // Choose QN for x. N=24 is a good balance for accuracy/width.
    integer N;
    // We'll keep everything as unsigned vectors; inputs copied into vectors first.
    reg [63:0] R_u, C_u, FS_u;
    // x = 1 / (Fs * R * C) with C in pF -> x = 1e12 / (Fs*R*C_pf)
    // x_qN = round( x * 2^N ) = round( (1e12 << N) / denom )
    reg  [127:0] NUM_1E12_SLLN;  // big enough for 1e12 << N
    reg  [127:0] DENOM;          // Fs*R*C
    reg  [127:0] X_qN;           // x in QN
    // Powers
    reg  [255:0] X2;             // x^2 in Q(2N)
    reg  [383:0] X3;             // x^3 in Q(3N)
    integer term1_q15;
    integer term2_q15;
    integer term3_q15;
    integer acc;
 begin
    N = 24;
    // Copy integer inputs into 64-bit vectors (no bit-slicing of integers)
    R_u  = R_OHM[31:0];
    C_u  = C_PF[31:0];
    FS_u = FS_HZ[31:0];
    // Denominator = Fs * R * C_pf  (fits in < 2^64 for typical values)
    DENOM = 128'd0;
    DENOM = FS_u;
    DENOM = DENOM * R_u;
    DENOM = DENOM * C_u;
    // // Guard: avoid divide by zero
    // if (DENOM == 0) begin
    //     alpha_q15_from_rc = 0;
    //     disable alpha_q15_from_rc;
    // end
    // Numerator = (1e12 << N). 1e12 * 2^24 ≈ 1.6777e19 (fits in 2^64..2^65),
    // so use 128 bits to be safe.
    NUM_1E12_SLLN = 128'd1000000000000 << N;
    // x_qN = rounded division
    X_qN = (NUM_1E12_SLLN + (DENOM >> 1)) / DENOM;
    // Powers
    X2 = X_qN * X_qN;
    X3 = X2 * X_qN;
    // Convert terms to Q1.15:
    // term1 = x            -> shift from QN to Q15
    term1_q15 = (X_qN >> (N - 15)) & 16'hFFFF;
    // term2 = x^2 / 2      -> Q(2N) to Q15 and /2
    term2_q15 = (X2 >> (2*N - 15 + 1)) & 16'hFFFF;
    // term3 = x^3 / 6      -> Q(3N) to Q15, then /6 with rounding
    begin : gen_t3
        reg [383:0] tmp_q15_wide;
        reg [383:0] tmp_div6;
        tmp_q15_wide = (X3 >> (3*N - 15));
        tmp_div6     = (tmp_q15_wide + 6'd3) / 6;
        term3_q15    = tmp_div6[15:0];
    end
    // Combine and clamp
    acc = term1_q15 - term2_q15 + term3_q15;
    if (acc < 0)            acc = 0;
    else if (acc > 16'h7FFF) acc = 16'h7FFF;
    alpha_q15_from_rc = acc;
 end
 endfunction
 `endif
--- a/cores/signal/sd_adc_q15/rtl/rcmodel_q15.v
+++ b/cores/signal/sd_adc_q15/rtl/rcmodel_q15.v
@@ -1,55 +0,0 @@
 `timescale 1ns/1ps
 // =============================================================================
 // RC model to convert sigma delta samples to Q1.15
 // Models the RC circuit on the outside of the FPGA
 // Uses: Yn+1 = Yn + (sd - Yn)*(1-exp(-T/RC))
 // parameters:
 //      -- alpha_q15 : the 1-exp(-T/RC), defaults to R=3k3, C=220p and T=1/15MHz
 //							  rounded to only use two bits (0b3b -> 0b00), the less
 //							  bits the better
 // inout:
 //      -- i_clk : input clock
 //      -- i_rst_n : reset signal
 //      -- i_sd_sample : 1 bit sample output from sd sampler
 //      -- o_sample_q15 : output samples in q.15
 // =============================================================================
 module rcmodel_q15 #(
    parameter integer alpha_q15 = 16'sh0b00
 )(
    input wire i_clk,
    input wire i_rst_n,
    input wire i_sd_sample,
    output wire [15:0] o_sample_q15
 );
    reg signed [15:0] y_q15;
    wire signed [15:0] sd_q15 = i_sd_sample ? 16'sh7fff : 16'sh0000;
    wire signed [15:0] e_q15 = sd_q15 - y_q15;
    // wire signed [31:0] prod_q30 = $signed(e_q15) * $signed(alpha_q15);
    wire signed [31:0] prod_q30;
    // Use shift-add algorithm for multiplication
    mul_const_shiftadd #(
        .C($signed(alpha_q15)),
        .IN_W(16),
        .OUT_W(32)
    ) alpha_times_e (
        .i_x(e_q15),
        .o_y(prod_q30)
    );
    wire signed [15:0] y_next_q15 = y_q15 + (prod_q30>>>15);
    // clamp to [0, 0x7FFF] (keeps signal view tidy)
    function signed [15:0] clamp01_q15(input signed [15:0] v);
        if (v < 16'sd0000) clamp01_q15 = 16'sd0000;
        else if (v > 16'sh7FFF) clamp01_q15 = 16'sh7FFF;
        else clamp01_q15 = v;
    endfunction
    always @(posedge i_clk or negedge i_rst_n) begin
        if (!i_rst_n) y_q15 <= 16'sd0000;
        else y_q15 <= clamp01_q15(y_next_q15);
    end
    assign o_sample_q15 = y_q15;
 endmodule
--- a/cores/signal/sd_adc_q15/rtl/sd_adc_q15.v
+++ b/cores/signal/sd_adc_q15/rtl/sd_adc_q15.v
@@ -1,58 +0,0 @@
 module sd_adc_q15 #(
    parameter integer R_OHM = 3300,
    parameter integer C_PF = 220
 )(
    input wire i_clk_15,
    input wire i_rst_n,
    input wire i_adc_a,
    input wire i_adc_b,
    output wire o_adc,
    output wire signed [15:0] o_signal_q15,
    output wire o_signal_valid
 );
    `include "rc_alpha_q15.vh"
    wire sd_signal;
    wire signed [15:0] raw_sample_biased;
    wire signed [15:0] raw_sample_q15;
    wire signed [15:0] lpf_sample_q15;
    sd_sampler sd_sampler(
        .i_clk(i_clk_15),
        .i_a(i_adc_a), .i_b(i_adc_b),
        .o_sample(sd_signal)
    );
    assign o_adc = sd_signal;
    localparam integer alpha_q15_int = alpha_q15_from_rc(R_OHM, C_PF, 15000000);
    localparam signed [15:0] alpha_q15 = alpha_q15_int[15:0];
    localparam signed [15:0] alpha_q15_top = alpha_q15 & 16'hff00;
    rcmodel_q15 #(
        .alpha_q15(alpha_q15_top)
    ) rc_model (
        .i_clk(i_clk_15), .i_rst_n(i_rst_n),
        .i_sd_sample(sd_signal),
        .o_sample_q15(raw_sample_q15)
    );
    lpf_iir_q15_k #(
        .K(8)
    ) lpf (
        .i_clk(i_clk_15), .i_rst_n(i_rst_n),
        .i_x_q15(raw_sample_q15),
        .o_y_q15(lpf_sample_q15)
    );
    decimate_by_r_q15 #(
        // .R(200), // 15MHz/200 = 75KHz
        .R(375), // 15MHz/375 = 40KHz
        .CNT_W(10)
    ) decimate (
        .i_clk(i_clk_15), .i_rst_n(i_rst_n),
        .i_valid(1'b1), .i_q15(lpf_sample_q15),
        .o_valid(o_signal_valid), .o_q15(o_signal_q15)
    );
 endmodule
--- a/cores/signal/sd_adc_q15/rtl/sd_sampler.v
+++ b/cores/signal/sd_adc_q15/rtl/sd_sampler.v
@@ -1,18 +0,0 @@
 module sd_sampler(
    input wire i_clk,
    input wire i_a,
    input wire i_b,
    output wire o_sample
 );
    wire comp_out;
    lvds_comparator comp (
        .a(i_a), .b(i_b), .o(comp_out)
    );
    reg registered_comp_out;
    always @(posedge i_clk) 
        registered_comp_out <= comp_out;
    assign o_sample = registered_comp_out;
 endmodule
--- a/cores/signal/sd_adc_q15/sd_adc_q15.core
+++ b/cores/signal/sd_adc_q15/sd_adc_q15.core
@@ -1,57 +0,0 @@
 CAPI=2:
 name: joppeb:signal:sd_adc_q15:1.0
 description: Sigma-delta ADC front-end with Q1.15 output
 filesets:
    rtl_common:
        depend:
            - joppeb:primitive:lvds_comparator
            - joppeb:signal:lpf_iir_q15_k
            - joppeb:signal:decimate_by_r_q15
            - joppeb:util:mul_const
        files:
            - rtl/rc_alpha_q15.vh:
                is_include_file: true
            - rtl/rcmodel_q15.v
            - rtl/sd_adc_q15.v
        file_type: verilogSource
    rtl_sampler:
        files:
            - rtl/sd_sampler.v
        file_type: verilogSource
    sim_sampler:
        files:
            - sim/sd_sampler.v
        file_type: verilogSource
    tb:
        files:
            - tb/tb_sd_adc_q15.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - rtl_common
            - rtl_sampler
        toplevel: sd_adc_q15
        parameters:
            - R_OHM
            - C_PF
    sim:
        default_tool: icarus
        filesets:
            - rtl_common
            - sim_sampler
            - tb
        toplevel: tb_sd_adc_q15
 parameters:
    R_OHM:
        datatype: int
        description: RC filter resistor value in ohms
        paramtype: vlogparam
    C_PF:
        datatype: int
        description: RC filter capacitor value in pF
        paramtype: vlogparam
--- a/cores/signal/sd_adc_q15/sim/sd_sampler.v
+++ b/cores/signal/sd_adc_q15/sim/sd_sampler.v
@@ -1,111 +0,0 @@
 `timescale 1ns/1ps
 // =============================================================================
 // Sigma-Delta sampler
 // Simulates an RC circuit between o_sample and i_b and i_a sine at i_a
 // =============================================================================
 module sd_sampler(
    input wire i_clk,
    input wire i_a,
    input wire i_b,
    output wire o_sample
 );
    // Sine source (i_a input / P)
    parameter real    F_HZ       = 5000;   // input sine frequency (1 kHz)
    parameter real    AMP        = 1.5;     // sine amplitude (V)
    parameter real    VCM        = 1.65;    // common-mode (V), centered in 0..3.3V
    // Comparator behavior
    parameter real    VTH        = 0.0;     // threshold on (vp - vn)
    parameter real    VHYST      = 0.05;     // symmetric hysteresis half-width (V)
    parameter integer ADD_HYST   = 0;       // 1 to enable hysteresis
    // 1-bit DAC rails (feedback into RC)
    parameter real    VLOW       = 0.0;     // DAC 0 (V)
    parameter real    VHIGH      = 3.3;     // DAC 1 (V)
    // RC filter (i_b input / N)
    parameter real    R_OHMS     = 3300.0;  // 3.3k
    parameter real    C_FARADS   = 220e-12; // 220 pF
    // Integration step (ties to `timescale`)
    parameter integer TSTEP_NS   = 10;      // sim step in ns (choose << tau)
    // ===== Internal state (simulation only) =====
    real vp, vn;          // comparator i_a/i_b inputs
    real v_rc;            // RC node voltage (== vn)
    real v_dac;           // DAC output voltage from o_sample
    real t_s;             // time in seconds
    real dt_s;            // step in seconds
    real tau_s;           // R*C time constant in seconds
    real two_pi;
    reg  q;               // comparator latched output (pre-delay)
    reg  out;
    reg  sampler;
    initial sampler <= 1'b0;
    always @(posedge i_clk) begin
        sampler <= out;
    end
    assign o_sample = sampler;
    // Helper task: update comparator with optional hysteresis
    task automatic comp_update;
        real diff;
    begin
        diff = (vp - vn);
        if (ADD_HYST != 0) begin
            // simple symmetric hysteresis around VTH
            if (q && (diff < (VTH - VHYST))) q = 1'b0;
            else if (!q && (diff > (VTH + VHYST))) q = 1'b1;
            // else hold
        end else begin
            q = (diff > VTH) ? 1'b1 : 1'b0;
        end
    end
    endtask
    initial begin
        // Init constants
        two_pi = 6.283185307179586;
        tau_s  = R_OHMS * C_FARADS;       // ~7.26e-7 s
        dt_s   = TSTEP_NS * 1.0e-9;
        // Init states
        t_s  = 0.0;
        q    = 1'b0;                      // start low
        out  = 1'b0;
        v_dac= VLOW;
        v_rc = (VHIGH + VLOW)/2.0;        // start mid-rail to reduce start-up transient
        vn   = v_rc;
        vp   = VCM;
        // Main sim loop
        forever begin
            #(TSTEP_NS);                  // advance discrete time step
            t_s  = t_s + dt_s;
            // 1) Update DAC from previous comparator state
            v_dac = sampler ? VHIGH : VLOW;
            // 2) RC low-pass driven by DAC: Euler step
            //    dv = (v_dac - v_rc) * dt/tau
            v_rc  = v_rc + (v_dac - v_rc) * (dt_s / tau_s);
            vn    = v_rc;
            // 3) Input sine on i_a
            vp    = VCM + AMP * $sin(two_pi * F_HZ * t_s);
            // 4) Comparator decision (with optional hysteresis)
            comp_update();
            // 5) Output with propagation delay
            out = q;
        end
    end
 endmodule
--- a/cores/signal/sd_adc_q15/tb/tb_sd_adc_q15.v
+++ b/cores/signal/sd_adc_q15/tb/tb_sd_adc_q15.v
@@ -1,36 +0,0 @@
 `timescale 1ns/1ps
 module tb_sd_adc_q15();
    // Clock and reset generation
    reg clk;
    reg resetn;
    initial clk <= 1'b0;
    initial resetn <= 1'b0;
    always #6.667 clk <= !clk;
    initial #40 resetn <= 1'b1;
    // Default run
    initial begin
        $dumpfile("out.vcd");
        $dumpvars;
        #2_000_000
        $finish;
    end;
    wire sd_a;
    wire sd_b;
    wire sd_o;
    wire signed [15:0] decimated_q15;
    wire decimated_valid;
    sd_adc_q15 #(
        .R_OHM(3300),
        .C_PF(220)
    ) dut(
        .i_clk_15(clk), .i_rst_n(resetn),
        .i_adc_a(sd_a), .i_adc_b(sd_b), .o_adc(sd_o),
        .o_signal_q15(decimated_q15),
        .o_signal_valid(decimated_valid)
    );
 endmodule
--- a/cores/signal/signal_scope/rtl/signal_scope_q15.v
+++ b/cores/signal/signal_scope/rtl/signal_scope_q15.v
@@ -1,257 +0,0 @@
 `include "clog2.vh"
 module signal_scope_q15 #(
    parameter depth = 2**12,
    parameter chain = 1
 )(
    input wire i_clk,
    input wire i_rst,
    input wire [15:0] i_signal_a,
    input wire i_signal_valid_a,
    input wire [15:0] i_signal_b,
    input wire i_signal_valid_b,
    input wire [15:0] i_signal_c,
    input wire i_signal_valid_c,
    input wire [15:0] i_signal_d,
    input wire i_signal_valid_d
 );
    localparam aw = `CLOG2(depth);
    localparam [aw-1:0] depth_last = depth-1;
    localparam [31:0] reg_base_addr = 32'h8000_0000;
    localparam [3:0] reg_control = 4'h0;
    localparam [3:0] reg_status = 4'h1;
    localparam [3:0] reg_trig_val = 4'h2;
    (* ram_style = "block" *) reg [16*4-1:0] mem[depth-1:0];
    reg [aw-1:0] counter;
    reg count_enable;
    reg arm_req;
    reg trigger_enable;
    reg scope_armed;
    reg scope_triggered;
    reg capture_done;
    reg [1:0] trigger_channel;
    reg [15:0] trig_val;
    reg [15:0] trigger_prev;
    reg trigger_prev_valid;
    reg [15:0] signal_a;
    reg [15:0] signal_b;
    reg [15:0] signal_c;
    reg [15:0] signal_d;
    reg signal_a_pending;
    reg signal_b_pending;
    reg signal_c_pending;
    reg signal_d_pending;
    wire [31:0] wb_adr;
    wire [31:0] wb_dat;
    wire [3:0] wb_sel;
    wire wb_we;
    wire wb_cyc;
    wire wb_stb;
    reg [31:0] wb_rdt;
    reg wb_ack;
    wire [aw-1:0] wb_mem_idx = wb_adr[aw+2:3];
    wire wb_is_reg = (wb_adr[31:28] == reg_base_addr[31:28]);
    wire [3:0] wb_reg_idx = wb_adr[5:2];
    reg [15:0] trigger_sample;
    reg trigger_sample_valid;
    reg wb_mem_read_pending;
    reg wb_mem_read_half;
    reg wb_mem_read_oob;
    reg [16*4-1:0] wb_mem_rdata;
    jtag_wb_bridge #(
        .chain(chain),
        .byte_aligned(0)
    ) jtag_scope_bridge (
        .i_clk(i_clk),
        .i_rst(i_rst),
        .o_wb_adr(wb_adr),
        .o_wb_dat(wb_dat),
        .o_wb_sel(wb_sel),
        .o_wb_we(wb_we),
        .o_wb_cyc(wb_cyc),
        .o_wb_stb(wb_stb),
        .i_wb_rdt(wb_rdt),
        .i_wb_ack(wb_ack),
        .o_cmd_reset()
    );
    always @(*) begin
        case(trigger_channel)
            2'd0: begin
                trigger_sample = i_signal_a;
                trigger_sample_valid = i_signal_valid_a;
            end
            2'd1: begin
                trigger_sample = i_signal_b;
                trigger_sample_valid = i_signal_valid_b;
            end
            2'd2: begin
                trigger_sample = i_signal_c;
                trigger_sample_valid = i_signal_valid_c;
            end
            default: begin
                trigger_sample = i_signal_d;
                trigger_sample_valid = i_signal_valid_d;
            end
        endcase
    end
    always @(posedge i_clk) begin
        if(i_rst) begin
            counter <= {aw{1'b0}};
            count_enable <= 1'b0;
            arm_req <= 1'b0;
            trigger_enable <= 1'b0;
            scope_armed <= 1'b0;
            scope_triggered <= 1'b0;
            capture_done <= 1'b0;
            trigger_channel <= 2'd0;
            wb_ack <= 1'b0;
            wb_rdt <= 32'b0;
            trig_val <= 16'h0000;
            trigger_prev <= 16'h0000;
            trigger_prev_valid <= 1'b0;
            signal_a <= 0;
            signal_b <= 0;
            signal_c <= 0;
            signal_d <= 0;
            signal_a_pending <= 1'b0;
            signal_b_pending <= 1'b0;
            signal_c_pending <= 1'b0;
            signal_d_pending <= 1'b0;
            wb_mem_read_pending <= 1'b0;
            wb_mem_read_half <= 1'b0;
            wb_mem_read_oob <= 1'b0;
            wb_mem_rdata <= {(16*4){1'b0}};
        end else begin
            // Sample signals
            if(i_signal_valid_a) begin
                signal_a <= i_signal_a;
                signal_a_pending <= 1'b1;
            end
            if(i_signal_valid_b) begin
                signal_b <= i_signal_b;
                signal_b_pending <= 1'b1;
            end
            if(i_signal_valid_c) begin
                signal_c <= i_signal_c;
                signal_c_pending <= 1'b1;
            end
            if(i_signal_valid_d) begin
                signal_d <= i_signal_d;
                signal_d_pending <= 1'b1;
            end
            // Trigger on selected channel rising across trig_val.
            if(scope_armed && trigger_enable && !count_enable && trigger_sample_valid) begin
                if(trigger_prev_valid &&
                   ($signed(trigger_prev) < $signed(trig_val)) &&
                   ($signed(trigger_sample) >= $signed(trig_val))) begin
                    count_enable <= 1'b1;
                    scope_triggered <= 1'b1;
                end
                trigger_prev <= trigger_sample;
                trigger_prev_valid <= 1'b1;
            end
            // Arm/rearm capture. If trigger is disabled, start capture immediately.
            if(arm_req) begin
                counter <= {aw{1'b0}};
                count_enable <= !trigger_enable;
                scope_armed <= 1'b1;
                scope_triggered <= !trigger_enable;
                capture_done <= 1'b0;
                trigger_prev_valid <= 1'b0;
                signal_a_pending <= 1'b0;
                signal_b_pending <= 1'b0;
                signal_c_pending <= 1'b0;
                signal_d_pending <= 1'b0;
            end
            // Write one full 4-channel frame at a time for maximum BRAM throughput.
            if(count_enable && signal_a_pending && signal_b_pending && signal_c_pending && signal_d_pending) begin
                if(counter <= depth_last) begin
                    mem[counter] <= {signal_a, signal_b, signal_c, signal_d};
                    counter <= counter + {{(aw-1){1'b0}}, 1'b1};
                    if(counter == depth_last) begin
                        count_enable <= 1'b0;
                        scope_armed <= 1'b0;
                        capture_done <= 1'b1;
                    end
                end else begin
                    count_enable <= 1'b0;
                    scope_armed <= 1'b0;
                    capture_done <= 1'b1;
                end
                signal_a_pending <= 1'b0;
                signal_b_pending <= 1'b0;
                signal_c_pending <= 1'b0;
                signal_d_pending <= 1'b0;
            end
            // WB slave response: register window + capture memory window.
            arm_req <= 1'b0;
            wb_ack <= 1'b0;
            if(wb_mem_read_pending) begin
                wb_ack <= 1'b1;
                wb_rdt <= wb_mem_read_oob ? 32'b0 :
                          (wb_mem_read_half ? wb_mem_rdata[63:32] : wb_mem_rdata[31:0]);
                wb_mem_read_pending <= 1'b0;
            end else if(wb_cyc & wb_stb) begin
                if(wb_we) begin
                    wb_ack <= 1'b1;
                    wb_rdt <= 32'b0;
                    if(wb_is_reg) begin
                        // Keep register write decode in one case so new writable registers
                        // can be added without touching memory-path logic.
                        case(wb_reg_idx)
                            reg_control: begin
                                if(wb_sel[0]) begin
                                    // Bit 0: write-1 pulse to arm/rearm scope.
                                    if(wb_dat[0])
                                        arm_req <= 1'b1;
                                    // Bit 1: trigger enable.
                                    trigger_enable <= wb_dat[1];
                                    // Bits [3:2]: trigger channel (0=a,1=b,2=c,3=d).
                                    trigger_channel <= wb_dat[3:2];
                                end
                            end
                            reg_trig_val: begin
                                if(wb_sel[0]) trig_val[7:0] <= wb_dat[7:0];
                                if(wb_sel[1]) trig_val[15:8] <= wb_dat[15:8];
                            end
                            default: begin
                            end
                        endcase
                    end
                end else begin
                    if(wb_is_reg) begin
                        wb_ack <= 1'b1;
                        case(wb_reg_idx)
                            // [3:2]=trigger_channel, [1]=trigger_enable, [0]=arm(write pulse only/read 0).
                            reg_control: wb_rdt <= {28'b0, trigger_channel, trigger_enable, 1'b0};
                            // [0]=triggered, [1]=capturing, [2]=armed, [3]=done
                            reg_status: wb_rdt <= {28'b0, capture_done, scope_armed, count_enable, scope_triggered};
                            reg_trig_val: wb_rdt <= {16'b0, trig_val};
                            default: wb_rdt <= 32'b0;
                        endcase
                    end else begin
                        // Synchronous RAM read for BRAM inference: issue read now, acknowledge next cycle.
                        wb_mem_rdata <= mem[wb_mem_idx];
                        wb_mem_read_half <= wb_adr[2];
                        wb_mem_read_oob <= (wb_mem_idx > depth_last);
                        wb_mem_read_pending <= 1'b1;
                    end
                end
            end
        end
    end
 endmodule
--- a/cores/signal/signal_scope/signal_scope_q15.core
+++ b/cores/signal/signal_scope/signal_scope_q15.core
@@ -1,32 +0,0 @@
 CAPI=2:
 name: joppeb:signal:signal_scope_q15:1.0
 description: Simple signal capture buffer for debug/scope use
 filesets:
    rtl:
        depend:
            - joppeb:util:clog2
            - joppeb:wb:jtag_wb_bridge
        files:
            - rtl/signal_scope_q15.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - rtl
        toplevel: signal_scope_q15
        parameters:
            - depth
            - chain
 parameters:
    depth:
        datatype: int
        description: Number of samples stored in internal memory
        paramtype: vlogparam
    chain:
        datatype: int
        description: JTAG chain identifier 
        paramtype: vlogparam
--- a/cores/signal/signal_scope/tool/capture_plot.py
+++ b/cores/signal/signal_scope/tool/capture_plot.py
@@ -1,243 +0,0 @@
 #!/usr/bin/env python3
 import argparse
 import sys
 import time
 from pathlib import Path
 import matplotlib.pyplot as plt
 MEM_BASE = 0x00000000
 REG_BASE = 0x80000000
 REG_CONTROL = REG_BASE + 0x00
 REG_STATUS = REG_BASE + 0x04
 REG_TRIG_VAL = REG_BASE + 0x08
 def _add_bridge_module_path() -> None:
    here = Path(__file__).resolve()
    bridge_tool = here.parents[3] / "wb" / "jtag_wb_bridge" / "tool"
    sys.path.insert(0, str(bridge_tool))
 def _to_signed(value: int, width: int) -> int:
    if width <= 0:
        return value
    sign_bit = 1 << (width - 1)
    mask = (1 << width) - 1
    value &= mask
    return value - (1 << width) if (value & sign_bit) else value
 def parse_args() -> argparse.Namespace:
    parser = argparse.ArgumentParser(
        description="Arm signal_scope once, dump samples over JTAG WB, and plot them."
    )
    parser.add_argument("--port", type=int, default=0, help="Digilent device index")
    parser.add_argument("--chain", type=int, default=1, help="JTAG USER chain")
    parser.add_argument("--selector", type=str, default=None, help="Optional device selector string")
    parser.add_argument(
        "--depth",
        type=int,
        default=1024,
        help="Number of scope frames to read (must match RTL depth)",
    )
    parser.add_argument(
        "--wait-s",
        type=float,
        default=0.05,
        help="Seconds to wait after arm/dearm before reading",
    )
    parser.add_argument(
        "--trigger-value",
        type=lambda x: int(x, 0),
        default=None,
        help="Optional trigger threshold (16-bit, signal_a rising crossing). If omitted, triggering is disabled.",
    )
    parser.add_argument(
        "--trigger-channel",
        choices=["a", "b", "c", "d"],
        default="a",
        help="Trigger source channel when triggering is enabled",
    )
    parser.add_argument(
        "--unsigned",
        action="store_true",
        help="Plot samples as unsigned (default: signed two's complement)",
    )
    parser.add_argument("--out", type=str, default=None, help="Optional PNG output path")
    parser.add_argument(
        "--dump-csv",
        type=str,
        default=None,
        help="Optional CSV output path with columns: index,value",
    )
    parser.add_argument(
        "--interactive",
        action="store_true",
        help="Keep running: press Enter to recapture/replot in the same window",
    )
    parser.add_argument(
        "--continuous",
        action="store_true",
        help="Keep running and recapture continuously without waiting for Enter",
    )
    return parser.parse_args()
 def capture_once(bridge, args: argparse.Namespace) -> list[tuple[int, int, int, int]]:
    samples = []
    frame_count = args.depth
    trigger_channel_map = {"a": 0, "b": 1, "c": 2, "d": 3}
    trigger_channel = trigger_channel_map[args.trigger_channel]
    if args.trigger_value is None:
        print("[signal_scope] Arming scope with trigger disabled...")
        bridge.write32(REG_CONTROL, 0x1)  # bit0: arm pulse, bit1: trigger enable=0
    else:
        trig_val = args.trigger_value & 0xFFFF
        print(
            f"[signal_scope] Config trigger: trig_val=0x{trig_val:04x}, "
            f"source=signal_{args.trigger_channel} rising"
        )
        bridge.write32(REG_TRIG_VAL, trig_val)
        print("[signal_scope] Arming scope with trigger enabled...")
        bridge.write32(REG_CONTROL, 0x3 | (trigger_channel << 2))  # bit0: arm, bit1: trig_en, bits[3:2]: channel
        # Wait until the new arm command is active, then wait for its trigger event.
        while (bridge.read32(REG_STATUS) & 0x4) == 0:
            time.sleep(0.001)
        print("[signal_scope] Waiting for trigger...")
        while True:
            status = bridge.read32(REG_STATUS)
            if status & 0x1:
                break
            time.sleep(0.001)
    if args.wait_s > 0:
        print(f"[signal_scope] Waiting {args.wait_s:.3f}s for capture to complete...")
        time.sleep(args.wait_s)
    print(f"[signal_scope] Reading back {frame_count} frames...")
    for idx in range(frame_count):
        base = MEM_BASE + idx * 8
        low = bridge.read32(base)
        high = bridge.read32(base + 4)
        ch_a = low & 0xFFFF
        ch_b = (low >> 16) & 0xFFFF
        ch_c = high & 0xFFFF
        ch_d = (high >> 16) & 0xFFFF
        if not args.unsigned:
            ch_a = _to_signed(ch_a, 16)
            ch_b = _to_signed(ch_b, 16)
            ch_c = _to_signed(ch_c, 16)
            ch_d = _to_signed(ch_d, 16)
        samples.append((ch_a, ch_b, ch_c, ch_d))
        if idx and (idx % max(1, frame_count // 10) == 0):
            pct = (100 * idx) // frame_count
    print(f"[signal_scope] Read complete: {len(samples)} frames")
    return samples
 def write_csv(samples: list[tuple[int, int, int, int]], csv_path: Path) -> None:
    print(f"[signal_scope] Writing CSV to {csv_path}...")
    with csv_path.open("w", encoding="utf-8") as f:
        f.write("index,ch_a,ch_b,ch_c,ch_d\n")
        for idx, values in enumerate(samples):
            f.write(f"{idx},{values[0]},{values[1]},{values[2]},{values[3]}\n")
    print(f"Wrote CSV: {csv_path}")
 def plot_samples(ax, samples: list[tuple[int, int, int, int]], args: argparse.Namespace, capture_idx: int) -> None:
    series = [[], [], [], []]
    for ch_a, ch_b, ch_c, ch_d in samples:
        series[0].append(ch_a)
        series[1].append(ch_b)
        series[2].append(ch_c)
        series[3].append(ch_d)
    ax.cla()
    ax.plot(series[0], linewidth=1, label="ch_d")
    ax.plot(series[1], linewidth=1, label="ch_c")
    ax.plot(series[2], linewidth=1, label="ch_b")
    ax.plot(series[3], linewidth=1, label="ch_a")
    ax.set_title(f"signal_scope_q15 capture #{capture_idx} (depth={args.depth}, chain={args.chain})")
    ax.set_xlabel("Sample")
    ax.set_ylabel("Value")
    if not args.unsigned:
        ax.set_ylim([-2**15, 2**15])
    ax.grid(True, alpha=0.3)
    ax.legend(loc="upper right")
 def main() -> int:
    args = parse_args()
    if args.depth <= 0:
        raise ValueError("--depth must be > 0")
    _add_bridge_module_path()
    from libjtag_wb_bridge.jtag_bridge import JtagBridge  # pylint: disable=import-error
    print(
        f"[signal_scope] Starting capture: port={args.port}, chain={args.chain}, "
        f"depth={args.depth}, selector={args.selector!r}"
    )
    with JtagBridge() as bridge:
        print("[signal_scope] Opening JTAG bridge...")
        if args.selector:
            bridge.open_selector(args.selector, port=args.port, chain=args.chain)
        else:
            bridge.open(port=args.port, chain=args.chain)
        print("[signal_scope] Bridge opened")
        print("[signal_scope] Clearing bridge flags and sending ping...")
        bridge.clear_flags()
        bridge.ping()
        print("[signal_scope] Bridge ready")
        status = bridge.read32(REG_STATUS)
        print(f"[signal_scope] Status: 0x{status:08x}")
        fig, ax = plt.subplots(figsize=(12, 4))
        capture_idx = 1
        while True:
            print(f"[signal_scope] Capture cycle #{capture_idx}")
            samples = capture_once(bridge, args)
            plot_samples(ax, samples, args, capture_idx)
            fig.tight_layout()
            fig.canvas.draw_idle()
            fig.canvas.flush_events()
            if args.dump_csv:
                write_csv(samples, Path(args.dump_csv))
            if args.out:
                out_path = Path(args.out)
                print(f"[signal_scope] Saving plot to {out_path}...")
                fig.savefig(out_path, dpi=150)
                print(f"Wrote plot: {out_path}")
            if not args.interactive and not args.continuous:
                break
            plt.show(block=False)
            if args.continuous:
                capture_idx += 1
                continue
            answer = input("[signal_scope] Press Enter to recapture, or 'q' + Enter to quit: ")
            if answer.strip().lower().startswith("q"):
                break
            capture_idx += 1
        if not args.out:
            print("[signal_scope] Showing plot window...")
            plt.show()
    print("[signal_scope] Done")
    return 0
 if __name__ == "__main__":
    raise SystemExit(main())
--- a/cores/system/mcu/rtl/mcu_peripherals.v
+++ b/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];
@@ -91,15 +89,15 @@ module mcu_peripherals (
    );
    wb_gpio_banks #(
-        .num_banks(4)
+        .BASE_ADDR(GPIO_BASE_ADDR),
        .NUM_BANKS(4)
    ) gpio (
-        .i_clk(i_clk),
+        .i_wb_clk(i_clk),
-        .i_rst(i_rst),
+        .i_wb_rst(i_rst),
        .i_wb_dat(gpio_wbs_dat_w),
        .i_wb_adr(gpio_wbs_adr),
        .i_wb_we(gpio_wbs_we),
-        .i_wb_stb(gpio_wbs_stb),
+        .i_wb_stb(gpio_wbs_stb & gpio_wbs_cyc),
        .i_wb_cyc(gpio_wbs_cyc),
        .i_wb_sel(gpio_wbs_sel),
        .o_wb_rdt(gpio_wbs_dat_r),
        .o_wb_ack(gpio_wbs_ack),
@@ -114,10 +112,8 @@ module mcu_peripherals (
        .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),
--- a/cores/system/mimas_sd_adc_r2r/mimas.ucf
+++ b/cores/system/mimas_sd_adc_r2r/mimas.ucf
@@ -1,54 +0,0 @@
 # Main clock input
 NET "aclk" LOC = P126;
 NET "aclk" TNM_NET = "SYS_CLK_PIN";
 TIMESPEC TS_SYS_CLK_PIN = PERIOD "SYS_CLK_PIN" 10 ns HIGH 50 %;
 # Boards button row
 NET "aresetn" LOC = P120;
 NET "aresetn" IOSTANDARD = LVCMOS33;
 NET "aresetn" PULLUP;
 NET "adc_a" LOC = P33;
 NET "adc_a" IOSTANDARD = LVDS_33;
 NET "adc_b" LOC = P32;
 NET "adc_b" IOSTANDARD = LVDS_33;
 NET "adc_o" LOC = P34;
 NET "adc_o" IOSTANDARD = LVCMOS33;
 NET "r2r[0]" LOC = P131;
 NET "r2r[1]" LOC = P133;
 NET "r2r[2]" LOC = P137;
 NET "r2r[3]" LOC = P139;
 NET "r2r[4]" LOC = P141;
 NET "r2r[5]" LOC = P1;
 NET "r2r[0]" IOSTANDARD = LVCMOS33;
 NET "r2r[1]" IOSTANDARD = LVCMOS33;
 NET "r2r[2]" IOSTANDARD = LVCMOS33;
 NET "r2r[3]" IOSTANDARD = LVCMOS33;
 NET "r2r[4]" IOSTANDARD = LVCMOS33;
 NET "r2r[5]" IOSTANDARD = LVCMOS33;
 NET "LED[0]" LOC = P119;
 NET "LED[0]" IOSTANDARD = LVCMOS33;
 NET "LED[0]" DRIVE = 8;
 NET "LED[1]" LOC = P118;
 NET "LED[1]" IOSTANDARD = LVCMOS33;
 NET "LED[1]" DRIVE = 8;
 NET "LED[2]" LOC = P117;
 NET "LED[2]" IOSTANDARD = LVCMOS33;
 NET "LED[2]" DRIVE = 8;
 NET "LED[3]" LOC = P116;
 NET "LED[3]" IOSTANDARD = LVCMOS33;
 NET "LED[3]" DRIVE = 8;
 NET "LED[4]" LOC = P115;
 NET "LED[4]" IOSTANDARD = LVCMOS33;
 NET "LED[4]" DRIVE = 8;
 NET "LED[5]" LOC = P114;
 NET "LED[5]" IOSTANDARD = LVCMOS33;
 NET "LED[5]" DRIVE = 8;
 NET "LED[6]" LOC = P112;
 NET "LED[6]" IOSTANDARD = LVCMOS33;
 NET "LED[6]" DRIVE = 8;
 NET "LED[7]" LOC = P111;
 NET "LED[7]" IOSTANDARD = LVCMOS33;
 NET "LED[7]" DRIVE = 8;
--- a/cores/system/mimas_sd_adc_r2r/mimas_sd_adc_r2r.core
+++ b/cores/system/mimas_sd_adc_r2r/mimas_sd_adc_r2r.core
@@ -1,47 +0,0 @@
 CAPI=2:
 name: joppeb:system:mimas_sd_adc_r2r:1.0
 description: Mimas top-level wiring sigma-delta ADC output directly to R2R DAC
 filesets:
    rtl:
        depend:
            - joppeb:primitive:clkgen
            - joppeb:signal:sd_adc_q15
            - joppeb:util:conv
            - joppeb:signal:signal_scope_q15
        files:
            - rtl/toplevel.v
        file_type: verilogSource
    mimas:
        files:
            - mimas.ucf : {file_type : UCF}
            - options.tcl : {file_type : tclSource}
 targets:
    default:
        filesets:
            - rtl
        toplevel: toplevel
    mimas:
        filesets:
            - rtl
            - mimas
        toplevel: toplevel
        parameters:
            - FPGA_SPARTAN6=true
        default_tool: ise
        tools:
            ise:
                family: Spartan6
                device: xc6slx9
                package: tqg144
                speed: -2
 parameters:
    FPGA_SPARTAN6:
        datatype: bool
        description: Select Spartan-6 family specific implementations
        paramtype: vlogdefine
--- a/cores/system/mimas_sd_adc_r2r/options.tcl
+++ b/cores/system/mimas_sd_adc_r2r/options.tcl
@@ -1,2 +0,0 @@
 project set "Create Binary Configuration File" TRUE -process "Generate Programming File"
 project set "Keep Hierarchy" Yes -process "Synthesize - XST"
--- a/cores/system/mimas_sd_adc_r2r/rtl/toplevel.v
+++ b/cores/system/mimas_sd_adc_r2r/rtl/toplevel.v
@@ -1,106 +0,0 @@
 `timescale 1ns/1ps
 module toplevel(
    input wire aclk,
    input wire aresetn,
    input wire adc_a,
    input wire adc_b,
    output wire adc_o,
    output wire [5:0] r2r,
    output wire [7:0] LED
 );
    `include "conv.vh"
    // Clocking
    wire clk_100;
    assign clk_100 = aclk;
    wire clk_15;
    clkgen #(
        .CLK_IN_HZ(100000000),
        .CLKFX_DIVIDE(20),
        .CLKFX_MULTIPLY(3)
    ) clk_gen_15 (
        .clk_in(clk_100),
        .clk_out(clk_15)
    );
    // Asynchronous assert on reset button, synchronous release in clk_15 domain.
    localparam [17:0] RESET_RELEASE_CYCLES = 18'd150000; // ~10 ms @ 15 MHz
    reg [17:0] rst_cnt = 18'd0;
    reg        sys_reset_r = 1'b1;
    always @(posedge clk_15 or negedge aresetn) begin
        if (!aresetn) begin
            rst_cnt <= 18'd0;
            sys_reset_r <= 1'b1;
        end else if (sys_reset_r) begin
            if (rst_cnt == RESET_RELEASE_CYCLES - 1'b1)
                sys_reset_r <= 1'b0;
            else
                rst_cnt <= rst_cnt + 1'b1;
        end
    end
    wire signed [15:0] signal_q15;
    wire signal_valid;
    sd_adc_q15 #(
        .R_OHM(3300),
        .C_PF(220)
    ) sd_adc (
        .i_clk_15(clk_15),
        .i_rst_n(!sys_reset_r),
        .i_adc_a(adc_a),
        .i_adc_b(adc_b),
        .o_adc(adc_o),
        .o_signal_q15(signal_q15),
        .o_signal_valid(signal_valid)
    );
    // signal_q15 is unipolar and biased (0-3.3V -> 0..32767)
    reg signed [15:0] signal_unbiased_q15 = 16'sd0;
    reg signal_unbiased_valid = 1'b0;
    localparam bias = 2**14;
    localparam gain = 2;
    always @(posedge clk_15) begin
        if (sys_reset_r) begin
            signal_unbiased_q15 <= 16'sd0;
            signal_unbiased_valid <= 1'b0;
        end else begin
            signal_unbiased_valid <= signal_valid;
            if (signal_valid) begin
                signal_unbiased_q15 <= (signal_q15 - $signed(bias)) * gain;
            end
        end
    end
    reg [5:0] dac_code = 6'd0;
    always @(posedge clk_15) begin
        if (sys_reset_r)
            dac_code <= 6'd0;
        else if (signal_unbiased_valid)
            dac_code <= q15_to_uq16(signal_unbiased_q15) >> 10;
    end
    assign r2r = dac_code;
    // Quick status indication: show ADC validity and most recent DAC code.
    assign LED[0] = signal_valid;
    assign LED[6:1] = dac_code;
    assign LED[7] = sys_reset_r;
    signal_scope_q15 #(
        .depth(2**13),
        .chain(1)
    ) scope1 (
        .i_clk(clk_15),
        .i_rst(sys_reset_r),
        .i_signal_a(signal_q15),
        .i_signal_valid_a(signal_valid),
        .i_signal_b(signal_unbiased_q15),
        .i_signal_valid_b(signal_unbiased_valid),
        .i_signal_valid_c(signal_valid),
        .i_signal_valid_d(signal_valid)
    );
 endmodule
--- a/cores/system/test/rtl/toplevel.v
+++ b/cores/system/test/rtl/toplevel.v
@@ -1,8 +1,7 @@
 `timescale 1ns/1ps
 module toplevel #(
-    parameter sim = 0,
+    parameter sim = 0
    parameter memfile = "sweep.hex"
 )(
    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 (
@@ -81,12 +80,12 @@ module toplevel #(
        .CLK_HZ(15_000_000),
        .FS_HZ(80_000)
    ) nco (
-        .i_clk    (clk_15),
+        .clk    (clk_15),
-        .i_rst_n  (sys_resetn),
+        .rst_n  (sys_resetn),
-        .i_freq_hz(GPIO_A),
+        .freq_hz(GPIO_A),
-        .o_sin_q15(sin_q15),
+        .sin_q15(sin_q15),
-        .o_cos_q15(),
+        .cos_q15(),
-        .o_clk_en (clk_en)
+        .clk_en (clk_en)
    );
    reg [5:0] dac_code;
--- a/cores/system/test/sw/sweep/sweep.c
+++ b/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      = (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)
@@ -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;
+    *LEDGR = 3;
-    *TIMER_LD = 1000 * 15000;
+    *TIMER = 1840000*2;
    for(;;){
-        for(int i=500; i<6000; 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<800; j++) asm volatile("nop");
        }
    }
 }
--- a/cores/system/test/tb/tb_toplevel.v
+++ b/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
--- a/cores/system/test/test.core
+++ b/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:
--- a/cores/util/mul_const/mul_const.core
+++ b/cores/util/mul_const/mul_const.core
@@ -1,15 +0,0 @@
 CAPI=2:
 name: joppeb:util:mul_const:1.0
 description: Constant multiplier helpers implemented with shift-add logic
 filesets:
    rtl:
        files:
            - rtl/mul_const.v
        file_type: verilogSource
 targets:
    default:
        filesets:
            - rtl
--- a/cores/util/mul_const/rtl/mul_const.v
+++ b/cores/util/mul_const/rtl/mul_const.v
@@ -1,31 +0,0 @@
 `timescale 1ns/1ps
 module mul_const_shiftadd #(
    parameter integer C = 0,
    parameter integer IN_W = 16,
    parameter integer OUT_W = 32
 )(
    input  wire signed [IN_W-1:0] i_x,
    output reg  signed [OUT_W-1:0] o_y
 );
    integer k;
    integer abs_c;
    reg signed [OUT_W-1:0] acc;
    reg signed [OUT_W-1:0] x_ext;
    always @* begin
        abs_c = (C < 0) ? -C : C;
        acc = {OUT_W{1'b0}};
        x_ext = {{(OUT_W-IN_W){i_x[IN_W-1]}}, i_x};
        for (k = 0; k < 32; k = k + 1) begin
            if (abs_c[k])
                acc = acc + (x_ext <<< k);
        end
        if (C < 0)
            o_y = -acc;
        else
            o_y = acc;
    end
 endmodule
--- a/cores/wb/formal_checker/formal/formal_wb_master_checker.v
+++ b/cores/wb/formal_checker/formal/formal_wb_master_checker.v
@@ -1,205 +1,74 @@
-// formal_wb_master_checker.v
+`timescale 1ns/1ps
 //
 // Wishbone Classic master-side protocol checker (plain Verilog).
 // Use when your DUT is a *master* and the bus/slave is the environment.
-module formal_wb_master_checker #(
+module formal_wb_master_checker (
-    parameter OPT_USE_ERR              = 0,
+    input wire        i_clk,
-    parameter OPT_USE_RTY              = 0,
+    input wire        i_rst,
-
+    input wire        i_wb_rst,
-    // If 1: require responses only when STB=1 (stricter than spec permission).
+    input wire [31:0] i_wb_adr,
-    // If 0: allow "ghost" responses with STB=0; we only COUNT termination when STB=1.
+    input wire [31:0] i_wb_dat,
-    parameter OPT_STRICT_RESP_WITH_STB = 0,
+    input wire [3:0]  i_wb_sel,
-
+    input wire        i_wb_we,
-    // If 1: require ACK/ERR/RTY to be single-cycle pulses.
+    input wire        i_wb_stb,
-    // If 0: allow them to be held.
+    input wire        i_wb_cyc,
-    parameter OPT_PULSE_RESP           = 1,
+    input wire [31:0] o_wb_rdt,
-
+    input wire        o_wb_ack
    // If 1: after a synchronous reset has been asserted for one clock,
    // require the master to hold CYC/STB low.
    parameter OPT_STRICT_RESET         = 1,
    // Optional widths
    parameter AW = 32,
    parameter DW = 32,
    parameter SW = 4
 ) (
    input  wire              i_clk,
    input  wire              i_rst,
    input  wire              i_wb_rst,
    // Master -> bus
    input  wire              i_wb_cyc,
    input  wire              i_wb_stb,
    input  wire              i_wb_we,
    input  wire [AW-1:0]     i_wb_adr,
    input  wire [DW-1:0]     i_wb_dat,
    input  wire [SW-1:0]     i_wb_sel,
    // Bus/slave -> master
    input  wire              o_wb_ack,
    input  wire              o_wb_err,
    input  wire              o_wb_rty,
    input  wire [DW-1:0]     o_wb_rdt
 );
 `ifdef FORMAL
    // -----------------------------
    // Reset combine
    // -----------------------------
    wire rst_any;
    assign rst_any = i_rst | i_wb_rst;
    // -----------------------------
    // Formal infrastructure
    // -----------------------------
    reg f_past_valid;
    initial f_past_valid = 1'b0;
-    always @(posedge i_clk)
+
    always @(posedge i_clk) begin
        f_past_valid <= 1'b1;
-    wire f_resp_any;
+        // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
-    assign f_resp_any = o_wb_ack
+        if(o_wb_ack)
-                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
+            assume(
-                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
+                (i_wb_cyc && i_wb_stb) ||
                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
            );
-    // A "real" termination in Classic requires STB high (handshake qualifies the transfer)
+        // A2: Slave must not ACK outside an active cycle
-    wire f_terminate;
+        if(!i_wb_cyc)
-    assign f_terminate = i_wb_cyc && i_wb_stb && f_resp_any;
+            assume(!o_wb_ack);
-    // -----------------------------
+        // A3: Once STB has been low for a full cycle, slave ACK must be low
-    // Track exactly one outstanding request (Classic)
+        if(
-    // -----------------------------
+            f_past_valid &&
-    reg f_pending;
+            !$past(i_wb_stb) &&
-    initial f_pending = 1'b0;
+            !i_wb_stb
        )
            assume(!o_wb_ack);
-    always @(posedge i_clk or posedge rst_any) begin
+        // R1: Reset must leave the master initialized on the following cycle
-        if (rst_any) begin
+        if(f_past_valid && $past(i_rst || i_wb_rst)) begin
-            f_pending <= 1'b0;
+            assert(!i_wb_cyc);
-        end else if (!i_wb_cyc) begin
+            assert(!i_wb_stb);
            // Dropping CYC ends the bus cycle and clears any outstanding request
            f_pending <= 1'b0;
        end else begin
            // Start pending when STB is asserted and none is pending
            if (!f_pending && i_wb_stb)
                f_pending <= 1'b1;
            // Clear pending only on a real termination (STB && response)
            if (f_terminate)
                f_pending <= 1'b0;
        end
        // R2: STB never high without CYC
        if(i_wb_stb)
            assert(i_wb_cyc);
        // R3: Once a request starts, hold it stable until the slave responds
        if(
            f_past_valid &&
            !$past(i_rst || i_wb_rst) &&
            $past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
            !o_wb_ack &&
            !(i_rst || i_wb_rst)
        ) begin
            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
        // R4: Once CYC is low, STB must also be low
        if(!i_wb_cyc)
            assert(!i_wb_stb);
    end
-    // -----------------------------
+    wire unused = &{1'b0, o_wb_rdt};
    // Reset rules (Wishbone synchronous reset semantics)
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid) begin
        if (rst_any) begin
            // R00: Monitor pending state must be cleared during reset
            R00: assert(f_pending == 1'b0);
            if (OPT_STRICT_RESET && $past(rst_any)) begin
                // R01: After reset was asserted on the prior clock, master must be idle
                R01: assert(!i_wb_cyc);
                // R02: After reset was asserted on the prior clock, master must not strobe
                R02: assert(!i_wb_stb);
            end
            if ($past(rst_any)) begin
                // A00: After reset was asserted on the prior clock, environment should not respond
                A00: assume(!o_wb_ack);
                if (OPT_USE_ERR) A01: assume(!o_wb_err);
                if (OPT_USE_RTY) A02: assume(!o_wb_rty);
            end
        end
    end
    // -----------------------------
    // Master-side RULES (ASSERTIONS)
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid && !rst_any) begin
        // R10: STB must imply CYC (no strobe outside of a cycle)
        if (i_wb_stb) begin
            R10: assert(i_wb_cyc);
        end
        // R11: While a request is pending and NOT terminated, master must keep CYC asserted
        if ($past(f_pending) && !$past(f_terminate)) begin
            R11: assert(i_wb_cyc);
        end
        // R12: While a request is pending and NOT terminated, master must keep STB asserted
        if ($past(f_pending) && !$past(f_terminate)) begin
            R12: assert(i_wb_stb);
        end
        // R13: Address stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            R13: assert(i_wb_adr == $past(i_wb_adr));
        end
        // R14: WE stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            R14: assert(i_wb_we == $past(i_wb_we));
        end
        // R15: SEL stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            R15: assert(i_wb_sel == $past(i_wb_sel));
        end
        // R16: Write data stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            R16: assert(i_wb_dat == $past(i_wb_dat));
        end
    end
    // -----------------------------
    // Environment SLAVE assumptions
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid && !rst_any) begin
        // A10: Any response must occur only during an active cycle
        if (f_resp_any) begin
            A10: assume(i_wb_cyc);
        end
        // A11: Optional strict profile: response only when STB=1
        if (OPT_STRICT_RESP_WITH_STB && f_resp_any) begin
            A11: assume(i_wb_stb);
        end
        // A12-A14: Mutual exclusion between ACK/ERR/RTY (recommended)
        if (o_wb_ack) begin
            if (OPT_USE_ERR) A12s1: assume(!o_wb_err);
            if (OPT_USE_RTY) A12s2: assume(!o_wb_rty);
        end
        if (OPT_USE_ERR && o_wb_err) begin
            A13s1: assume(!o_wb_ack);
            if (OPT_USE_RTY) A13s2: assume(!o_wb_rty);
        end
        if (OPT_USE_RTY && o_wb_rty) begin
            A14s1: assume(!o_wb_ack);
            if (OPT_USE_ERR) A14s2: assume(!o_wb_err);
        end
        // A15-A17: Optional pulse-only responses
        if (OPT_PULSE_RESP) begin
            if ($past(o_wb_ack)) begin
                A15: assume(!o_wb_ack);
            end
            if (OPT_USE_ERR && $past(o_wb_err)) begin
                A16: assume(!o_wb_err);
            end
            if (OPT_USE_RTY && $past(o_wb_rty)) begin
                A17: assume(!o_wb_rty);
            end
        end
    end
    // -----------------------------
    // Coverage: explore protocol space ("state diagram" witnesses)
    // -----------------------------
    // TODO
 `endif
 endmodule
--- a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v
+++ b/cores/wb/formal_checker/formal/formal_wb_slave_checker.v
@@ -1,222 +1,68 @@
-// formal_wb_slave_checker.v
+`timescale 1ns/1ps
 //
 // Wishbone Classic slave-side protocol checker (plain Verilog).
 // Use when your DUT is a *slave* and the bus/master is the environment.
-module formal_wb_slave_checker #(
+module formal_wb_slave_checker (
-    parameter OPT_USE_ERR              = 0,
+    input wire        i_clk,
-    parameter OPT_USE_RTY              = 0,
+    input wire        i_rst,
-
+    input wire        i_wb_rst,
-    // If 1: require slave to only assert responses when STB=1 (stricter profile).
+    input wire [31:0] i_wb_adr,
-    // If 0: allow "ghost" responses with STB=0; termination still only counts when STB=1.
+    input wire [31:0] i_wb_dat,
-    parameter OPT_STRICT_RESP_WITH_STB = 0,
+    input wire [3:0]  i_wb_sel,
-
+    input wire        i_wb_we,
-    // If 1: require termination signals to be pulses (1 cycle).
+    input wire        i_wb_stb,
-    // If 0: allow them to be held.
+    input wire        i_wb_cyc,
-    parameter OPT_PULSE_RESP           = 1,
+    input wire [31:0] o_wb_rdt,
-
+    input wire        o_wb_ack
    // If 1: after a synchronous reset has been asserted for one clock,
    // require the master to hold CYC/STB low.
    parameter OPT_STRICT_RESET         = 1,
    // If 1: assert read data stable while ACK is held (useful if you allow ACK-hold).
    parameter OPT_ASSERT_RDATA_STABLE_DURING_ACK = 1,
    // Optional widths
    parameter AW = 32,
    parameter DW = 32,
    parameter SW = 4
 ) (
    input  wire              i_clk,
    input  wire              i_rst,
    input  wire              i_wb_rst,
    // Master -> slave
    input  wire              i_wb_cyc,
    input  wire              i_wb_stb,
    input  wire              i_wb_we,
    input  wire [AW-1:0]     i_wb_adr,
    input  wire [DW-1:0]     i_wb_dat,
    input  wire [SW-1:0]     i_wb_sel,
    // Slave -> master
    input  wire              o_wb_ack,
    input  wire              o_wb_err,
    input  wire              o_wb_rty,
    input  wire [DW-1:0]     o_wb_rdt
 );
 `ifdef FORMAL
    // -----------------------------
    // Reset combine
    // -----------------------------
    wire rst_any;
    assign rst_any = i_rst | i_wb_rst;
    // -----------------------------
    // Formal infrastructure
    // -----------------------------
    reg f_past_valid;
    initial f_past_valid = 1'b0;
-    always @(posedge i_clk)
+
    always @(posedge i_clk) begin
        f_past_valid <= 1'b1;
-    wire f_resp_any;
+        // A1: Reset forces cyc=0, stb=0
-    assign f_resp_any = o_wb_ack
+        if (i_rst) begin
-                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
+            assume(!i_wb_cyc);
-                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
+            assume(!i_wb_stb);
    // Real termination only counts when STB=1
    wire f_terminate;
    assign f_terminate = i_wb_cyc && i_wb_stb && f_resp_any;
    // -----------------------------
    // Outstanding request tracking (Classic)
    // -----------------------------
    reg f_pending;
    initial f_pending = 1'b0;
    always @(posedge i_clk or posedge rst_any) begin
        if (rst_any) begin
            f_pending <= 1'b0;
        end else if (!i_wb_cyc) begin
            f_pending <= 1'b0;
        end else begin
            if (!f_pending && i_wb_stb)
                f_pending <= 1'b1;
            if (f_terminate)
                f_pending <= 1'b0;
        end
        // A2: std->cyc, stb never high without cyc
        if(i_wb_stb)
            assume(i_wb_cyc);
        // 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
            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)
            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);
        // 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);
        // R4: once STB has been dropped for a full cycle, ACK must be low
        if(
            f_past_valid &&
            !$past(i_wb_stb) &&
            !i_wb_stb
        )
            assert(!o_wb_ack);
    end
-    // -----------------------------
+    wire unused = &{1'b0, o_wb_rdt};
    // Reset rules (Wishbone synchronous reset semantics)
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid) begin
        if (rst_any) begin
            // R00: Monitor pending state must be cleared during reset
            R00: assert(f_pending == 1'b0);
            if (OPT_STRICT_RESET && $past(rst_any)) begin
                // A00: After reset was asserted on the prior clock, assume master is idle
                A00: assume(!i_wb_cyc);
                // A01: After reset was asserted on the prior clock, assume master is not strobing
                A01: assume(!i_wb_stb);
            end
            if ($past(rst_any)) begin
                // R01: After reset was asserted on the prior clock, slave must not respond
                R01: assert(!o_wb_ack);
                if (OPT_USE_ERR) R02: assert(!o_wb_err);
                if (OPT_USE_RTY) R03: assert(!o_wb_rty);
            end
        end
    end
    // -----------------------------
    // Master/environment assumptions (Classic rules)
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid && !rst_any) begin
        // A10: STB must imply CYC
        if (i_wb_stb) begin
            A10: assume(i_wb_cyc);
        end
        // A11: While pending and not terminated, master holds CYC asserted
        if ($past(f_pending) && !$past(f_terminate)) begin
            A11: assume(i_wb_cyc);
        end
        // A12: While pending and not terminated, master holds STB asserted
        if ($past(f_pending) && !$past(f_terminate)) begin
            A12: assume(i_wb_stb);
        end
        // A13: Address stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            A13: assume(i_wb_adr == $past(i_wb_adr));
        end
        // A14: WE stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            A14: assume(i_wb_we == $past(i_wb_we));
        end
        // A15: SEL stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            A15: assume(i_wb_sel == $past(i_wb_sel));
        end
        // A16: Write data stable while pending and not terminated
        if ($past(f_pending) && !$past(f_terminate)) begin
            A16: assume(i_wb_dat == $past(i_wb_dat));
        end
    end
    // -----------------------------
    // Slave/DUT assertions (response sanity)
    // -----------------------------
    always @(posedge i_clk) if (f_past_valid && !rst_any) begin
        // R10: Any response must occur only during an active cycle
        if (f_resp_any) begin
            R10: assert(i_wb_cyc);
        end
        // R11: Optional strict profile: response only when STB=1
        if (OPT_STRICT_RESP_WITH_STB && f_resp_any) begin
            R11: assert(i_wb_stb);
        end
        // R12-R14: Mutual exclusion of termination signals (recommended)
        if (o_wb_ack) begin
            if (OPT_USE_ERR) R12s1: assert(!o_wb_err);
            if (OPT_USE_RTY) R12s2: assert(!o_wb_rty);
        end
        if (OPT_USE_ERR && o_wb_err) begin
            R13s1: assert(!o_wb_ack);
            if (OPT_USE_RTY) R13s2: assert(!o_wb_rty);
        end
        if (OPT_USE_RTY && o_wb_rty) begin
            R14s1: assert(!o_wb_ack);
            if (OPT_USE_ERR) R14s2: assert(!o_wb_err);
        end
        // R15-R17: Optional pulse-only responses
        if (OPT_PULSE_RESP) begin
            if ($past(o_wb_ack)) begin
                R15: assert(!o_wb_ack);
            end
            if (OPT_USE_ERR && $past(o_wb_err)) begin
                R16: assert(!o_wb_err);
            end
            if (OPT_USE_RTY && $past(o_wb_rty)) begin
                R17: assert(!o_wb_rty);
            end
        end
        // R18: A real termination (STB && response) should only happen when a request is pending.
        if (i_wb_stb && f_resp_any) begin
            R18: assert(f_pending || $past(f_pending));
        end
        // R19: Optional read-data stability while ACK is held (only relevant if ACK can be held)
        if (OPT_ASSERT_RDATA_STABLE_DURING_ACK) begin
            if (o_wb_ack && !i_wb_we && $past(o_wb_ack)) begin
                R19: assert(o_wb_rdt == $past(o_wb_rdt));
            end
        end
        // R20: If no cycle, no responses (strong sanity rule)
        if (!i_wb_cyc) begin
            R20: assert(!f_resp_any);
        end
    end
    // -----------------------------
    // Coverage: exercise the slave (useful witness traces)
    // -----------------------------
    // TODO
 `endif
 endmodule
--- a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby
+++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby
@@ -1,19 +1,9 @@
 [tasks]
 prove
 cover
 bmc
 [options]
-bmc: mode bmc
+mode prove
-bmc: depth 16
+depth 8
 cover: mode cover
 cover: depth 16
 prove: mode prove
 [engines]
-bmc: smtbmc yices
+abc pdr
 cover: smtbmc yices
 prove: abc pdr
 [script]
 {{"-formal"|gen_reads}}
--- a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt
+++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt
@@ -1,2 +0,0 @@
 SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Removing directory '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove'.
 SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Copy '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/{{files}}' to '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/src/{{files}}'.
--- a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path
+++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path
@@ -1 +0,0 @@
 ../jtag_wb_bridge/status.sqlite
--- a/cores/wb/wb_gpio/formal/formal_wb_gpio.v
+++ b/cores/wb/wb_gpio/formal/formal_wb_gpio.v
@@ -1,29 +1,35 @@
 `timescale 1ns/1ps
-module formal_wb_gpio;
+module formal_wb_gpio #(
    parameter [31:0] address = 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      i_wb_cyc;
    (* anyseq *) reg [31:0] i_gpio;
    wire [31:0] o_wb_rdt;
    wire        o_wb_ack;
    wire [31:0] o_gpio;
    wire        i_wb_cyc;
    reg         f_past_valid;
-    wb_gpio dut (
+    assign i_wb_cyc = i_wb_stb || o_wb_ack;
-        .i_clk(i_wb_clk),
+
-        .i_rst(i_wb_rst),
+    wb_gpio #(
        .address(address)
    ) 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_wb_cyc(i_wb_cyc),
        .i_gpio(i_gpio),
        .o_wb_rdt(o_wb_rdt),
        .o_wb_ack(o_wb_ack),
@@ -32,7 +38,7 @@ module formal_wb_gpio;
    formal_wb_slave_checker wb_checker (
        .i_clk(i_wb_clk),
-        .i_rst(i_wb_rst),
+        .i_rst(i_rst),
        .i_wb_rst(i_wb_rst),
        .i_wb_adr(i_wb_adr),
        .i_wb_dat(i_wb_dat),
@@ -50,13 +56,9 @@ module formal_wb_gpio;
        f_past_valid <= 1'b1;
        // R1: reads return the sampled GPIO input on the following cycle
-        if(f_past_valid && 
+        if (f_past_valid && !$past(i_wb_rst) && !i_wb_rst && $past(i_wb_stb) && !$past(i_wb_we)) begin
                !i_wb_rst && $past(!i_wb_rst) && 
                o_wb_ack && 
                $past(i_wb_sel)==4'hf && i_wb_sel==4'hf &&
                $past(i_wb_cyc & i_wb_stb & !i_wb_we) &&
                (i_wb_cyc & i_wb_stb & !i_wb_we))
            assert(o_wb_rdt == $past(i_gpio));
        end
        // R2: reset clears the output register and read data register
        if (f_past_valid && $past(i_wb_rst)) begin
--- a/cores/wb/wb_gpio/formal/wb_gpio.sby
+++ b/cores/wb/wb_gpio/formal/wb_gpio.sby
@@ -1,23 +1,13 @@
 [tasks]
 prove
 cover
 bmc
 [options]
-bmc: mode bmc
+mode prove
-bmc: depth 50
+depth 8
 cover: mode cover
 cover: depth 50
 prove: mode prove
 [engines]
-bmc: smtbmc yices
+smtbmc z3 parallel.enable=true parallel.threads.max=8
 cover: smtbmc yices
 prove: abc pdr
 [script]
 {{"-formal"|gen_reads}}
 prep -top {{top_level}}
 [files]
-{{files}}
+{{files}}
--- a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby
+++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby
@@ -1,13 +1,13 @@
 [options]
 mode prove
 depth 8
 [engines]
-abc pdr
+smtbmc z3 parallel.enable=true parallel.threads.max=8
 [script]
 {{"-formal"|gen_reads}}
 prep -top {{top_level}}
 clk2fflogic
 [files]
 {{files}}
--- a/cores/wb/wb_gpio/formal/wb_gpio/logfile.txt
+++ b/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}}'.
--- a/cores/wb/wb_gpio/rtl/wb_gpio.v
+++ b/cores/wb/wb_gpio/rtl/wb_gpio.v
@@ -1,53 +1,56 @@
-module wb_gpio (
+module wb_gpio #(
-    input  wire         i_clk,
+  parameter address = 32'h00000000
-    input  wire         i_rst,
+)(
  input  wire        i_wb_clk,
  input  wire        i_wb_rst,   // optional; tie low if unused
  input  wire [31:0] i_wb_adr,   // optional; can ignore for single-reg
  input  wire [31:0] i_wb_dat,
  input  wire [3:0]  i_wb_sel,
  input  wire        i_wb_we,
  input  wire        i_wb_stb,
  input  wire [31:0] i_gpio,
-    input  wire [31:0]  i_wb_adr,
+  output reg  [31:0] o_wb_rdt,
-    input  wire [31:0]  i_wb_dat,
+  output reg         o_wb_ack,
-    output reg  [31:0]  o_wb_rdt,
+  output reg  [31:0] o_gpio
    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,
 	input  wire	[31:0]	i_gpio,
 	output wire	[31:0]	o_gpio
 );
 	// Registers
 	reg [31:0] gpo;
 	wire [31:0] gpi;
 	assign o_gpio = gpo;
 	assign gpi = i_gpio;
-	reg wb_ack = 0;
+  initial o_gpio <= 32'h00000000;
-	assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb;
+  initial o_wb_rdt <= 32'h00000000;
-	always @(posedge i_clk) begin
+  wire addr_check;
-		if(i_rst) begin
+  assign addr_check = (i_wb_adr == address);
 			gpo <= 0;
 			wb_ack <= 0;
 			o_wb_rdt <= 0;
 		end else begin
 			// Ack generation
            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
-            // Read cycle
+  // One-cycle ACK pulse per request (works even if stb stays high)
-            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
+  initial o_wb_ack <= 1'b0;
-				if(i_wb_sel[0]) o_wb_rdt[7:0] <= gpi[7:0];
+  always @(posedge i_wb_clk) begin
-				if(i_wb_sel[1]) o_wb_rdt[15:8] <= gpi[15:8];
+    if (i_wb_rst) begin
-				if(i_wb_sel[2]) o_wb_rdt[23:16] <= gpi[23:16];
+      o_wb_ack <= 1'b0;
-				if(i_wb_sel[3]) o_wb_rdt[31:24] <= gpi[31:24];
+    end else begin
-            end
+      o_wb_ack <= i_wb_stb & ~o_wb_ack; // pulse while stb asserted
-            // write cycle
+    end
-            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
+  end
-				if(i_wb_sel[0]) gpo[7:0] <= i_wb_dat[7:0];
+
-				if(i_wb_sel[1]) gpo[15:8] <= i_wb_dat[15:8];
+  // Read data (combinational or registered; registered here)
-				if(i_wb_sel[2]) gpo[23:16] <= i_wb_dat[23:16];
+  always @(posedge i_wb_clk) begin
-				if(i_wb_sel[3]) gpo[31:24] <= i_wb_dat[31:24];
+    if (i_wb_rst) begin
-			end
+      o_wb_rdt <= 32'h0;
-		end
+    end else if (i_wb_stb && !i_wb_we) begin
-	end
+      o_wb_rdt <= i_gpio;
    end
  end
  // Write latch (update on the acknowledged cycle)
  always @(posedge i_wb_clk) begin
    if (i_wb_rst) begin
      o_gpio <= 32'h0;
    end else if (i_wb_stb && i_wb_we && addr_check && (i_wb_stb & ~o_wb_ack)) begin
      // Apply byte enables (so sb works if the master uses sel)
      if (i_wb_sel[0]) o_gpio[7:0]   <= i_wb_dat[7:0];
      if (i_wb_sel[1]) o_gpio[15:8]  <= i_wb_dat[15:8];
      if (i_wb_sel[2]) o_gpio[23:16] <= i_wb_dat[23:16];
      if (i_wb_sel[3]) o_gpio[31:24] <= i_wb_dat[31:24];
    end
  end
 endmodule
--- a/cores/wb/wb_gpio/wb_gpio.core
+++ b/cores/wb/wb_gpio/wb_gpio.core
@@ -25,6 +25,8 @@ targets:
        filesets:
            - rtl
        toplevel: wb_gpio
        parameters:
            - address
    formal:
        default_tool: symbiyosys
@@ -33,3 +35,11 @@ targets:
            - formal_rtl
            - formal_cfg
        toplevel: formal_wb_gpio
        parameters:
            - address
 parameters:
    address:
        datatype: int
        description: Wishbone address matched by this peripheral
        paramtype: vlogparam
--- a/cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v
+++ b/cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v
@@ -1,50 +0,0 @@
 `timescale 1ns/1ps
 module formal_wb_gpio_banks #(
    parameter integer num_banks = 2,
 );
    (* 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_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)
    ) dut (
        .i_clk(i_clk),
        .i_rst(i_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_clk),
        .i_rst(i_rst),
        .i_wb_rst(i_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
--- a/cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby
+++ b/cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby
@@ -1,25 +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]
 read -formal clog2.vh
 {{"-formal"|gen_reads}}
 prep -top {{top_level}}
 [files]
 src/joppeb_util_clog2_1.0/clog2.vh
 {{files}}
--- a/cores/wb/wb_gpio_banks/rtl/wb_gpio_banks.v
+++ b/cores/wb/wb_gpio_banks/rtl/wb_gpio_banks.v
@@ -1,61 +1,63 @@
-`include "clog2.vh"
+`default_nettype none
 module wb_gpio_banks #(
-	parameter  num_banks = 4
+  parameter integer NUM_BANKS = 4,
-)(
+  parameter [31:0] BASE_ADDR = 32'h8000_0000
-    input  wire         i_clk,
+) (
-    input  wire         i_rst,
+  input  wire                     i_wb_clk,
-
+  input  wire                     i_wb_rst,
-    input  wire [31:0]  i_wb_adr,
+  input  wire [31:0]              i_wb_adr,
-    input  wire [31:0]  i_wb_dat,
+  input  wire [31:0]              i_wb_dat,
-    output reg  [31:0]  o_wb_rdt,
+  input  wire [3:0]               i_wb_sel,
-    input  wire [3:0]   i_wb_sel,
+  input  wire                     i_wb_we,
-    input  wire         i_wb_we,
+  input  wire                     i_wb_stb,
-    input  wire         i_wb_cyc,
+  input  wire [NUM_BANKS*32-1:0]  i_gpio,
-    input  wire         i_wb_stb,
+  output reg  [31:0]              o_wb_rdt,
-    output reg          o_wb_ack,
+  output reg                      o_wb_ack,
-
+  output wire [NUM_BANKS*32-1:0]  o_gpio
 	input wire [num_banks*32-1:0] i_gpio,
 	output wire [num_banks*32-1:0] o_gpio
 );
 	localparam sw = `CLOG2(num_banks);
 	wire [num_banks-1:0] bank_sel;
-	wire [num_banks-1:0] bank_ack;
+  wire [NUM_BANKS-1:0]           bank_sel;
-	wire [num_banks*32-1:0] bank_rdt;
+  wire [NUM_BANKS-1:0]           bank_stb;
  wire [NUM_BANKS*32-1:0]        bank_rdt;
  wire [NUM_BANKS-1:0]           bank_ack;
-	genvar gi;
+  genvar gi;
-	generate
+  generate
-		for(gi=0; gi<num_banks; gi=gi+1) begin : gen_gpio
+    for (gi = 0; gi < NUM_BANKS; gi = gi + 1) begin : gen_gpio
-			localparam [2+sw-1:0] addr = gi*4;
+      localparam [31:0] BANK_ADDR = BASE_ADDR + (gi * 4);
 			assign bank_sel[gi] = (i_wb_adr[2+sw-1:0] == addr);
 			wb_gpio u_gpio(
 				.i_clk(i_clk),
 				.i_rst(i_rst),
 				.i_wb_adr(i_wb_adr),
 				.i_wb_dat(i_wb_dat),
 				.i_wb_cyc(i_wb_cyc & bank_sel[gi]),
 				.i_wb_stb(i_wb_stb & bank_sel[gi]),
 				.i_wb_we(i_wb_we),
 				.i_wb_sel(i_wb_sel),
 				.o_wb_ack(bank_ack[gi]),
 				.o_wb_rdt(bank_rdt[gi*32 +: 32]),
 				.i_gpio(i_gpio[gi*32 +: 32]),
 				.o_gpio(o_gpio[gi*32 +: 32])
 			);
 		end
 	endgenerate
-	integer bi;
+      assign bank_sel[gi] = (i_wb_adr == BANK_ADDR);
-	always @* begin
+      assign bank_stb[gi] = i_wb_stb & bank_sel[gi];
-		o_wb_rdt = 32'h00000000;
+
-		o_wb_ack = 1'b0;
+      wb_gpio #(
-		for(bi=0; bi<num_banks; bi=bi+1) begin
+        .address(BANK_ADDR)
-			if(bank_sel[bi]) begin
+      ) u_gpio (
-				o_wb_rdt = bank_rdt[bi*32 +: 32];
+        .i_wb_clk(i_wb_clk),
-				o_wb_ack = bank_ack[bi];
+        .i_wb_rst(i_wb_rst),
-			end
+        .i_wb_adr(i_wb_adr),
-		end
+        .i_wb_dat(i_wb_dat),
-	end;
+        .i_wb_sel(i_wb_sel),
        .i_wb_we(i_wb_we),
        .i_wb_stb(bank_stb[gi]),
        .i_gpio(i_gpio[gi*32 +: 32]),
        .o_wb_rdt(bank_rdt[gi*32 +: 32]),
        .o_wb_ack(bank_ack[gi]),
        .o_gpio(o_gpio[gi*32 +: 32])
      );
    end
  endgenerate
  integer bi;
  always @* begin
    o_wb_rdt = 32'h0000_0000;
    o_wb_ack = 1'b0;
    for (bi = 0; bi < NUM_BANKS; bi = bi + 1) begin
      if (bank_sel[bi]) begin
        o_wb_rdt = bank_rdt[bi*32 +: 32];
        o_wb_ack = bank_ack[bi];
      end
    end
  end
 endmodule
--- a/cores/wb/wb_gpio_banks/wb_gpio_banks.core
+++ b/cores/wb/wb_gpio_banks/wb_gpio_banks.core
@@ -7,20 +7,9 @@ filesets:
    rtl:
        depend:
            - joppeb:wb:wb_gpio
            - joppeb:util:clog2
        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:
@@ -30,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:
--- a/cores/wb/wb_mem32/formal/wb_mem32.sby
+++ b/cores/wb/wb_mem32/formal/wb_mem32.sby
@@ -1,19 +1,9 @@
 [tasks]
 prove
 cover
 bmc
 [options]
-bmc: mode bmc
+mode prove
-bmc: depth 50
+depth 8
 cover: mode cover
 cover: depth 50
 prove: mode prove
 [engines]
-bmc: smtbmc yices
+smtbmc z3 parallel.enable=true parallel.threads.max=8
 cover: smtbmc yices
 prove: abc pdr
 [script]
 read -formal clog2.vh
@@ -22,4 +12,4 @@ prep -top {{top_level}}
 [files]
 src/joppeb_util_clog2_1.0/clog2.vh
-{{files}}
+{{files}}
--- a/cores/wb/wb_mem32/rtl/wb_mem32.v
+++ b/cores/wb/wb_mem32/rtl/wb_mem32.v
@@ -27,7 +27,7 @@ module wb_mem32 #(
    wire [mem_aw-1:0] wb_word_adr = i_wb_adr[mem_aw+1:2];
    assign o_wb_rdt = wb_rdt_r;
-    assign o_wb_ack = wb_ack_r & i_wb_cyc & i_wb_stb;
+    assign o_wb_ack = wb_ack_r;
    always @(posedge i_clk) begin
        if (i_rst || i_wb_rst) begin
--- a/cores/wb/wb_timer/formal/formal_wb_timer.v
+++ b/cores/wb/wb_timer/formal/formal_wb_timer.v
@@ -1,60 +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 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
--- a/cores/wb/wb_timer/formal/wb_timer.sby
+++ b/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}}
--- a/cores/wb/wb_timer/rtl/wb_timer.v
+++ b/cores/wb/wb_timer/rtl/wb_timer.v
@@ -1,185 +1,74 @@
 `timescale 1ns/1ps
-module wb_countdown_timer (
+module wb_countdown_timer #(
    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
+    // One-cycle acknowledge on any valid WB access
-    reg [31:0]       counter; // The actual counter. Generates an interrupt when it reaches 0
+    // (classic, zero-wait-state peripheral)
-    reg [31:0]       preload; // The value with which the counter gets loaded after it reaches 0. 0 to keep the timer off
+    assign o_wb_ack = i_wb_cyc & i_wb_stb;
-    reg wb_ack = 0;
+    // Internal countdown and prescaler
-    reg irq_fired = 0;
+    reg [WIDTH-1:0] counter;
-    reg counter_started = 0;
+    reg [DIVIDER:0] presc;   // enough bits to count up to 2^DIVIDER-1
-    reg counter_running = 0;
+    wire tick = (DIVIDER == 0) ? 1'b1 : (presc[DIVIDER] == 1'b1);
    reg prev_counter_running = 0;
    assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb; // Make sure the ack only happend during a cycle
-    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
+        if (i_rst) begin
-            counter <= 0;
+            counter <= {WIDTH{1'b0}};
-            preload <= 0;
+            presc   <= { (DIVIDER+1){1'b0} };
-            wb_ack <= 0;
+            o_irq   <= 1'b0;
            o_wb_dat <= 0;
            irq_fired <= 0;
            counter_started <= 0;
            counter_running <= 0;
            prev_counter_running <= 0;
        end else begin
-
+            // Default prescaler behavior
-            prev_counter_running <= counter_running;
+            if (DIVIDER != 0) begin
-            counter_running <= counter>0;
+                if (counter != 0 && !o_irq)
-
+                    presc <= presc + 1'b1;
-            if(!irq_fired && prev_counter_running && !counter_running)
+                else
-                irq_fired <= 1'b1;
+                    presc <= { (DIVIDER+1){1'b0} };
            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
-            // write cycle
+            // Wishbone write: load counter and clear IRQ
-            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
+            if (o_wb_ack && i_wb_we) begin
-                if(i_wb_adr[3:0] == 4'b0000) begin
+                counter <= i_wb_dat[WIDTH-1:0];
-                    if(i_wb_sel[0]) counter[7:0] <= i_wb_dat[7:0];
+                o_irq   <= 1'b0;
-                    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];
+                // reset prescaler on (re)start or stop
-                    if(i_wb_sel[3]) counter[31:24] <= i_wb_dat[31:24];
+                presc   <= { (DIVIDER+1){1'b0} };
-                    counter_started <= 1'b1;
+
-                end else if(i_wb_adr[3:0] == 4'b0100) begin
+            end else begin
-                    if(i_wb_sel[0]) preload[7:0] <= i_wb_dat[7:0];
+                // Countdown when running (counter>0), not already IRQ'd
-                    if(i_wb_sel[1]) preload[15:8] <= i_wb_dat[15:8];
+                if (!o_irq && counter != 0) begin
-                    if(i_wb_sel[2]) preload[23:16] <= i_wb_dat[23:16];
+                    if (tick) begin
-                    if(i_wb_sel[3]) preload[31:24] <= i_wb_dat[31:24];
+                        if (counter == 1) begin
-                    counter_started <= 1'b1;
+                            counter <= {WIDTH{1'b0}};
-                end else if(i_wb_adr[3:0] == 4'b1000) begin
+                            o_irq   <= 1'b1; // sticky until next write
-                    // Any write to BASE+8 will ack the IRQ
+                            presc   <= { (DIVIDER+1){1'b0} };
-                    irq_fired <= 1'b0;
+                        end else begin
                            counter <= counter - 1'b1;
                        end
                    end
                end
            end
        end
    end
-`ifdef FORMAL
+endmodule
    // 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
--- a/cores/wb/wb_timer/tb/tb_wb_timer.v
+++ b/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
--- a/cores/wb/wb_timer/wb_timer.core
+++ b/cores/wb/wb_timer/wb_timer.core
@@ -8,44 +8,22 @@ 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:
        filesets:
            - rtl
        toplevel: wb_countdown_timer
    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:
-            - FORMAL=true
+            - WIDTH
            - DIVIDER
 parameters:
-    FORMAL:
+    WIDTH:
-        datatype: bool
+        datatype: int
-        description: Enable in-module formal-only logic
+        description: Counter width in bits
-        paramtype: vlogdefine
+        paramtype: vlogparam
    DIVIDER:
        datatype: int
        description: Prescaler divider as a power of two exponent
        paramtype: vlogparam
--- a/fusesoc_libraries/serv
+++ b/fusesoc_libraries/serv
--- a/modem/modem_dtmf.py
+++ b/modem/modem_dtmf.py
@@ -1,79 +0,0 @@
 #!/usr/bin/env python3
 import argparse
 import sys
 import time
 import serial
 def read_response(port: serial.Serial, timeout_s: float) -> list[str]:
    deadline = time.monotonic() + timeout_s
    lines: list[str] = []
    while time.monotonic() < deadline:
        raw = port.readline()
        if not raw:
            continue
        line = raw.decode(errors="replace").strip()
        if not line:
            continue
        lines.append(line)
        if line in {"OK", "ERROR"}:
            break
    return lines
 def send_at(port: serial.Serial, command: str, timeout_s: float) -> tuple[bool, list[str]]:
    port.write((command + "\r").encode())
    port.flush()
    lines = read_response(port, timeout_s)
    ok = any(line == "OK" for line in lines)
    err = any(line == "ERROR" for line in lines)
    return ok and not err, lines
 def send_and_log(port: serial.Serial, command: str, timeout_s: float) -> tuple[bool, list[str]]:
    ok, lines = send_at(port, command, timeout_s)
    print(f"> {command}")
    for line in lines:
        print(f"< {line}")
    return ok, lines
 def main() -> int:
    parser = argparse.ArgumentParser(description="Control an AT modem and send DTMF tones")
    parser.add_argument("device", help="Serial device path, e.g. /dev/ttyACM0")
    parser.add_argument("--baud", type=int, default=115200, help="Serial baudrate (default: 115200)")
    parser.add_argument("--timeout", type=float, default=2.0, help="AT command timeout seconds")
    args = parser.parse_args()
    try:
        with serial.Serial(args.device, args.baud, timeout=0.2, write_timeout=1.0) as port:
            port.reset_input_buffer()
            port.reset_output_buffer()
            # Inicialise
            for cmd in ("AT", "ATZ0", "ATE1", "ATX0"):
                ok, lines = send_and_log(port, cmd, args.timeout)
                if not ok:
                    print(f"Modem did not accept {cmd}", file=sys.stderr)
                    return 1
            send_and_log(port, "ATS6=0", args.timeout) # Set wait for dial tone time to 0
            send_and_log(port, "ATS11=2", args.timeout) # set tone length to 1 ms
            send_and_log(port, "ATH1", args.timeout)
            while True:
                send_and_log(port, "ATDT0123456789;", args.timeout)
            send_and_log(port, "ATH0", args.timeout)
    except serial.SerialException as exc:
        print(f"Serial error: {exc}", file=sys.stderr)
        return 1
    print("Done")
    return 0
 if __name__ == "__main__":
    raise SystemExit(main())
--- a/xilinx_fusesoc.sh
+++ b/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 "$@"
		`@@ -1,2 +0,0 @@`
			`project set "Create Binary Configuration File" TRUE -process "Generate Programming File"`
			`project set "Keep Hierarchy" Yes -process "Synthesize - XST"`
		`@@ -1,2 +0,0 @@`
			`SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Removing directory '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove'.`
			`SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Copy '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/{{files}}' to '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/src/{{files}}'.`
		`@@ -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}}'.`