Added missing signal modules

.gitignore

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

.gitmodules

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

check_formal.sh

@@ -0,0 +1,95 @@
+#!/bin/sh
+
+# Add or remove cores here. Each entry should be a full FuseSoC VLNV.
+CORES="
+joppeb:wb:wb_mem32
+joppeb:wb:wb_gpio
+joppeb:wb:wb_gpio_banks
+joppeb:wb:jtag_wb_bridge
+joppeb:wb:wb_timer
+"
+
+if [ -n "$1" ]; then
+	CORES="$1"
+fi
+
+# Add or remove formal tasks here.
+TASKS="
+bmc
+cover
+prove
+"
+
+total=0
+passed=0
+failed=0
+passed_runs=""
+failed_runs=""
+
+run_task() {
+	core="$1"
+	task="$2"
+	label="$core [$task]"
+	log_file=""
+	total=$((total + 1))
+
+	printf '\n[%d] Running formal %s for %s\n' "$total" "$task" "$core"
+
+	log_file=$(mktemp /tmp/check_formal.XXXXXX) || exit 2
+
+	if \
+		FUSESOC_CORE="$core" \
+		FUSESOC_TASK="$task" \
+		script -qefc 'fusesoc run --target formal "$FUSESOC_CORE" --taskname "$FUSESOC_TASK"' "$log_file" \
+			>/dev/null 2>&1
+	then
+		passed=$((passed + 1))
+		passed_runs="$passed_runs
+$label"
+		printf 'Result: PASS (%s)\n' "$label"
+		rm -f "$log_file"
+		return 0
+	else
+		failed=$((failed + 1))
+		failed_runs="$failed_runs
+$label"
+		printf 'Result: FAIL (%s)\n' "$label"
+		printf 'Captured log for %s:\n' "$label"
+		cat "$log_file" #| grep summary
+		rm -f "$log_file"
+		return 1
+	fi
+}
+
+for core in $CORES; do
+	for task in $TASKS; do
+		run_task "$core" "$task"
+	done
+done
+
+printf '\nFormal run summary\n'
+printf '  Total:   %d\n' "$total"
+printf '  Passed:  %d\n' "$passed"
+printf '  Failed:  %d\n' "$failed"
+
+if [ -n "$passed_runs" ]; then
+	printf '\nPassed runs:\n'
+	printf '%s\n' "$passed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ -n "$failed_runs" ]; then
+	printf '\nFailed runs:\n'
+	printf '%s\n' "$failed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ "$failed" -ne 0 ]; then
+	exit 1
+fi

cores/primitive/lvds_comparator/lvds_comparator.core

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

cores/primitive/lvds_comparator/lvds_comparator.v

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

cores/primitive/lvds_comparator/lvds_comparator_generic_impl.v

@@ -0,0 +1,7 @@
+module lvds_comparator_generic_impl (
+    input wire a,
+    input wire b,
+    output wire o
+);
+    assign o = a;
+endmodule

cores/primitive/lvds_comparator/lvds_comparator_spartan6.v

@@ -0,0 +1,14 @@
+module lvds_comparator_spartan6_impl (
+    input wire a,
+    input wire b,
+    output wire o
+);
+    IBUFDS #(
+        .DIFF_TERM("FALSE"),
+        .IOSTANDARD("LVDS33")
+    ) lvds_buf (
+        .O(o),
+        .I(a),
+        .IB(b)
+    );
+endmodule

cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.core

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

cores/signal/decimate_by_r_q15.v/decimate_by_r_q15.v

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

cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.core

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

cores/signal/lpf_iir_q15_k/lpf_iir_q15_k.v

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

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:
-//      -- clk : input clock
+//      -- i_clk : input clock
-//      -- rst_n : reset
+//      -- i_rst_n : reset
-//      -- freq_hz : decimal number of desired generated frequency in Hz, 0-FS/2
+//      -- i_freq_hz : decimal number of desired generated frequency in Hz, 0-FS/2
-//      -- sin_q15/cos_q15 : I and Q outputs
+//      -- o_sin_q15/o_cos_q15 : I and Q outputs
-//      -- clk_en : output valid strobe
+//      -- o_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 clk,                                 // CLK_HZ domain
+    input wire i_clk,                               // CLK_HZ domain
-    input wire rst_n,                               // async active-low reset
+    input wire i_rst_n,                             // async active-low reset
-    input wire [31:0] freq_hz,                      // desired output frequency (Hz), 0..FS_HZ/2
+    input wire [31:0] i_freq_hz,                    // desired output frequency (Hz), 0..FS_HZ/2
 
-    output reg signed [15:0] sin_q15,               // Q1.15 sine
+    output reg signed [15:0] o_sin_q15,             // Q1.15 sine
-    output reg signed [15:0] cos_q15,               // Q1.15 cosine
+    output reg signed [15:0] o_cos_q15,             // Q1.15 cosine
-    output reg clk_en                               // 1-cycle strobe @ FS_HZ
+    output reg o_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 clk or negedge rst_n) begin
+    always @(posedge i_clk or negedge i_rst_n) begin
-        if (!rst_n) begin tick_cnt <= 0; clk_en <= 1'b0; end
+        if (!i_rst_n) begin tick_cnt <= 0; o_clk_en <= 1'b0; end
         else begin
-        clk_en <= 1'b0;
+        o_clk_en <= 1'b0;
-        if (tick_cnt == DIV-1) begin tick_cnt <= 0; clk_en <= 1'b1; end
+        if (tick_cnt == DIV-1) begin tick_cnt <= 0; o_clk_en <= 1'b1; end
         else tick_cnt <= tick_cnt + 1'b1;
         end
     end
 
-    // 32-cycle shift-add multiply: prod = freq_hz * RECIP  (no multiplications themself)
+    // 32-cycle shift-add multiply: prod = i_freq_hz * RECIP  (no multiplications themself)
-	// Starts at clk_en, finishes in 32 cycles (<< available cycles per sample).
+	// Starts at o_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 clk or negedge rst_n) begin
+    always @(posedge i_clk or negedge i_rst_n) begin
-        if (!rst_n) begin
+        if (!i_rst_n) begin
         mul_busy <= 1'b0; mul_i <= 6'd0; f_reg <= 32'd0; acc <= 96'd0;
         end else begin
-        if (clk_en && !mul_busy) begin
+        if (o_clk_en && !mul_busy) begin
             // kick off a new multiply this sample
             mul_busy <= 1'b1;
             mul_i    <= 6'd0;
