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