fix(rtl,gui,cosim,formal): adapt surrounding files for dual 16-pt FFT (follow-up to PR #33)
- radar_system_top.v: DC notch now masks to dop_bin[3:0] per sub-frame so both sub-frames get their DC zeroed correctly; rename DOPPLER_FFT_SIZE → DOPPLER_FRAME_CHIRPS to avoid confusion with the per-FFT size (now 16) - radar_dashboard.py: remove fftshift (crosses sub-frame boundary), display raw Doppler bins, remove dead velocity constants - golden_reference.py: model dual 16-pt FFT with per-sub-frame Hamming window, update DC notch and CFAR to match RTL - fv_doppler_processor.sby: reference xfft_16.v / fft_twiddle_16.mem, raise BMC depth to 512 and cover to 1024 - fv_radar_mode_controller.sby: raise cover depth to 600 - fv_radar_mode_controller.v: pin cfg_* to reduced constants (documented as single-config proof), fix Property 5 mode guard, strengthen Cover 1 - STALE_NOTICE.md: document that real-data hex files are stale and need regeneration with external dataset Closes #39
This commit is contained in:
Serhii
@@ -4,24 +4,24 @@ cover
|
||||
|
||||
[options]
|
||||
bmc: mode bmc
|
||||
bmc: depth 150
|
||||
bmc: depth 512
|
||||
cover: mode cover
|
||||
cover: depth 150
|
||||
cover: depth 1024
|
||||
|
||||
[engines]
|
||||
smtbmc z3
|
||||
|
||||
[script]
|
||||
read_verilog -formal doppler_processor.v
|
||||
read_verilog -formal xfft_32.v
|
||||
read_verilog -formal xfft_16.v
|
||||
read_verilog -formal fft_engine.v
|
||||
read_verilog -formal fv_doppler_processor.v
|
||||
prep -top fv_doppler_processor
|
||||
|
||||
[files]
|
||||
../doppler_processor.v
|
||||
../xfft_32.v
|
||||
../xfft_16.v
|
||||
../fft_engine.v
|
||||
../fft_twiddle_32.mem
|
||||
../fft_twiddle_16.mem
|
||||
../fft_twiddle_1024.mem
|
||||
fv_doppler_processor.v
|
||||
|
||||
@@ -8,7 +8,8 @@
|
||||
// Single-clock design: clk is an input wire, async2sync handles async reset.
|
||||
// Each formal step = one clock edge.
|
||||
//
|
||||
// Parameters reduced: RANGE_BINS=4, CHIRPS_PER_FRAME=4, CHIRPS_PER_SUBFRAME=2, DOPPLER_FFT_SIZE=2.
|
||||
// Parameters: RANGE_BINS reduced for tractability, but the FFT/sub-frame size
|
||||
// remains 16 so the wrapper matches the real xfft_16 interface.
|
||||
// Includes full xfft_16 and fft_engine sub-modules.
|
||||
//
|
||||
// Focus: memory address bounds (highest-value finding) and state encoding.
|
||||
@@ -17,12 +18,12 @@ module fv_doppler_processor (
|
||||
input wire clk
|
||||
);
|
||||
|
||||
// Reduced parameters for tractable BMC
|
||||
localparam RANGE_BINS = 4;
|
||||
localparam CHIRPS_PER_FRAME = 4;
|
||||
localparam CHIRPS_PER_SUBFRAME = 2; // Dual sub-frame: 2 chirps per sub-frame
|
||||
localparam DOPPLER_FFT_SIZE = 2; // FFT size matches sub-frame size
|
||||
localparam MEM_DEPTH = RANGE_BINS * CHIRPS_PER_FRAME; // 16
|
||||
// Only RANGE_BINS is reduced; the FFT wrapper still expects 16 samples.
|
||||
localparam RANGE_BINS = 2;
|
||||
localparam CHIRPS_PER_FRAME = 32;
|
||||
localparam CHIRPS_PER_SUBFRAME = 16;
|
||||
localparam DOPPLER_FFT_SIZE = 16;
|
||||
localparam MEM_DEPTH = RANGE_BINS * CHIRPS_PER_FRAME;
|
||||
|
||||
// State encoding (mirrors DUT localparams)
|
||||
localparam S_IDLE = 3'b000;
|
||||
@@ -130,9 +131,11 @@ module fv_doppler_processor (
|
||||
assume(!data_valid);
|
||||
end
|
||||
|
||||
// new_chirp_frame must be a clean pulse (not during active processing)
|
||||
// new_chirp_frame may assert during accumulation at the 16-chirp boundary.
|
||||
// Only suppress it during FFT-processing states.
|
||||
always @(posedge clk) begin
|
||||
if (reset_n && state != S_IDLE)
|
||||
if (reset_n && (state == S_PRE_READ || state == S_LOAD_FFT ||
|
||||
state == S_FFT_WAIT || state == S_OUTPUT))
|
||||
assume(!new_chirp_frame);
|
||||
end
|
||||
|
||||
@@ -201,11 +204,17 @@ module fv_doppler_processor (
|
||||
end
|
||||
|
||||
// ================================================================
|
||||
// COVER 1: Complete processing of all range bins
|
||||
// COVER 1: Complete processing of all range bins after a full frame was
|
||||
// actually accumulated.
|
||||
// ================================================================
|
||||
reg f_seen_full;
|
||||
initial f_seen_full = 1'b0;
|
||||
always @(posedge clk)
|
||||
if (frame_buffer_full) f_seen_full <= 1'b1;
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (reset_n)
|
||||
cover(frame_complete && f_past_valid);
|
||||
cover(frame_complete && f_seen_full);
|
||||
end
|
||||
|
||||
// ================================================================
|
||||
|
||||
@@ -6,7 +6,7 @@ cover
|
||||
bmc: mode bmc
|
||||
bmc: depth 200
|
||||
cover: mode cover
|
||||
cover: depth 200
|
||||
cover: depth 600
|
||||
|
||||
[engines]
|
||||
smtbmc z3
|
||||
|
||||
@@ -66,13 +66,15 @@ module fv_radar_mode_controller (
|
||||
(* anyseq *) wire stm32_new_azimuth;
|
||||
(* anyseq *) wire trigger;
|
||||
|
||||
// Gap 2: Formal cfg_* inputs — solver-driven for exhaustive coverage
|
||||
(* anyseq *) wire [15:0] cfg_long_chirp_cycles;
|
||||
(* anyseq *) wire [15:0] cfg_long_listen_cycles;
|
||||
(* anyseq *) wire [15:0] cfg_guard_cycles;
|
||||
(* anyseq *) wire [15:0] cfg_short_chirp_cycles;
|
||||
(* anyseq *) wire [15:0] cfg_short_listen_cycles;
|
||||
(* anyseq *) wire [5:0] cfg_chirps_per_elev;
|
||||
// Runtime config inputs are pinned to the reduced localparams so this
|
||||
// wrapper proves one tractable configuration. It does not sweep the full
|
||||
// runtime-configurable cfg_* space.
|
||||
wire [15:0] cfg_long_chirp_cycles = LONG_CHIRP_CYCLES;
|
||||
wire [15:0] cfg_long_listen_cycles = LONG_LISTEN_CYCLES;
|
||||
wire [15:0] cfg_guard_cycles = GUARD_CYCLES;
|
||||
wire [15:0] cfg_short_chirp_cycles = SHORT_CHIRP_CYCLES;
|
||||
wire [15:0] cfg_short_listen_cycles = SHORT_LISTEN_CYCLES;
|
||||
wire [5:0] cfg_chirps_per_elev = CHIRPS_PER_ELEVATION;
|
||||
|
||||
// ================================================================
|
||||
// DUT outputs
|
||||
@@ -109,7 +111,8 @@ module fv_radar_mode_controller (
|
||||
.stm32_new_elevation(stm32_new_elevation),
|
||||
.stm32_new_azimuth (stm32_new_azimuth),
|
||||
.trigger (trigger),
|
||||
// Gap 2: Runtime-configurable timing inputs
|
||||
// Runtime-configurable timing ports, bound here to the reduced wrapper
|
||||
// constants for tractable proof depth.
|
||||
.cfg_long_chirp_cycles (cfg_long_chirp_cycles),
|
||||
.cfg_long_listen_cycles (cfg_long_listen_cycles),
|
||||
.cfg_guard_cycles (cfg_guard_cycles),
|
||||
@@ -181,7 +184,7 @@ module fv_radar_mode_controller (
|
||||
// ================================================================
|
||||
always @(posedge clk) begin
|
||||
if (reset_n && f_past_valid) begin
|
||||
if ($past(mode) == 2'b10 &&
|
||||
if ($past(mode) == 2'b10 && mode == 2'b10 &&
|
||||
$past(scan_state) == S_LONG_LISTEN &&
|
||||
$past(timer) == LONG_LISTEN_CYCLES - 1)
|
||||
assert(scan_state == S_IDLE);
|
||||
@@ -202,11 +205,11 @@ module fv_radar_mode_controller (
|
||||
end
|
||||
|
||||
// ================================================================
|
||||
// COVER 1: Full scan completes (scan_complete pulses)
|
||||
// COVER 1: Full auto-scan completes
|
||||
// ================================================================
|
||||
always @(posedge clk) begin
|
||||
if (reset_n)
|
||||
cover(scan_complete);
|
||||
cover(scan_complete && mode == 2'b01);
|
||||
end
|
||||
|
||||
// ================================================================
|
||||
|
||||
Reference in New Issue
Block a user