-            f_reg    <= (freq_hz > (FS_HZ>>1)) ? (FS_HZ>>1) : freq_hz; // clamp to Nyquist
+            f_reg    <= (i_freq_hz > (FS_HZ>>1)) ? (FS_HZ>>1) : i_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 clk or negedge rst_n) begin
+    always @(posedge i_clk or negedge i_rst_n) begin
-        if (!rst_n) ftw_q <= {PHASE_BITS{1'b0}};
+        if (!i_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 clk or negedge rst_n) begin
+    always @(posedge i_clk or negedge i_rst_n) begin
-        if (!rst_n)      phase <= {PHASE_BITS{1'b0}};
+        if (!i_rst_n)        phase <= {PHASE_BITS{1'b0}};
-        else if (clk_en) phase <= phase + ftw_q;
+        else if (o_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 (.addr(idx_sin), .dout(mag_sin_u8));
+    sine_qtr_lut64 u_lut_s (.i_addr(idx_sin), .o_dout(mag_sin_u8));
-    sine_qtr_lut64 u_lut_c (.addr(idx_cos), .dout(mag_cos_u8));
+    sine_qtr_lut64 u_lut_c (.i_addr(idx_cos), .o_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 clk or negedge rst_n) begin
+    always @(posedge i_clk or negedge i_rst_n) begin
-        if (!rst_n) begin
+        if (!i_rst_n) begin
-        sin_q15 <= 16'sd0; cos_q15 <= 16'sd0;
+        o_sin_q15 <= 16'sd0; o_cos_q15 <= 16'sd0;
-        end else if (clk_en) begin
+        end else if (o_clk_en) begin
-        sin_q15 <= sin_next; cos_q15 <= cos_next;
+        o_sin_q15 <= sin_next; o_cos_q15 <= cos_next;
         end
     end
 
 endmodule
 	
 module sine_qtr_lut64(
-    input wire [5:0] addr,
+    input wire [5:0] i_addr,
-    output reg [7:0] dout
+    output reg [7:0] o_dout
 );
     always @* begin
-        case (addr)
+        case (i_addr)
-            6'd0: dout = 8'd0;    6'd1: dout = 8'd6;    6'd2: dout = 8'd13;   6'd3: dout = 8'd19;
+            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'd4: dout = 8'd25;   6'd5: dout = 8'd31;   6'd6: dout = 8'd37;   6'd7: dout = 8'd44;
+            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'd8: dout = 8'd50;   6'd9: dout = 8'd56;   6'd10: dout = 8'd62;  6'd11: dout = 8'd68;
+            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'd12: dout = 8'd74;  6'd13: dout = 8'd80;  6'd14: dout = 8'd86;  6'd15: dout = 8'd92;
+            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'd16: dout = 8'd98;  6'd17: dout = 8'd103; 6'd18: dout = 8'd109; 6'd19: dout = 8'd115;
+            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'd20: dout = 8'd120; 6'd21: dout = 8'd126; 6'd22: dout = 8'd131; 6'd23: dout = 8'd136;
+            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'd24: dout = 8'd142; 6'd25: dout = 8'd147; 6'd26: dout = 8'd152; 6'd27: dout = 8'd157;
+            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'd28: dout = 8'd162; 6'd29: dout = 8'd167; 6'd30: dout = 8'd171; 6'd31: dout = 8'd176;
+            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'd32: dout = 8'd180; 6'd33: dout = 8'd185; 6'd34: dout = 8'd189; 6'd35: dout = 8'd193;
+            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'd36: dout = 8'd197; 6'd37: dout = 8'd201; 6'd38: dout = 8'd205; 6'd39: dout = 8'd208;
+            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'd40: dout = 8'd212; 6'd41: dout = 8'd215; 6'd42: dout = 8'd219; 6'd43: dout = 8'd222;
+            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'd44: dout = 8'd225; 6'd45: dout = 8'd228; 6'd46: dout = 8'd231; 6'd47: dout = 8'd233;
+            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'd48: dout = 8'd236; 6'd49: dout = 8'd238; 6'd50: dout = 8'd240; 6'd51: dout = 8'd242;
+            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'd52: dout = 8'd244; 6'd53: dout = 8'd246; 6'd54: dout = 8'd247; 6'd55: dout = 8'd249;
+            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'd56: dout = 8'd250; 6'd57: dout = 8'd251; 6'd58: dout = 8'd252; 6'd59: dout = 8'd253;
+            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'd60: dout = 8'd254; 6'd61: dout = 8'd254; 6'd62: dout = 8'd255; 6'd63: dout = 8'd255;
+            6'd60: o_dout = 8'd254; 6'd61: o_dout = 8'd254; 6'd62: o_dout = 8'd255; 6'd63: o_dout = 8'd255;
-            default: dout=8'd0;
+            default: o_dout=8'd0;
         endcase
     end
 endmodule

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 (
-        .clk    (clk),
+        .i_clk    (clk),
-        .rst_n  (resetn),
+        .i_rst_n  (resetn),
-        .freq_hz(freq),
+        .i_freq_hz(freq),
-        .sin_q15(sin_q15),
+        .o_sin_q15(sin_q15),
-        .cos_q15(cos_q15),
+        .o_cos_q15(cos_q15),
-        .clk_en (out_en)
+        .o_clk_en (out_en)
     );
 
     initial begin

cores/signal/sd_adc_q15/rtl/rc_alpha_q15.vh

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

cores/signal/sd_adc_q15/rtl/rcmodel_q15.v

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

cores/signal/sd_adc_q15/rtl/sd_adc_q15.v

@@ -0,0 +1,57 @@
+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(10)
+    ) 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(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

cores/signal/sd_adc_q15/rtl/sd_sampler.v

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

cores/signal/sd_adc_q15/sd_adc_q15.core

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

cores/signal/sd_adc_q15/sim/sd_sampler.v

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

cores/signal/sd_adc_q15/tb/tb_sd_adc_q15.v

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

cores/system/mcu/mcu.core

@@ -0,0 +1,48 @@
+CAPI=2:
+
+name: joppeb:system:mcu:1.0
+description: basic RISC-V MCU system
+
+filesets:
+    rtl:
+        depend:
+            - "^award-winning:serv:servile:1.4.0"
+            - joppeb:util:clog2
+            - joppeb:wb:jtag_wb_bridge
+            - joppeb:wb:wb_gpio_banks
+            - joppeb:wb:wb_timer
+            - joppeb:wb:wb_arbiter
+            - joppeb:wb:wb_mux
+        files:
+            - rtl/mcu.v
+            - rtl/mcu_peripherals.v
+        file_type: verilogSource
+
+targets:
+    default:
+        filesets:
+            - rtl
+        toplevel: mcu
+        parameters:
+            - memfile
+            - memsize
+            - sim
+            - jtag
+
+parameters:
+    memfile:
+        datatype: str
+        description: Memory initialization file passed to the internal RAM
+        paramtype: vlogparam
+    memsize:
+        datatype: int
+        description: Internal RAM size in bytes
+        paramtype: vlogparam
+    sim:
+        datatype: int
+        description: Enable simulation-friendly RAM initialization behavior
+        paramtype: vlogparam
+    jtag:
+        datatype: int
+        description: Enable the JTAG Wishbone bridge and arbiter path
+        paramtype: vlogparam

cores/system/mcu/rtl/mcu.v

@@ -0,0 +1,382 @@
+`timescale 1ns/1ps
+`include "clog2.vh"
+
+module mcu #(
+    parameter memfile = "",
+    parameter memsize = 8192,
+    parameter sim = 1'b0,
+    parameter jtag = 1
+)(
+    input wire i_clk,
+    input wire i_rst,
+
+    input wire [31:0] i_GPI_A,
+    input wire [31:0] i_GPI_B,
+    input wire [31:0] i_GPI_C,
+    input wire [31:0] i_GPI_D,
+    output wire [31:0] o_GPO_A,
+    output wire [31:0] o_GPO_B,
+    output wire [31:0] o_GPO_C,
+    output wire [31:0] o_GPO_D
+);
+    localparam WITH_CSR = 1;
+    localparam rf_width = 8;
+
+    wire rst;
+    wire rst_wb;
+    wire rst_mem_peripherals;
+    wire rst_cmd_jtag;
+    wire timer_irq;
+    assign rst = i_rst | rst_mem_peripherals | rst_cmd_jtag;
+    // Keep the Wishbone path alive during JTAG "core reset" so memory can be programmed.
+    assign rst_wb = i_rst;
+
+    // Busses
+    // CPU<->memory interconnect (CPU is a WB master)
+    wire [31:0] wb_mem_adr;
+    wire [31:0] wb_mem_dat;
+    wire [3:0] wb_mem_sel;
+    wire wb_mem_we;
+    wire wb_mem_stb;
+    wire [31:0] wb_mem_rdt_cpu;
+    wire wb_mem_ack_cpu;
+
+    // Interconnect->memory (shared WB slave side)
+    wire [31:0] wb_mem_adr_s;
+    wire [31:0] wb_mem_dat_s;
+    wire [3:0] wb_mem_sel_s;
+    wire wb_mem_we_s;
+    wire wb_mem_stb_s;
+    wire [31:0] wb_mem_rdt_s;
+    wire wb_mem_ack_s;
+
+    //  CPU->peripherals
+    wire [31:0] wb_ext_adr;
+    wire [31:0] wb_ext_dat;
+    wire [3:0] wb_ext_sel;
+    wire wb_ext_we;
+    wire wb_ext_stb;
+    wire [31:0] wb_ext_rdt;
+    wire wb_ext_ack;
+    
+    // GPIO
+    wire [4*32-1:0] GPO;
+    wire [4*32-1:0] GPI;
+    assign o_GPO_A = GPO[32*1-1:32*0];
+    assign o_GPO_B = GPO[32*2-1:32*1];
+    assign o_GPO_C = GPO[32*3-1:32*2];
+    assign o_GPO_D = GPO[32*4-1:32*3];
+    assign GPI[32*1-1:32*0] = i_GPI_A;
+    assign GPI[32*2-1:32*1] = i_GPI_B;
+    assign GPI[32*3-1:32*2] = i_GPI_C;
+    assign GPI[32*4-1:32*3] = i_GPI_D;
+
+    cpu #(
+        .sim(sim),
+        .WITH_CSR(WITH_CSR),
+        .rf_width(rf_width)
+    ) cpu (
+        .i_clk(i_clk),
+        .i_rst(rst),
+        .i_timer_irq(timer_irq),
+
+        //Memory interface
+        .o_wb_mem_adr(wb_mem_adr),
+        .o_wb_mem_dat(wb_mem_dat),
+        .o_wb_mem_sel(wb_mem_sel),
+        .o_wb_mem_we(wb_mem_we),
+        .o_wb_mem_stb(wb_mem_stb),
+        .i_wb_mem_rdt(wb_mem_rdt_cpu),
+        .i_wb_mem_ack(wb_mem_ack_cpu),
+
+        //Extension interface
+        .o_wb_ext_adr(wb_ext_adr),
+        .o_wb_ext_dat(wb_ext_dat),
+        .o_wb_ext_sel(wb_ext_sel),
+        .o_wb_ext_we(wb_ext_we),
+        .o_wb_ext_stb(wb_ext_stb),
+        .i_wb_ext_rdt(wb_ext_rdt),
+        .i_wb_ext_ack(wb_ext_ack)
+    );
+
+    generate
+        if (jtag) begin : gen_jtag_wb
+            wire [31:0] wb_jtag_adr;
+            wire [31:0] wb_jtag_dat;
+            wire [3:0] wb_jtag_sel;
+            wire wb_jtag_we;
+            wire wb_jtag_cyc;
+            wire wb_jtag_stb;
+            wire [31:0] wb_jtag_rdt;
+            wire wb_jtag_ack;
+
+            wire [2*32-1:0] wbm_adr_i;
+            wire [2*32-1:0] wbm_dat_i;
+            wire [2*4-1:0] wbm_sel_i;
+            wire [1:0] wbm_we_i;
+            wire [1:0] wbm_cyc_i;
+            wire [1:0] wbm_stb_i;
+            wire [2*3-1:0] wbm_cti_i;
+            wire [2*2-1:0] wbm_bte_i;
+            wire [2*32-1:0] wbm_dat_o;
+            wire [1:0] wbm_ack_o;
+            wire [1:0] wbm_err_o;
+            wire [1:0] wbm_rty_o;
+
+            assign wbm_adr_i = {wb_jtag_adr, wb_mem_adr};
+            assign wbm_dat_i = {wb_jtag_dat, wb_mem_dat};
+            assign wbm_sel_i = {wb_jtag_sel, wb_mem_sel};
+            assign wbm_we_i = {wb_jtag_we, wb_mem_we};
+            assign wbm_cyc_i = {wb_jtag_cyc, wb_mem_stb};
+            assign wbm_stb_i = {wb_jtag_stb, wb_mem_stb};
+            assign wbm_cti_i = 6'b0;
+            assign wbm_bte_i = 4'b0;
+
+            assign wb_mem_rdt_cpu = wbm_dat_o[31:0];
+            assign wb_mem_ack_cpu = wbm_ack_o[0];
+            assign wb_jtag_rdt = wbm_dat_o[63:32];
+            assign wb_jtag_ack = wbm_ack_o[1];
+
+            wb_arbiter #(
+                .dw(32),
+                .aw(32),
+                .num_masters(2)
+            ) wb_mem_arbiter (
+                .wb_clk_i(i_clk),
+                .wb_rst_i(rst_wb),
+                .wbm_adr_i(wbm_adr_i),
+                .wbm_dat_i(wbm_dat_i),
+                .wbm_sel_i(wbm_sel_i),
+                .wbm_we_i(wbm_we_i),
+                .wbm_cyc_i(wbm_cyc_i),
+                .wbm_stb_i(wbm_stb_i),
+                .wbm_cti_i(wbm_cti_i),
+                .wbm_bte_i(wbm_bte_i),
+                .wbm_dat_o(wbm_dat_o),
+                .wbm_ack_o(wbm_ack_o),
+                .wbm_err_o(wbm_err_o),
+                .wbm_rty_o(wbm_rty_o),
+                .wbs_adr_o(wb_mem_adr_s),
+                .wbs_dat_o(wb_mem_dat_s),
+                .wbs_sel_o(wb_mem_sel_s),
+                .wbs_we_o(wb_mem_we_s),
+                .wbs_cyc_o(),
+                .wbs_stb_o(wb_mem_stb_s),
+                .wbs_cti_o(),
+                .wbs_bte_o(),
+                .wbs_dat_i(wb_mem_rdt_s),
+                .wbs_ack_i(wb_mem_ack_s),
+                .wbs_err_i(1'b0),
+                .wbs_rty_i(1'b0)
+            );
+
+            jtag_wb_bridge #(
+                .chain(1)
+            ) jtag_wb (
+                .i_clk(i_clk),
+                .i_rst(i_rst),
+                .o_wb_adr(wb_jtag_adr),
+                .o_wb_dat(wb_jtag_dat),
+                .o_wb_sel(wb_jtag_sel),
+                .o_wb_we(wb_jtag_we),
+                .o_wb_cyc(wb_jtag_cyc),
+                .o_wb_stb(wb_jtag_stb),
+                .i_wb_rdt(wb_jtag_rdt),
+                .i_wb_ack(wb_jtag_ack),
+                .o_cmd_reset(rst_cmd_jtag)
+            );
+        end else begin : gen_no_jtag_wb
+            assign wb_mem_adr_s = wb_mem_adr;
+            assign wb_mem_dat_s = wb_mem_dat;
+            assign wb_mem_sel_s = wb_mem_sel;
+            assign wb_mem_we_s = wb_mem_we;
+            assign wb_mem_stb_s = wb_mem_stb;
+            assign wb_mem_rdt_cpu = wb_mem_rdt_s;
+            assign wb_mem_ack_cpu = wb_mem_ack_s;
+            assign rst_cmd_jtag = 1'b0;
+        end
+    endgenerate
+
+    memory #(
+        .memfile(memfile),
+        .memsize(memsize),
+        .sim(sim)
+    ) memory (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .i_wb_rst(rst_wb),
+        .i_wb_adr(wb_mem_adr_s),
+        .i_wb_dat(wb_mem_dat_s),
+        .i_wb_sel(wb_mem_sel_s),
+        .i_wb_we(wb_mem_we_s),
+        .i_wb_stb(wb_mem_stb_s),
+        .o_wb_rdt(wb_mem_rdt_s),
+        .o_wb_ack(wb_mem_ack_s)
+    );
+
+    mcu_peripherals peripherals (
+        .i_clk(i_clk),
+        .i_rst(rst),
+        .i_wb_adr(wb_ext_adr),
+        .i_wb_dat(wb_ext_dat),
+        .i_wb_sel(wb_ext_sel),
+        .i_wb_we(wb_ext_we),
+        .i_wb_stb(wb_ext_stb),
+        .o_wb_rdt(wb_ext_rdt),
+        .o_wb_ack(wb_ext_ack),
+        // Peripheral IO
+        .i_gpio(GPI),
+        .o_gpio(GPO),
+        .o_timer_irq(timer_irq),
+        .o_core_reset(rst_mem_peripherals)
+    );
+
+endmodule
+
+module cpu #(
+    parameter sim = 1'b0,
+    parameter WITH_CSR = 1,
+    parameter rf_width = 8
+)(
+    input wire i_clk,
+    input wire i_rst,
+    input wire i_timer_irq,
+    // CPU->memory
+    output wire [31:0] o_wb_mem_adr,
+    output wire [31:0] o_wb_mem_dat,
+    output wire [3:0] o_wb_mem_sel,
+    output wire o_wb_mem_we,
+    output wire o_wb_mem_stb,
+    input wire [31:0] i_wb_mem_rdt,
+    input wire i_wb_mem_ack,
+    // CPU->peripherals
+    output wire [31:0] o_wb_ext_adr,
+    output wire [31:0] o_wb_ext_dat,
+    output wire [3:0] o_wb_ext_sel,
+    output wire o_wb_ext_we,
+    output wire o_wb_ext_stb,
+    input wire [31:0] i_wb_ext_rdt,
+    input wire i_wb_ext_ack
+);
+    wire [6+WITH_CSR:0] rf_waddr;
+    wire [rf_width-1:0] rf_wdata;
+    wire rf_wen;
+    wire [6+WITH_CSR:0] rf_raddr;
+    wire [rf_width-1:0] rf_rdata;
+    wire rf_ren;
+
+    // SERV core with mux splitting dbus into mem and ext and
+    // arbiter combining mem and ibus.
+    servile #(
+        .reset_pc(32'h0000_0000),
+        .reset_strategy("MINI"),
+        .rf_width(rf_width),
+        .sim(sim),
+        .with_csr(WITH_CSR),
+        .with_c(0),
+        .with_mdu(0)
+    ) servile (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .i_timer_irq(i_timer_irq),
+
+        .o_wb_mem_adr(o_wb_mem_adr),
+        .o_wb_mem_dat(o_wb_mem_dat),
+        .o_wb_mem_sel(o_wb_mem_sel),
+        .o_wb_mem_we(o_wb_mem_we),
+        .o_wb_mem_stb(o_wb_mem_stb),
+        .i_wb_mem_rdt(i_wb_mem_rdt),
+        .i_wb_mem_ack(i_wb_mem_ack),
+
+        .o_wb_ext_adr(o_wb_ext_adr),
+        .o_wb_ext_dat(o_wb_ext_dat),
+        .o_wb_ext_sel(o_wb_ext_sel),
+        .o_wb_ext_we(o_wb_ext_we),
+        .o_wb_ext_stb(o_wb_ext_stb),
+        .i_wb_ext_rdt(i_wb_ext_rdt),
+        .i_wb_ext_ack(i_wb_ext_ack),
+
+        .o_rf_waddr(rf_waddr),
+        .o_rf_wdata(rf_wdata),
+        .o_rf_wen(rf_wen),
+        .o_rf_raddr(rf_raddr),
+        .o_rf_ren(rf_ren),
+        .i_rf_rdata(rf_rdata)
+    );
+
+    serv_rf_ram #(
+        .width(rf_width),
+        .csr_regs(WITH_CSR*4)
+    ) rf_ram (
+        .i_clk(i_clk),
+        .i_waddr(rf_waddr),
+        .i_wdata(rf_wdata),
+        .i_wen(rf_wen),
+        .i_raddr(rf_raddr),
+        .i_ren(rf_ren),
+        .o_rdata(rf_rdata)
+    );
+endmodule
+
+module memory #(
+    parameter memfile = "",
+    parameter memsize = 8192,
+    parameter sim = 1'b0
+)(
+    input wire i_clk,
+    input wire i_rst,
+    input wire i_wb_rst,
+    input wire [31:0] i_wb_adr,
+    input wire [31:0] i_wb_dat,
+    input wire [3:0] i_wb_sel,
+    input wire i_wb_we,
+    input wire i_wb_stb,
+    output wire [31:0] o_wb_rdt,
+    output wire o_wb_ack
+);
+    localparam mem_depth = memsize/4;
+    localparam mem_aw = `CLOG2(mem_depth);
+
+    reg [31:0] mem [0:mem_depth-1] /* verilator public */;
+    reg [31:0] wb_rdt_r;
+    reg wb_ack_r;
+    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;
+
+    always @(posedge i_clk) begin
+        if (i_rst || i_wb_rst) begin
+            wb_ack_r <= 1'b0;
+            wb_rdt_r <= 32'b0;
+        end else begin
+            wb_ack_r <= i_wb_stb & ~wb_ack_r;
+
+            if (i_wb_stb & ~wb_ack_r) begin
+                wb_rdt_r <= mem[wb_word_adr];
+
+                if (i_wb_we) begin
+                    if (i_wb_sel[0]) mem[wb_word_adr][7:0] <= i_wb_dat[7:0];
+                    if (i_wb_sel[1]) mem[wb_word_adr][15:8] <= i_wb_dat[15:8];
+                    if (i_wb_sel[2]) mem[wb_word_adr][23:16] <= i_wb_dat[23:16];
+                    if (i_wb_sel[3]) mem[wb_word_adr][31:24] <= i_wb_dat[31:24];
+                end
+            end
+        end
+    end
+
+    integer i;
+    initial begin
+        if (sim == 1'b1) begin
+            for (i = 0; i < mem_depth; i = i + 1)
+                mem[i] = 32'h00000000;
+        end
+        if (|memfile) begin
+            $display("Preloading %m from %s", memfile);
+            $readmemh(memfile, mem);
+        end
+        wb_rdt_r = 32'b0;
+        wb_ack_r = 1'b0;
+    end
+
+endmodule

cores/system/mcu/rtl/mcu_peripherals.v

@@ -0,0 +1,131 @@
+`timescale 1ns/1ps
+
+module mcu_peripherals (
+    input wire i_clk,
+    input wire i_rst,
+
+    input wire [31:0] i_wb_adr,
+    input wire [31:0] i_wb_dat,
+    input wire [3:0] i_wb_sel,
+    input wire i_wb_we,
+    input wire i_wb_stb,
+    output wire [31:0] o_wb_rdt,
+    output wire o_wb_ack,
+
+    input wire [4*32-1:0] i_gpio,
+    output wire [4*32-1:0] o_gpio,
+    output wire o_timer_irq,
+    output wire o_core_reset
+);
+    localparam [31:0] GPIO_BASE_ADDR = 32'h4000_0000;
+    localparam [31:0] GPIO_ADDR_MASK = 32'hFFFF_0000;
+    localparam [31:0] TIMER_BASE_ADDR = 32'h4001_0000;
+    localparam [31:0] TIMER_ADDR_MASK = 32'hFFFF_0000;
+
+    assign o_core_reset = 1'b0;
+
+    wire [2*32-1:0] wbs_adr;
+    wire [2*32-1:0] wbs_dat_w;
+    wire [2*4-1:0] wbs_sel;
+    wire [1:0] wbs_we;
+    wire [1:0] wbs_cyc;
+    wire [1:0] wbs_stb;
+    wire [2*3-1:0] wbs_cti;
+    wire [2*2-1:0] wbs_bte;
+    wire [2*32-1:0] wbs_dat_r;
+    wire [1:0] wbs_ack;
+
+    wire [31:0] gpio_wbs_adr = wbs_adr[0*32 +: 32];
+    wire [31:0] gpio_wbs_dat_w = wbs_dat_w[0*32 +: 32];
+    wire [3:0] gpio_wbs_sel = wbs_sel[0*4 +: 4];
+    wire gpio_wbs_we = wbs_we[0];
+    wire gpio_wbs_cyc = wbs_cyc[0];
+    wire gpio_wbs_stb = wbs_stb[0];
+    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];
+    wire [31:0] timer_wbs_dat_r;
+    wire timer_wbs_ack;
+
+    wb_mux #(
+        .dw(32),
+        .aw(32),
+        .num_slaves(2),
+        .MATCH_ADDR({TIMER_BASE_ADDR, GPIO_BASE_ADDR}),
+        .MATCH_MASK({TIMER_ADDR_MASK, GPIO_ADDR_MASK})
+    ) ext_mux (
+        .wb_clk_i(i_clk),
+        .wb_rst_i(i_rst),
+
+        .wbm_adr_i(i_wb_adr),
+        .wbm_dat_i(i_wb_dat),
+        .wbm_sel_i(i_wb_sel),
+        .wbm_we_i(i_wb_we),
+        .wbm_cyc_i(i_wb_stb),
+        .wbm_stb_i(i_wb_stb),
+        .wbm_cti_i(3'b000),
+        .wbm_bte_i(2'b00),
+        .wbm_dat_o(o_wb_rdt),
+        .wbm_ack_o(o_wb_ack),
+        .wbm_err_o(),
+        .wbm_rty_o(),
+        
+        .wbs_adr_o(wbs_adr),
+        .wbs_dat_o(wbs_dat_w),
+        .wbs_sel_o(wbs_sel),
+        .wbs_we_o(wbs_we),
+        .wbs_cyc_o(wbs_cyc),
+        .wbs_stb_o(wbs_stb),
+        .wbs_cti_o(wbs_cti),
+        .wbs_bte_o(wbs_bte),
+        .wbs_dat_i(wbs_dat_r),
+        .wbs_ack_i(wbs_ack),
+        .wbs_err_i(2'b00),
+        .wbs_rty_i(2'b00)
+    );
+
+    wb_gpio_banks #(
+        .BASE_ADDR(GPIO_BASE_ADDR),
+        .NUM_BANKS(4)
+    ) gpio (
+        .i_wb_clk(i_clk),
+        .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_cyc(gpio_wbs_cyc),
+        .i_wb_sel(gpio_wbs_sel),
+        .o_wb_rdt(gpio_wbs_dat_r),
+        .o_wb_ack(gpio_wbs_ack),
+        .i_gpio(i_gpio),
+        .o_gpio(o_gpio)
+    );
+
+    assign wbs_dat_r[0*32 +: 32] = gpio_wbs_dat_r;
+    assign wbs_ack[0] = gpio_wbs_ack;
+
+    wb_countdown_timer timer (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .o_irq(o_timer_irq),
+        .i_wb_adr(timer_wbs_adr),
+        .i_wb_dat(timer_wbs_dat_w),
+        .o_wb_dat(timer_wbs_dat_r),
+        .i_wb_sel(timer_wbs_sel),
+        .i_wb_we(timer_wbs_we),
+        .i_wb_cyc(timer_wbs_cyc),
+        .i_wb_stb(timer_wbs_stb),
+        .o_wb_ack(timer_wbs_ack)
+    );
+
+
+    assign wbs_dat_r[1*32 +: 32] = timer_wbs_dat_r;
+    assign wbs_ack[1] = timer_wbs_ack;
+endmodule

cores/system/test/rtl/toplevel.v

@@ -1,6 +1,9 @@
 `timescale 1ns/1ps
 
-module toplevel(
+module toplevel #(
+    parameter sim = 0,
+    parameter memfile = "sweep.hex"
+)(
     input wire aclk,
     input wire aresetn,
 
@@ -11,6 +14,7 @@ module toplevel(
     output wire[7:0] LED
 
 );
+    `include "conv.vh"
 
     // Clocking
     wire clk_100;
@@ -25,56 +29,75 @@ module toplevel(
         .clk_out(clk_15)
     );
 
-    wire wb_rst;
-    assign wb_rst = ~aresetn;
 
-    wire [31:0] wb_adr;
+    // Reset conditioning for button input:
-    wire [31:0] wb_dat_w;
+    // - asynchronous assert when button is pressed (aresetn=0)
-    wire [31:0] wb_dat_r;
+    // - synchronous, debounced deassert in clk_15 domain
-    wire [3:0] wb_sel;
+    localparam [17:0] RESET_RELEASE_CYCLES = sim ? 18'd16 : 18'd150000; // ~10 ms @ 15 MHz on hardware
-    wire wb_we;
+    reg [17:0] rst_cnt = 18'd0;
-    wire wb_cyc;
+    reg        sys_reset_r = 1'b1;
-    wire wb_stb;
+    always @(posedge clk_15 or negedge aresetn) begin
-    wire wb_ack;
+        if (!aresetn) begin
-    wire wb_cmd_reset;
+            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 sys_reset = sys_reset_r;
+    wire sys_resetn = !sys_reset_r;
 
-    wire [31:0] gpio_out;
+    wire [31:0] GPIO_A;
-    wire gpio_rst;
+    wire [31:0] GPIO_B;
-    assign gpio_rst = wb_rst;
+    wire [31:0] GPIO_C;
+    wire [31:0] GPIO_D;
 
-    jtag_wb_bridge u_jtag_wb_bridge (
+    wire test;
+
+    mcu #(
+        .memfile(memfile),
+        .sim(sim),
+        .jtag(1)
+    ) mcu (
         .i_clk(clk_15),
-        .i_rst(wb_rst),
+        .i_rst(sys_reset),
-        .o_wb_adr(wb_adr),
+        .i_GPI_A(GPIO_A),
-        .o_wb_dat(wb_dat_w),
+        .i_GPI_B(GPIO_B),
-        .o_wb_sel(wb_sel),
+        .i_GPI_C(GPIO_C),
-        .o_wb_we(wb_we),
+        .i_GPI_D(GPIO_D),
-        .o_wb_cyc(wb_cyc),
+        .o_GPO_A(GPIO_A),
-        .o_wb_stb(wb_stb),
+        .o_GPO_B(GPIO_B),
-        .i_wb_rdt(wb_dat_r),
+        .o_GPO_C(GPIO_C),
-        .i_wb_ack(wb_ack),
+        .o_GPO_D(GPIO_D)
-        .o_cmd_reset(wb_cmd_reset)
     );
 
-    wb_gpio #(
+
-        .address(32'h00000000)
+    wire [15:0] sin_q15;
-    ) u_wb_gpio (
+    wire clk_en;
-        .i_wb_clk(clk_15),
+    nco_q15 #(
-        .i_wb_rst(gpio_rst),
+        .CLK_HZ(15_000_000),
-        .i_wb_adr(wb_adr),
+        .FS_HZ(80_000)
-        .i_wb_dat(wb_dat_w),
+    ) nco (
-        .i_wb_sel(wb_sel),
+        .i_clk    (clk_15),
-        .i_wb_we(wb_we),
+        .i_rst_n  (sys_resetn),
-        .i_wb_stb(wb_cyc & wb_stb),
+        .i_freq_hz(GPIO_A),
-        .i_gpio(gpio_out),
+        .o_sin_q15(sin_q15),
-        .o_wb_rdt(wb_dat_r),
+        .o_cos_q15(),
-        .o_wb_ack(wb_ack),
+        .o_clk_en (clk_en)
-        .o_gpio(gpio_out)
     );
 
-    assign led_green = aresetn;
+    reg [5:0] dac_code;
-    assign led_red = wb_cmd_reset;
+    always @(posedge clk_15) begin
-    assign LED = gpio_out[7:0];
+        dac_code <= q15_to_uq16(sin_q15) >> 10;
-    assign r2r = gpio_out[13:8];
+    end
+    assign r2r = dac_code;
+
+    assign LED = GPIO_B[7:0];
+    assign led_green = GPIO_C[0];
+    assign led_red = GPIO_C[1];
+
 
 endmodule

cores/system/test/sw/.gitignore

@@ -0,0 +1,8 @@
+*.o
+*.hex
+*.bin
+*.map
+*.elf.asm
+*.elf
+*.coe
+*.mif

cores/system/test/sw/sweep/Makefile

@@ -0,0 +1,47 @@
+TOOLCHAIN_PREFIX ?= riscv64-elf-
+
+CC      := $(TOOLCHAIN_PREFIX)gcc
+OBJCOPY := $(TOOLCHAIN_PREFIX)objcopy
+OBJDUMP := $(TOOLCHAIN_PREFIX)objdump
+SIZE    := $(TOOLCHAIN_PREFIX)size
+
+TARGET  := sweep
+SRCS_C  := sweep.c
+SRCS_S  := start.s
+OBJS    := $(SRCS_C:.c=.o) $(SRCS_S:.s=.o)
+
+ARCH_FLAGS := -march=rv32i_zicsr -mabi=ilp32
+CFLAGS     := $(ARCH_FLAGS) -Os -ffreestanding -fno-builtin -Wall -Wextra
+ASFLAGS    := $(ARCH_FLAGS)
+LDFLAGS    := $(ARCH_FLAGS) -nostdlib -nostartfiles -Wl,-Bstatic,-Tlink.ld,--gc-sections,-Map,$(TARGET).map
+
+.PHONY: all clean disasm size
+
+all: $(TARGET).elf $(TARGET).bin $(TARGET).hex $(TARGET).elf.asm
+
+$(TARGET).elf: $(OBJS) link.ld
+	$(CC) $(LDFLAGS) -o $@ $(OBJS)
+
+%.o: %.c
+	$(CC) $(CFLAGS) -c -o $@ $<
+
+%.o: %.s
+	$(CC) $(ASFLAGS) -c -o $@ $<
+
+$(TARGET).bin: $(TARGET).elf
+	$(OBJCOPY) -O binary $< $@
+
+$(TARGET).hex: $(TARGET).bin
+	hexdump -v -e '1/4 "%08x\n"' $< > $@
+
+$(TARGET).elf.asm: $(TARGET).elf
+	$(OBJDUMP) -d -S $< > $@
+
+disasm: $(TARGET).elf.asm
+
+size: $(TARGET).elf
+	$(SIZE) $<
+
+clean:
+	rm -f $(TARGET).elf $(TARGET).bin $(TARGET).hex $(TARGET).coe $(TARGET).mif \
+		$(TARGET).elf.asm $(TARGET).map $(OBJS)

cores/system/test/sw/sweep/link.ld

@@ -0,0 +1,35 @@
+OUTPUT_ARCH("riscv")
+ENTRY(_start)
+
+MEMORY
+{
+  RAM (rwx) : ORIGIN = 0x00000000, LENGTH = 8192 
+}
+
+SECTIONS
+{
+  .text :
+  {
+    KEEP(*(.text.init))
+    *(.text .text.*)
+    *(.rodata .rodata.*)
+  } > RAM
+
+  .data :
+  {
+    *(.data .data.*)
+  } > RAM
+
+  .bss (NOLOAD) :
+  {
+    __bss_start = .;
+    *(.bss .bss.*)
+    *(.sbss .sbss.*)
+    *(.scommon)
+    *(COMMON)
+    __bss_end = .;
+  } > RAM
+
+  . = ALIGN(4);
+  __stack_top = ORIGIN(RAM) + LENGTH(RAM);
+}

cores/system/test/sw/sweep/start.s

@@ -0,0 +1,99 @@
+.section .text.init
+.globl _start
+.type _start, @function
+_start:
+    la sp, __stack_top
+
+    # Zero .bss
+    la t0, __bss_start
+    la t1, __bss_end
+1:
+    bgeu t0, t1, 2f
+    sw zero, 0(t0)
+    addi t0, t0, 4
+    j 1b
+
+2:
+    call main
+
+3:
+    j 3b
+
+.size _start, .-_start
+
+
+.section .text
+.globl trap_entry
+.type trap_entry, @function
+trap_entry:
+    # Save full integer context (except x0/x2) because an interrupt can
+    # preempt code with live values in any register, not just caller-saved.
+    addi sp, sp, -128
+    sw   ra, 124(sp)
+    sw   gp, 120(sp)
+    sw   tp, 116(sp)
+    sw   t0, 112(sp)
+    sw   t1, 108(sp)
+    sw   t2, 104(sp)
+    sw   s0, 100(sp)
+    sw   s1,  96(sp)
+    sw   a0,  92(sp)
+    sw   a1,  88(sp)
+    sw   a2,  84(sp)
+    sw   a3,  80(sp)
+    sw   a4,  76(sp)
+    sw   a5,  72(sp)
+    sw   a6,  68(sp)
+    sw   a7,  64(sp)
+    sw   s2,  60(sp)
+    sw   s3,  56(sp)
+    sw   s4,  52(sp)
+    sw   s5,  48(sp)
+    sw   s6,  44(sp)
+    sw   s7,  40(sp)
+    sw   s8,  36(sp)
+    sw   s9,  32(sp)
+    sw   s10, 28(sp)
+    sw   s11, 24(sp)
+    sw   t3,  20(sp)
+    sw   t4,  16(sp)
+    sw   t5,  12(sp)
+    sw   t6,   8(sp)
+
+    csrr t0, mcause
+    li   t1, 0x80000007      # machine timer interrupt (RV32)
+    bne  t0, t1, 1f
+    call timer_isr           # C function that ACKs/clears the timer so i_timer_irq goes low
+1:
+    lw   t6,   8(sp)
+    lw   t5,  12(sp)
+    lw   t4,  16(sp)
+    lw   t3,  20(sp)
+    lw   s11, 24(sp)
+    lw   s10, 28(sp)
+    lw   s9,  32(sp)
+    lw   s8,  36(sp)
+    lw   s7,  40(sp)
+    lw   s6,  44(sp)
+    lw   s5,  48(sp)
+    lw   s4,  52(sp)
+    lw   s3,  56(sp)
+    lw   s2,  60(sp)
+    lw   a7,  64(sp)
+    lw   a6,  68(sp)
+    lw   a5,  72(sp)
+    lw   a4,  76(sp)
+    lw   a3,  80(sp)
+    lw   a2,  84(sp)
+    lw   a1,  88(sp)
+    lw   a0,  92(sp)
+    lw   s1,  96(sp)
+    lw   s0, 100(sp)
+    lw   t2, 104(sp)
+    lw   t1, 108(sp)
+    lw   t0, 112(sp)
+    lw   tp, 116(sp)
+    lw   gp, 120(sp)
+    lw   ra, 124(sp)
+    addi sp, sp, 128
+    mret

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

@@ -0,0 +1,47 @@
+#include <stdint.h>
+
+#define GPIO_BASE   0x40000000u
+static volatile uint32_t * const R_FREQ     = (volatile uint32_t *)(GPIO_BASE+0);
+static volatile uint32_t * const LEDS       = (volatile uint32_t *)(GPIO_BASE+4);
+static volatile uint32_t * const LEDGR      = (volatile uint32_t *)(GPIO_BASE+8);
+
+#define TIMER_BASE  0x40010000u
+static volatile uint32_t * const TIMER_CNT  = (volatile uint32_t *)(TIMER_BASE+0);
+static volatile uint32_t * const TIMER_LD   = (volatile uint32_t *)(TIMER_BASE+4);
+static volatile uint32_t * const TIMER_ACK  = (volatile uint32_t *)(TIMER_BASE+8);
+
+#define MSTATUS_MIE (1u << 3)
+#define MIE_MTIE    (1u << 7)
+
+extern void trap_entry();
+
+static inline void irq_init() {
+    /* mtvec first */
+    asm volatile ("csrw mtvec, %0" :: "r"(trap_entry));
+
+    /* enable machine timer interrupt */
+    asm volatile ("csrs mie, %0" :: "r"(MIE_MTIE));
+
+    /* global enable last */
+    asm volatile ("csrs mstatus, %0" :: "r"(MSTATUS_MIE));
+}
+
+void timer_isr(){
+    *TIMER_ACK = 1;
+    *LEDGR = ~(*LEDGR);
+}
+
+void main(){
+    irq_init();
+
+    *LEDGR = 1;
+    *TIMER_LD = 2 * 15000000/1000;
+
+    for(;;){
+        for(int i=1000; i<10000; i+=10){
+            *R_FREQ = i;
+            *LEDS = i>>4;
+            // for(int j=0; j<80; j++) asm volatile("nop");
+        }
+    }
+}

cores/system/test/tb/tb_toplevel.v

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

cores/system/test/test.core

@@ -7,11 +7,21 @@ filesets:
     rtl:
         depend:
             - joppeb:primitive:clkgen
-            - joppeb:wb:jtag_wb_bridge
+            - joppeb:system:mcu
-            - joppeb:wb:wb_gpio
+            - joppeb:signal:nco_q15
+            - joppeb:util:conv
         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}
+        file_type: user
 
     mimas:
         files:
@@ -23,11 +33,19 @@ targets:
         filesets:
             - rtl
         toplevel: toplevel
+    sim:
+        default_tool: icarus
+        filesets:
+            - rtl
+            - sw
+            - tb
+        toplevel: tb_toplevel
 
     mimas:
         filesets:
             - rtl
             - mimas
+            - sw
         toplevel: toplevel
         parameters:
             - FPGA_SPARTAN6=true

cores/util/clog2/clog2.vh

@@ -2,6 +2,7 @@
 `define CLOG2_VH
 
 // Verilog-2001 compatible ceil(log2(x)) macro (matches $clog2 semantics).
+`ifndef CLOG2
 `define CLOG2(x) \
   (((x) <= 1) ? 0 : \
    ((x) <= 2) ? 1 : \
@@ -37,3 +38,4 @@
    ((x) <= 2147483648) ? 31 : 32)
 
 `endif
+`endif

cores/util/conv/conv.core

@@ -0,0 +1,16 @@
+CAPI=2:
+
+name: joppeb:util:conv:1.0
+description: Verilog conversion helper header
+
+filesets:
+    include:
+        files:
+            - conv.vh:
+                is_include_file: true
+        file_type: verilogSource
+
+targets:
+    default:
+        filesets:
+            - include

cores/util/conv/conv.vh

@@ -0,0 +1,16 @@
+`ifndef CONV_VH
+`define CONV_VH
+
+// =============================================================================
+// Convert Q1.15 to a biased UQ0.16 signal
+// =============================================================================
+function [15:0] q15_to_uq16;
+    input [15:0] q15;
+    reg [16:0] biased;
+begin
+    biased = q15 + 17'sd32768;
+    q15_to_uq16 = biased[15:0];
+end
+endfunction
+
+`endif

cores/util/mul_const/mul_const.core

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

cores/util/mul_const/rtl/mul_const.v

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

cores/wb/formal_checker/formal/formal_wb_master_checker.v

@@ -1,73 +1,205 @@
-`timescale 1ns/1ps
+// formal_wb_master_checker.v
+//
+// 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,
+    parameter OPT_USE_RTY              = 0,
+
+    // If 1: require responses only when STB=1 (stricter than spec permission).
+    // If 0: allow "ghost" responses with STB=0; we only COUNT termination when STB=1.
+    parameter OPT_STRICT_RESP_WITH_STB = 0,
+
+    // If 1: require ACK/ERR/RTY to be single-cycle pulses.
+    // If 0: allow them to be held.
+    parameter OPT_PULSE_RESP           = 1,
+
+    // 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,
-    input wire [31:0] i_wb_adr,
+
-    input wire [31:0] i_wb_dat,
+    // Master -> bus
-    input wire [3:0]  i_wb_sel,
-    input wire        i_wb_we,
-    input wire        i_wb_stb,
     input  wire              i_wb_cyc,
-    input wire [31:0] o_wb_rdt,
+    input  wire              i_wb_stb,
-    input wire        o_wb_ack
+    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;
 
-        // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
+    wire f_resp_any;
-        if(o_wb_ack)
+    assign f_resp_any = o_wb_ack
-            assume(
+                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
-                (i_wb_cyc && i_wb_stb) ||
+                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
-                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
-            );
 
-        // A2: Slave must not ACK outside an active cycle
+    // A "real" termination in Classic requires STB high (handshake qualifies the transfer)
-        if(!i_wb_cyc)
+    wire f_terminate;
-            assume(!o_wb_ack);
+    assign f_terminate = i_wb_cyc && i_wb_stb && f_resp_any;
 
-        // A3: Once STB has been low for a full cycle, slave ACK must be low
+    // -----------------------------
-        if(
+    // Track exactly one outstanding request (Classic)
-            f_past_valid &&
+    // -----------------------------
-            !$past(i_wb_stb) &&
+    reg f_pending;
-            !i_wb_stb
+    initial f_pending = 1'b0;
-        )
-            assume(!o_wb_ack);
 
-        // R1: Reset must leave the master initialized on the following cycle
+    always @(posedge i_clk or posedge rst_any) begin
-        if(f_past_valid && $past(i_rst || i_wb_rst)) begin
+        if (rst_any) begin
-            assert(!i_wb_cyc);
+            f_pending <= 1'b0;
-            assert(!i_wb_stb);
+        end else if (!i_wb_cyc) begin
+            // 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
     end
 
-        // R2: STB never high without CYC
+    // -----------------------------
-        if(i_wb_stb)
+    // Reset rules (Wishbone synchronous reset semantics)
-            assert(i_wb_cyc);
+    // -----------------------------
+    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);
 
-        // R3: Once a request starts, hold it stable until the slave responds
+            if (OPT_STRICT_RESET && $past(rst_any)) begin
-        if(
+                // R01: After reset was asserted on the prior clock, master must be idle
-            f_past_valid &&
+                R01: assert(!i_wb_cyc);
-            $past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
+                // R02: After reset was asserted on the prior clock, master must not strobe
-            !o_wb_ack &&
+                R02: assert(!i_wb_stb);
-            !(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 ($past(rst_any)) begin
-        if(!i_wb_cyc)
+                // A00: After reset was asserted on the prior clock, environment should not respond
-            assert(!i_wb_stb);
+                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
 
-    wire unused = &{1'b0, o_wb_rdt};
+    // -----------------------------
+    // 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

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,68 +1,222 @@
-`timescale 1ns/1ps
+// formal_wb_slave_checker.v
+//
+// 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,
+    parameter OPT_USE_RTY              = 0,
+
+    // If 1: require slave to only assert responses when STB=1 (stricter profile).
+    // If 0: allow "ghost" responses with STB=0; termination still only counts when STB=1.
+    parameter OPT_STRICT_RESP_WITH_STB = 0,
+
+    // If 1: require termination signals to be pulses (1 cycle).
+    // If 0: allow them to be held.
+    parameter OPT_PULSE_RESP           = 1,
+
+    // 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,
-    input wire [31:0] i_wb_adr,
+
-    input wire [31:0] i_wb_dat,
+    // Master -> slave
-    input wire [3:0]  i_wb_sel,
-    input wire        i_wb_we,
-    input wire        i_wb_stb,
     input  wire              i_wb_cyc,
-    input wire [31:0] o_wb_rdt,
+    input  wire              i_wb_stb,
-    input wire        o_wb_ack
+    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;
 
-        // A1: Reset forces cyc=0, stb=0
+    wire f_resp_any;
-        if (i_rst) begin
+    assign f_resp_any = o_wb_ack
-            assume(!i_wb_cyc);
+                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
-            assume(!i_wb_stb);
+                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
+
+    // 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
     end
 
-        // A2: std->cyc, stb never high without cyc
+    // -----------------------------
-        if(i_wb_stb)
+    // Reset rules (Wishbone synchronous reset semantics)
-            assume(i_wb_cyc);
+    // -----------------------------
+    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);
 
-        // A3: once a request starts, hold it stable until the slave responds
+            if (OPT_STRICT_RESET && $past(rst_any)) begin
-        if(f_past_valid && $past(i_wb_cyc && i_wb_stb && !o_wb_ack)) begin
+                // A00: After reset was asserted on the prior clock, assume master is idle
-            assume(i_wb_cyc);
+                A00: assume(!i_wb_cyc);
-            assume(i_wb_stb);
+                // A01: After reset was asserted on the prior clock, assume master is not strobing
-            assume(i_wb_adr == $past(i_wb_adr));
+                A01: assume(!i_wb_stb);
-            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 ($past(rst_any)) begin
-        if(o_wb_ack)
+                // R01: After reset was asserted on the prior clock, slave must not respond
-            assert(
+                R01: assert(!o_wb_ack);
-                (i_wb_cyc && i_wb_stb) ||
+                if (OPT_USE_ERR) R02: assert(!o_wb_err);
-                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
+                if (OPT_USE_RTY) R03: assert(!o_wb_rty);
-            );
+            end
-
+        end
-        // 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};
+    // -----------------------------
+    // 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

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby

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

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby

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

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt

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

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path

@@ -0,0 +1 @@
+../jtag_wb_bridge/status.sqlite

cores/wb/jtag_wb_bridge/rtl/jtag_wb_bridge.v

@@ -505,8 +505,8 @@ module jtag_wb_bridge #(
         // Mark active command complete
         act_valid <= 1'b0;
 
-        // If there is a queued command, promote and start it
+        // If there is a queued command and the WB port is idle, promote it now.
-        if (q_valid) begin
+        if (q_valid && !wb_busy) begin
           act_valid  <= 1'b1;
           act_opcode <= q_opcode;
           act_addr   <= q_addr;

cores/wb/jtag_wb_bridge/tool/libjtag_wb_bridge/Makefile

@@ -32,7 +32,7 @@ $(SHARED_LIB): $(LIB_OBJS)
 	$(CXX) -shared $(LDFLAGS) -o $@ $(LIB_OBJS) $(LIBS)
 
 $(TARGET): $(APP_OBJS) $(STATIC_LIB)
-	$(CXX) $(LDFLAGS) -o $@ $(APP_OBJS) -L. -ljtag_wb_bridge $(LIBS)
+	$(CXX) $(LDFLAGS) -o $@ $(APP_OBJS) -L. $(STATIC_LIB) $(LIBS)
 
 %.o: %.cpp
 	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $<

cores/wb/jtag_wb_bridge/tool/libjtag_wb_bridge/jtag_wb_bridge_client.cpp

@@ -107,7 +107,7 @@ bool JtagWishboneBridge::ping() {
   ping_value = static_cast<uint8_t>(response & 0xffu);
   if (ping_value != 0xa5) {
     char msg[96];
-    std::snprintf(msg, sizeof(msg), "ping mismatch: expected 0xa4, got 0x%02x", ping_value);
+    std::snprintf(msg, sizeof(msg), "ping mismatch: expected 0xa5, got 0x%02x", ping_value);
     return setError(msg);
   }
   last_error_.clear();

cores/wb/jtag_wb_bridge/tool/libjtag_wb_bridge/prog.cpp

@@ -31,15 +31,10 @@ int main(int argc, char** argv) {
     return -1;
   }
 
-  uint8_t ping_value = 0;
   if (!bridge.ping()) {
     std::printf("PING command failed: %s\n", bridge.lastError().c_str());
     return -1;
   }
-  if (ping_value != 0xa5u) {
-    std::printf("PING response was not right: %02x\n", ping_value);
-    return -1;
-  }
 
   const std::string file = parser.getString("file");
   FILE* f = std::fopen(file.c_str(), "rb");

cores/wb/jtag_wb_bridge/tool/test.py

@@ -5,4 +5,4 @@ with JtagBridge() as bridge:
     bridge.clear_flags()
     bridge.ping()
 
-    bridge.write32(0x0, 0xAA)
+    bridge.write8(0x0, 0xAA)

cores/wb/wb_arbiter/rtl/arbiter.v

@@ -0,0 +1,138 @@
+/**
+ * Module: arbiter
+ *
+ * Description:
+ *  A look ahead, round-robing parameterized arbiter.
+ *
+ * <> request
+ *  each bit is controlled by an actor and each actor can 'request' ownership
+ *  of the shared resource by bring high its request bit.
+ *
+ * <> grant
+ *  when an actor has been given ownership of shared resource its 'grant' bit
+ *  is driven high
+ *
+ * <> select
+ *  binary representation of the grant signal (optional use)
+ *
+ * <> active
+ *  is brought high by the arbiter when (any) actor has been given ownership
+ *  of shared resource.
+ *
+ *
+ * Created: Sat Jun  1 20:26:44 EDT 2013
+ *
+ * Author:  Berin Martini // berin.martini@gmail.com
+ */
+ `ifndef _arbiter_ `define _arbiter_
+ `include "clog2.vh"
+
+module arbiter
+  #(parameter
+    NUM_PORTS = 6,
+    SEL_WIDTH = ((NUM_PORTS > 1) ? `CLOG2(NUM_PORTS) : 1))
+   (input wire                  clk,
+    input wire                  rst,
+    input wire [NUM_PORTS-1:0]  request,
+    output reg [NUM_PORTS-1:0]  grant,
+    output reg [SEL_WIDTH-1:0]  select,
+    output reg                  active
+);
+
+    /**
+     * Local parameters
+     */
+
+    localparam WRAP_LENGTH = 2*NUM_PORTS;
+
+
+    // Find First 1 - Start from MSB and count downwards, returns 0 when no
+    // bit set
+    function [SEL_WIDTH-1:0] ff1 (
+        input [NUM_PORTS-1:0] in
+    );
+        reg     set;
+        integer i;
+
+        begin
+            set = 1'b0;
+            ff1 = 'b0;
+
+            for (i = 0; i < NUM_PORTS; i = i + 1) begin
+                if (in[i] & ~set) begin
+                    set = 1'b1;
+                    ff1 = i[0 +: SEL_WIDTH];
+                end
+            end
+        end
+    endfunction
+
+
+`ifdef VERBOSE
+    initial $display("Bus arbiter with %d units", NUM_PORTS);
+`endif
+
+
+    /**
+     * Internal signals
+     */
+
+    integer                 yy;
+
+    wire                    next;
+    wire [NUM_PORTS-1:0]    order;
+
+    reg  [NUM_PORTS-1:0]    token;
+    wire [NUM_PORTS-1:0]    token_lookahead [NUM_PORTS-1:0];
+    wire [WRAP_LENGTH-1:0]  token_wrap;
+
+
+    /**
+     * Implementation
+     */
+
+    assign token_wrap   = {token, token};
+
+    assign next         = ~|(token & request);
+
+
+    always @(posedge clk)
+        grant <= token & request;
+
+
+    always @(posedge clk)
+        select <= ff1(token & request);
+
+
+    always @(posedge clk)
+        active <= |(token & request);
+
+
+    always @(posedge clk)
+        if (rst) token <= 'b1;
+        else if (next) begin
+
+            for (yy = 0; yy < NUM_PORTS; yy = yy + 1) begin : TOKEN_
+
+                if (order[yy]) begin
+                    token <= token_lookahead[yy];
+                end
+            end
+        end
+
+
+    genvar xx;
+    generate
+        for (xx = 0; xx < NUM_PORTS; xx = xx + 1) begin : ORDER_
+
+            assign token_lookahead[xx]  = token_wrap[xx +: NUM_PORTS];
+
+            assign order[xx]            = |(token_lookahead[xx] & request);
+
+        end
+    endgenerate
+
+
+endmodule
+
+`endif //  `ifndef _arbiter_

cores/wb/wb_arbiter/rtl/wb_arbiter.v

@@ -0,0 +1,101 @@
+/* wb_arbiter. Part of wb_intercon
+ *
+ * ISC License
+ *
+ * Copyright (C) 2013-2019  Olof Kindgren <olof.kindgren@gmail.com>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+/*
+ Wishbone arbiter, burst-compatible
+ Simple round-robin arbiter for multiple Wishbone masters
+ */
+`include "clog2.vh"
+
+module wb_arbiter
+ #(parameter dw = 32,
+   parameter aw = 32,
+   parameter num_hosts = 0,
+   parameter num_masters = num_hosts)
+  (
+   input wire			    wb_clk_i,
+   input wire			    wb_rst_i,
+
+   // Wishbone Master Interface
+   input wire [num_masters*aw-1:0]  wbm_adr_i,
+   input wire [num_masters*dw-1:0]  wbm_dat_i,
+   input wire [num_masters*4-1:0]   wbm_sel_i,
+   input wire [num_masters-1:0]	    wbm_we_i,
+   input wire [num_masters-1:0]	    wbm_cyc_i,
+   input wire [num_masters-1:0]	    wbm_stb_i,
+   input wire [num_masters*3-1:0]   wbm_cti_i,
+   input wire [num_masters*2-1:0]   wbm_bte_i,
+   output wire [num_masters*dw-1:0] wbm_dat_o,
+   output wire [num_masters-1:0]    wbm_ack_o,
+   output wire [num_masters-1:0]    wbm_err_o,
+   output wire [num_masters-1:0]    wbm_rty_o,
+
+   // Wishbone Slave interface
+   output wire [aw-1:0]		    wbs_adr_o,
+   output wire [dw-1:0]		    wbs_dat_o,
+   output wire [3:0]		    wbs_sel_o,
+   output wire			    wbs_we_o,
+   output wire			    wbs_cyc_o,
+   output wire			    wbs_stb_o,
+   output wire [2:0]		    wbs_cti_o,
+   output wire [1:0]		    wbs_bte_o,
+   input wire [dw-1:0]		    wbs_dat_i,
+   input wire			    wbs_ack_i,
+   input wire			    wbs_err_i,
+   input wire			    wbs_rty_i);
+
+
+///////////////////////////////////////////////////////////////////////////////
+// Parameters
+///////////////////////////////////////////////////////////////////////////////
+
+   //Use parameter instead of localparam to work around a bug in Xilinx ISE
+   parameter master_sel_bits = num_masters > 1 ? `CLOG2(num_masters) : 1;
+
+   wire [num_masters-1:0]     grant;
+   wire [master_sel_bits-1:0] master_sel;
+   wire 		      active;
+
+   arbiter
+     #(.NUM_PORTS (num_masters))
+   arbiter0
+     (.clk (wb_clk_i),
+      .rst (wb_rst_i),
+      .request (wbm_cyc_i),
+      .grant (grant),
+      .select (master_sel),
+      .active (active));
+/* verilator lint_off WIDTH */
+   //Mux active master
+   assign wbs_adr_o = wbm_adr_i[master_sel*aw+:aw];
+   assign wbs_dat_o = wbm_dat_i[master_sel*dw+:dw];
+   assign wbs_sel_o = wbm_sel_i[master_sel*4+:4];
+   assign wbs_we_o  = wbm_we_i [master_sel];
+   assign wbs_cyc_o = wbm_cyc_i[master_sel] & active;
+   assign wbs_stb_o = wbm_stb_i[master_sel];
+   assign wbs_cti_o = wbm_cti_i[master_sel*3+:3];
+   assign wbs_bte_o = wbm_bte_i[master_sel*2+:2];
+
+   assign wbm_dat_o = {num_masters{wbs_dat_i}};
+   assign wbm_ack_o = ((wbs_ack_i & active) << master_sel);
+   assign wbm_err_o = ((wbs_err_i & active) << master_sel);
+   assign wbm_rty_o = ((wbs_rty_i & active) << master_sel);
+/* verilator lint_on WIDTH */
+
+endmodule // wb_arbiter

cores/wb/wb_arbiter/wb_arbiter.core

@@ -0,0 +1,42 @@
+CAPI=2:
+
+name: joppeb:wb:wb_arbiter:1.0
+description: Wishbone round-robin arbiter
+
+filesets:
+    rtl:
+        depend:
+            - joppeb:util:clog2
+        files:
+            - rtl/arbiter.v
+            - rtl/wb_arbiter.v
+        file_type: verilogSource
+
+targets:
+    default:
+        filesets:
+            - rtl
+        toplevel: wb_arbiter
+        parameters:
+            - dw
+            - aw
+            - num_hosts
+            - num_masters
+
+parameters:
+    dw:
+        datatype: int
+        description: Wishbone data width
+        paramtype: vlogparam
+    aw:
+        datatype: int
+        description: Wishbone address width
+        paramtype: vlogparam
+    num_hosts:
+        datatype: int
+        description: Deprecated alias for num_masters
+        paramtype: vlogparam
+    num_masters:
+        datatype: int
+        description: Number of wishbone masters
+        paramtype: vlogparam

cores/wb/wb_gpio/formal/formal_wb_gpio.v

@@ -1,35 +1,29 @@
 `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;
 
-    assign i_wb_cyc = i_wb_stb || o_wb_ack;
+    wb_gpio dut (
-
+        .i_clk(i_wb_clk),
-    wb_gpio #(
+        .i_rst(i_wb_rst),
-        .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),
@@ -38,7 +32,7 @@ module formal_wb_gpio #(
 
     formal_wb_slave_checker wb_checker (
         .i_clk(i_wb_clk),
-        .i_rst(i_rst),
+        .i_rst(i_wb_rst),
         .i_wb_rst(i_wb_rst),
         .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
@@ -56,9 +50,13 @@ module formal_wb_gpio #(
         f_past_valid <= 1'b1;
 
         // R1: reads return the sampled GPIO input on the following cycle
-        if (f_past_valid && !$past(i_wb_rst) && !i_wb_rst && $past(i_wb_stb) && !$past(i_wb_we)) begin
+        if(f_past_valid && 
+                !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

cores/wb/wb_gpio/formal/wb_gpio.sby

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

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

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

cores/wb/wb_gpio/rtl/wb_gpio.v

@@ -1,55 +1,52 @@
-module wb_gpio #(
+module wb_gpio (
-  parameter address = 32'h00000000
+    input  wire         i_clk,
-)(
+    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,
-  input  wire [31:0] i_wb_adr,   // optional; can ignore for single-reg
     input  wire [31:0]  i_wb_dat,
+    output reg  [31:0]  o_wb_rdt,
     input  wire [3:0]   i_wb_sel,
     input  wire         i_wb_we,
+    input  wire         i_wb_cyc,
     input  wire         i_wb_stb,
-  input  wire [31:0] i_gpio,
+    output wire         o_wb_ack,
 
-  output reg  [31:0] o_wb_rdt,
+	input  wire	[31:0]	i_gpio,
-  output reg         o_wb_ack,
+	output wire	[31:0]	o_gpio
-  output reg  [31:0] o_gpio
 );
 	
-  initial o_gpio <= 32'h00000000;
+	// Registers
-  initial o_wb_rdt <= 32'h00000000;
+	reg [31:0] gpo;
+	wire [31:0] gpi;
+	assign o_gpio = gpo;
+	assign gpi = i_gpio;
 
-  wire addr_check;
+	reg wb_ack = 0;
-  assign addr_check = (i_wb_adr == address);
+	assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb;
 
-  // One-cycle ACK pulse per request (works even if stb stays high)
+	always @(posedge i_clk) begin
-  initial o_wb_ack <= 1'b0;
+		if(i_rst) begin
-  always @(posedge i_wb_clk) begin
+			gpo <= 0;
-    if (i_wb_rst) begin
+			wb_ack <= 0;
-      o_wb_ack <= 1'b0;
+			o_wb_rdt <= 0;
 		end else begin
-      o_wb_ack <= i_wb_stb & ~o_wb_ack; // pulse while stb asserted
+			// Ack generation
-    end
+            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
-  end
 
-  // Read data (combinational or registered; registered here)
+            // Read cycle
-  always @(posedge i_wb_clk) begin
+            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
-    if (i_wb_rst) begin
+				if(i_wb_sel[0]) o_wb_rdt[7:0] <= gpi[7:0];
-      o_wb_rdt <= 32'h0;
+				if(i_wb_sel[1]) o_wb_rdt[15:8] <= gpi[15:8];
-    end else if (i_wb_stb && !i_wb_we) begin
+				if(i_wb_sel[2]) o_wb_rdt[23:16] <= gpi[23:16];
-      o_wb_rdt <= i_gpio;
+				if(i_wb_sel[3]) o_wb_rdt[31:24] <= gpi[31:24];
             end
+            // write cycle
+            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
+				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];
+				if(i_wb_sel[2]) gpo[23:16] <= i_wb_dat[23:16];
+				if(i_wb_sel[3]) gpo[31:24] <= i_wb_dat[31:24];
 			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
 

cores/wb/wb_gpio/wb_gpio.core

@@ -8,6 +8,7 @@ filesets:
         files:
             - rtl/wb_gpio.v
         file_type: verilogSource
+
     formal_rtl:
         depend:
             - joppeb:wb:formal_checker
@@ -24,8 +25,7 @@ targets:
         filesets:
             - rtl
         toplevel: wb_gpio
-        parameters:
+            
-            - address
     formal:
         default_tool: symbiyosys
         filesets:
@@ -33,11 +33,3 @@ targets:
             - formal_rtl
             - formal_cfg
         toplevel: formal_wb_gpio
-        parameters:
-            - address
-
-parameters:
-    address:
-        datatype: int
-        description: Wishbone address matched by this peripheral
-        paramtype: vlogparam

cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v

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

cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby

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

cores/wb/wb_gpio_banks/rtl/wb_gpio_banks.v

@@ -0,0 +1,61 @@
+`include "clog2.vh"
+
+module wb_gpio_banks #(
+	parameter  num_banks = 4
+)(
+    input  wire         i_clk,
+    input  wire         i_rst,
+
+    input  wire [31:0]  i_wb_adr,
+    input  wire [31:0]  i_wb_dat,
+    output reg  [31:0]  o_wb_rdt,
+    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 [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*32-1:0] bank_rdt;
+
+	genvar gi;
+	generate
+		for(gi=0; gi<num_banks; gi=gi+1) begin : gen_gpio
+			localparam [2+sw-1:0] 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;
+	always @* begin
+		o_wb_rdt = 0;
+		o_wb_ack = 0;
+		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

cores/wb/wb_gpio_banks/wb_gpio_banks.core

@@ -0,0 +1,52 @@
+CAPI=2:
+
+name: joppeb:wb:wb_gpio_banks:1.0
+description: Wishbone GPIO bank wrapper
+
+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:
+        filesets:
+            - rtl
+        toplevel: wb_gpio_banks
+        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:
+        datatype: int
+        description: Number of GPIO banks to instantiate
+        paramtype: vlogparam
+    BASE_ADDR:
+        datatype: int
+        description: Base wishbone address for bank 0
+        paramtype: vlogparam

cores/wb/wb_mem32/formal/wb_mem32.sby

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

cores/wb/wb_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;
+    assign o_wb_ack = wb_ack_r & i_wb_cyc & i_wb_stb;
 
     always @(posedge i_clk) begin
         if (i_rst || i_wb_rst) begin

cores/wb/wb_mux/rtl/wb_mux.v

@@ -0,0 +1,145 @@
+/* wb_mux. Part of wb_intercon
+ *
+ * ISC License
+ *
+ * Copyright (C) 2013-2019  Olof Kindgren <olof.kindgren@gmail.com>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+/*
+ Wishbone multiplexer, burst-compatible
+
+ Simple mux with an arbitrary number of slaves.
+
+ The parameters MATCH_ADDR and MATCH_MASK are flattened arrays
+ aw*NUM_SLAVES sized arrays that are used to calculate the
+ active slave. slave i is selected when
+ (wb_adr_i & MATCH_MASK[(i+1)*aw-1:i*aw] is equal to
+ MATCH_ADDR[(i+1)*aw-1:i*aw]
+ If several regions are overlapping, the slave with the lowest
+ index is selected. This can be used to have fallback
+ functionality in the last slave, in case no other slave was
+ selected.
+
+ If no match is found, the wishbone transaction will stall and
+ an external watchdog is required to abort the transaction
+
+ Todo:
+ Registered master/slave connections
+ Rewrite with System Verilog 2D arrays when tools support them
+*/
+`include "clog2.vh"
+
+module wb_mux
+  #(parameter dw = 32,        // Data width
+    parameter aw = 32,        // Address width
+    parameter num_devices = 2, // Number of devices
+    parameter num_slaves = num_devices, // Number of devices (deprecated)
+    parameter [num_slaves*aw-1:0] MATCH_ADDR = 0,
+    parameter [num_slaves*aw-1:0] MATCH_MASK = 0)
+
+   (
+    input wire			    wb_clk_i,
+    input wire			    wb_rst_i,
+
+    // Master Interface
+    input wire [aw-1:0]		    wbm_adr_i,
+    input wire [dw-1:0]		    wbm_dat_i,
+    input wire [3:0]		    wbm_sel_i,
+    input wire			    wbm_we_i,
+    input wire			    wbm_cyc_i,
+    input wire			    wbm_stb_i,
+    input wire [2:0]		    wbm_cti_i,
+    input wire [1:0]		    wbm_bte_i,
+    output wire [dw-1:0]	    wbm_dat_o,
+    output wire			    wbm_ack_o,
+    output wire			    wbm_err_o,
+    output wire			    wbm_rty_o,
+    // Wishbone Slave interface
+    output wire [num_slaves*aw-1:0] wbs_adr_o,
+    output wire [num_slaves*dw-1:0] wbs_dat_o,
+    output wire [num_slaves*4-1:0]  wbs_sel_o,
+    output wire [num_slaves-1:0]    wbs_we_o,
+    output wire [num_slaves-1:0]    wbs_cyc_o,
+    output wire [num_slaves-1:0]    wbs_stb_o,
+    output wire [num_slaves*3-1:0]  wbs_cti_o,
+    output wire [num_slaves*2-1:0]  wbs_bte_o,
+    input wire [num_slaves*dw-1:0]  wbs_dat_i,
+    input wire [num_slaves-1:0]	    wbs_ack_i,
+    input wire [num_slaves-1:0]	    wbs_err_i,
+    input wire [num_slaves-1:0]	    wbs_rty_i);
+
+///////////////////////////////////////////////////////////////////////////////
+// Master/slave connection
+///////////////////////////////////////////////////////////////////////////////
+
+   //Use parameter instead of localparam to work around a bug in Xilinx ISE
+   parameter slave_sel_bits = num_slaves > 1 ? `CLOG2(num_slaves) : 1;
+
+   reg  			 wbm_err;
+   wire [slave_sel_bits-1:0] 	 slave_sel;
+   wire [num_slaves-1:0] 	 match;
+
+   genvar 			 idx;
+
+   generate
+      for(idx=0; idx<num_slaves ; idx=idx+1) begin : addr_match
+	 assign match[idx] = (wbm_adr_i & MATCH_MASK[idx*aw+:aw]) == MATCH_ADDR[idx*aw+:aw];
+      end
+   endgenerate
+
+//
+// Find First 1 - Start from MSB and count downwards, returns 0 when no bit set
+//
+   function [slave_sel_bits-1:0] ff1;
+      input [num_slaves-1:0] in;
+      integer 		     i;
+
+      begin
+	 ff1 = 0;
+	 for (i = num_slaves-1; i >= 0; i=i-1) begin
+	    if (in[i])
+/* verilator lint_off WIDTH */
+	      ff1 = i;
+/* verilator lint_on WIDTH */
+	 end
+      end
+   endfunction
+
+   assign slave_sel = ff1(match);
+
+   always @(posedge wb_clk_i)
+     wbm_err <= wbm_cyc_i & !(|match);
+
+   assign wbs_adr_o = {num_slaves{wbm_adr_i}};
+   assign wbs_dat_o = {num_slaves{wbm_dat_i}};
+   assign wbs_sel_o = {num_slaves{wbm_sel_i}};
+   assign wbs_we_o  = {num_slaves{wbm_we_i}};
+/* verilator lint_off WIDTH */
+
+   // Expand master CYC to slave bus width before shifting to one-hot select.
+   // Shifting a 1-bit signal would otherwise zero out all but slave 0.
+   assign wbs_cyc_o = match & ({num_slaves{wbm_cyc_i}} << slave_sel);
+/* verilator lint_on WIDTH */
+   assign wbs_stb_o = {num_slaves{wbm_stb_i}};
+
+   assign wbs_cti_o = {num_slaves{wbm_cti_i}};
+   assign wbs_bte_o = {num_slaves{wbm_bte_i}};
+
+   assign wbm_dat_o = wbs_dat_i[slave_sel*dw+:dw];
+   assign wbm_ack_o = wbs_ack_i[slave_sel];
+   assign wbm_err_o = wbs_err_i[slave_sel] | wbm_err;
+   assign wbm_rty_o = wbs_rty_i[slave_sel];
+
+endmodule

cores/wb/wb_mux/wb_mux.core

@@ -0,0 +1,51 @@
+CAPI=2:
+
+name: joppeb:wb:wb_mux:1.0
+description: Wishbone address decoder and multiplexer
+
+filesets:
+    rtl:
+        depend:
+            - joppeb:util:clog2
+        files:
+            - rtl/wb_mux.v
+        file_type: verilogSource
+
+targets:
+    default:
+        filesets:
+            - rtl
+        toplevel: wb_mux
+        parameters:
+            - dw
+            - aw
+            - num_devices
+            - num_slaves
+            - MATCH_ADDR
+            - MATCH_MASK
+
+parameters:
+    dw:
+        datatype: int
+        description: Wishbone data width
+        paramtype: vlogparam
+    aw:
+        datatype: int
+        description: Wishbone address width
+        paramtype: vlogparam
+    num_devices:
+        datatype: int
+        description: Deprecated alias for num_slaves
+        paramtype: vlogparam
+    num_slaves:
+        datatype: int
+        description: Number of wishbone slaves
+        paramtype: vlogparam
+    MATCH_ADDR:
+        datatype: int
+        description: Flattened slave address match table
+        paramtype: vlogparam
+    MATCH_MASK:
+        datatype: int
+        description: Flattened slave address mask table
+        paramtype: vlogparam

cores/wb/wb_timer/formal/formal_wb_timer.v

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

cores/wb/wb_timer/formal/wb_timer.sby

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

cores/wb/wb_timer/rtl/wb_timer.v

@@ -0,0 +1,185 @@
+`timescale 1ns/1ps
+
+module wb_countdown_timer (
+    input  wire         i_clk,
+    input  wire         i_rst,
+    output wire         o_irq,
+
+    input  wire [31:0]  i_wb_adr,
+    input  wire [31:0]  i_wb_dat,
+    output reg  [31:0]  o_wb_dat,
+    input  wire [3:0]   i_wb_sel,
+    input  wire         i_wb_we,
+    input  wire         i_wb_cyc,
+    input  wire         i_wb_stb,
+    output wire         o_wb_ack
+);
+
+    // Registers
+    reg [31:0]       counter; // The actual counter. Generates an interrupt when it reaches 0
+    reg [31:0]       preload; // The value with which the counter gets loaded after it reaches 0. 0 to keep the timer off
+
+    reg wb_ack = 0;
+    reg irq_fired = 0;
+    reg counter_started = 0;
+    reg counter_running = 0;
+    reg prev_counter_running = 0;
+    assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb; // Make sure the ack only happend during a cycle
+
+    assign o_irq = irq_fired;
+
+    always @(posedge i_clk) begin
+        if(i_rst) begin
+            counter <= 0;
+            preload <= 0;
+            wb_ack <= 0;
+            o_wb_dat <= 0;
+            irq_fired <= 0;
+            counter_started <= 0;
+            counter_running <= 0;
+            prev_counter_running <= 0;
+        end else begin
+
+            prev_counter_running <= counter_running;
+            counter_running <= counter>0;
+
+            if(!irq_fired && prev_counter_running && !counter_running)
+                irq_fired <= 1'b1;
+            if(counter>0 && counter_started)
+                counter <= counter - 1;
+
+            if(counter == 0 && preload>0 && counter_started)
+                counter <= preload;
+
+            if(counter == 0 && preload == 0)
+                counter_started <= 1'b0;
+
+            // Ack generation
+            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
+
+            // Read cycle
+            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
+                if(i_wb_adr[3:0] == 4'b0000) begin
+                    if(i_wb_sel[0]) o_wb_dat[7:0] <= counter[7:0];
+                    if(i_wb_sel[1]) o_wb_dat[15:8] <= counter[15:8];
+                    if(i_wb_sel[2]) o_wb_dat[23:16] <= counter[23:16];
+                    if(i_wb_sel[3]) o_wb_dat[31:24] <= counter[31:24];
+                end else if(i_wb_adr[3:0] == 4'b0100) begin
+                    if(i_wb_sel[0]) o_wb_dat[7:0] <= preload[7:0];
+                    if(i_wb_sel[1]) o_wb_dat[15:8] <= preload[15:8];
+                    if(i_wb_sel[2]) o_wb_dat[23:16] <= preload[23:16];
+                    if(i_wb_sel[3]) o_wb_dat[31:24] <= preload[31:24];
+                end
+            end
+
+            // write cycle
+            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
+                if(i_wb_adr[3:0] == 4'b0000) begin
+                    if(i_wb_sel[0]) counter[7:0] <= i_wb_dat[7:0];
+                    if(i_wb_sel[1]) counter[15:8] <= i_wb_dat[15:8];
+                    if(i_wb_sel[2]) counter[23:16] <= i_wb_dat[23:16];
+                    if(i_wb_sel[3]) counter[31:24] <= i_wb_dat[31:24];
+                    counter_started <= 1'b1;
+                end else if(i_wb_adr[3:0] == 4'b0100) begin
+                    if(i_wb_sel[0]) preload[7:0] <= i_wb_dat[7:0];
+                    if(i_wb_sel[1]) preload[15:8] <= i_wb_dat[15:8];
+                    if(i_wb_sel[2]) preload[23:16] <= i_wb_dat[23:16];
+                    if(i_wb_sel[3]) preload[31:24] <= i_wb_dat[31:24];
+                    counter_started <= 1'b1;
+                end else if(i_wb_adr[3:0] == 4'b1000) begin
+                    // Any write to BASE+8 will ack the IRQ
+                    irq_fired <= 1'b0;
+                end
+            end
+
+        end
+    end
+
+`ifdef FORMAL
+    // Formal verification
+    reg f_past_valid = 1'b0;
+    wire cnt_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h0);
+    wire pld_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h4);
+    wire ack_write = i_wb_cyc && i_wb_stb && i_wb_we && (i_wb_adr[3:0] == 4'h8);
+    reg [31:0] past_counter;
+
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+        past_counter <= counter;
+
+        // R1: Reset clears all timer state on the following cycle.
+        // Check counter, preload, wb_ack, o_wb_dat, irq_fired,
+        // counter_started, counter_running, and prev_counter_running.
+        if(f_past_valid && $past(i_rst)) begin
+            R1s1: assert(counter==0);
+            R1s2: assert(preload==0);
+            R1s3: assert(!wb_ack);
+            R1s4: assert(o_wb_dat==0);
+            R1s5: assert(!irq_fired);
+            R1s6: assert(!counter_started);
+            R1s7: assert(!counter_running);
+        end
+
+        // R2: irq_fired is sticky until reset or a write to BASE+8 clears it.
+        // -> if last cycle was irq and last cycle was not reset and not ack write then now still irq
+        if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(!ack_write))
+            R2: assert(irq_fired);
+
+        // R3: A write to BASE+8 clears irq_fired on the following cycle.
+        // -> if last cycle was ack write and irq was high it must be low now
+        if(f_past_valid && $past(!i_rst) && $past(irq_fired) && $past(ack_write))
+            R3: assert(!irq_fired);
+
+        // R4: While the timer is running and no counter write overrides it,
+        // counter decrements by exactly one each cycle.
+        if(f_past_valid && $past(!i_rst) && $past(counter>1) && $past(counter_started) && $past(!cnt_write))
+            R4: assert(counter == $past(counter)-1);
+
+        // R5: When counter reaches zero with preload > 0 and the timer is started,
+        // the counter reloads from preload.
+        if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && $past(counter_started) && $past(!cnt_write))
+            R5: assert(counter == $past(preload));
+
+        // R6: When counter == 0 and preload == 0, the timer stops
+        // (counter_started deasserts unless a write rearms it).
+        if(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload==0) && $past(!cnt_write) && $past(!pld_write)) begin
+            R6s1: assert(counter==0);
+            R6s2: assert(counter_started==0);
+        end
+
+        // R7: A write to BASE+0 or BASE+4 arms the timer
+        // (counter_started asserts on the following cycle).
+        if(f_past_valid && $past(!i_rst) && ($past(cnt_write) || $past(pld_write)))
+            R7: assert(counter_started==1);
+
+        // R8: o_irq always reflects irq_fired.
+        R8: assert(o_irq == irq_fired);
+
+        // R9: Interrupt only fired after counter was 0 two clock cycles ago
+        if(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired)
+            R9: assert($past(past_counter) == 0);
+
+        // C1: Cover a counter write that starts the timer.
+        C1s1: cover(f_past_valid && !i_rst && cnt_write);
+        if(f_past_valid && $past(!i_rst) && $past(cnt_write))
+            C1s2: cover(counter_started);
+
+        // C2: Cover a preload write.
+        C2: cover(f_past_valid && !i_rst && pld_write);
+
+        // C3: Cover the counter decrementing at least once.
+        C3: cover(f_past_valid && $past(!i_rst) && $past(counter)==counter-1 && $past(!cnt_write) && $past(!pld_write));
+
+        // C4: Cover the counter reloading from preload.
+        C4: cover(f_past_valid && $past(!i_rst) && $past(counter==0) && $past(preload>0) && counter>0 && $past(!cnt_write) && $past(!pld_write));
+
+        // C5: Cover irq_fired asserting when the timer expires.
+        C5: cover(f_past_valid && $past(!i_rst) && $past(!irq_fired) && irq_fired && $past(counter==0));
+
+        // C6: Cover irq_fired being cleared by a write to BASE+8.
+        C6: cover(f_past_valid && $past(!i_rst) && $past(irq_fired) && !irq_fired && $past(ack_write));
+
+    end
+`endif
+
+endmodule

cores/wb/wb_timer/tb/tb_wb_timer.v

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

cores/wb/wb_timer/wb_timer.core

@@ -0,0 +1,51 @@
+CAPI=2:
+
+name: joppeb:wb:wb_timer:1.0
+description: Wishbone countdown timer peripheral
+
+filesets:
+    rtl:
+        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
+
+parameters:
+    FORMAL:
+        datatype: bool
+        description: Enable in-module formal-only logic
+        paramtype: vlogdefine

fusesoc.conf

@@ -4,3 +4,14 @@ sync-uri = ./cores
 sync-type = local
 auto-sync = true
 
+[library.serv]
+location = ./fusesoc_libraries/serv
+sync-uri = git@github.com:Jojojoppe/serv.git
+sync-type = local
+auto-sync = true
+
+[library.fusesoc-cores]
+location = ./fusesoc_libraries/fusesoc-cores
+sync-uri = https://github.com/fusesoc/fusesoc-cores
+sync-type = git
+auto-sync = true

xilinx_fusesoc.sh

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