Mirrors/NawfalMotii79-PLFM_RADAR
1
0
Fork 0
mirror of https://github.com/NawfalMotii79/PLFM_RADAR.git synced 2026-06-10 15:31:21 +00:00
Code Issues Packages Projects Releases Wiki Activity

chirp-v2 PR-D: chirp_scheduler replaces radar_mode_controller; MF/MTI wave_sel-native

Browse Source 
Single 100 MHz scheduler emits wave_sel[1:0] and chirp_pulse natively. Modes
00 (STM32 pass-through), 01 (auto-scan over SHORT/MEDIUM/LONG sub-frames),
10 (single-chirp debug), 11 (track dwell with watchdog scan-fallback after
RP_DEF_TRACK_WATCHDOG_FRAMES=5 idle frames). Sub-frame mask lets ops drop a
waveform without recompiling.

Drops the receiver_final wave_sel shim added in PR-C: wave_sel comes
straight from the scheduler; chirp_pulse replaces the old mc_new_chirp
toggle + XOR edge converter. matched_filter_multi_segment and mti_canceller
take wave_sel[1:0] and chirp_pulse directly — no parallel paths.

multi_segment also bumped: SHORT_CHIRP_SAMPLES 50 -> 100 (V2 1 us SHORT)
and MEDIUM_CHIRP_SAMPLES = 500 (5 us). LONG path unchanged. Dead
mc_new_elevation/azimuth XOR converters removed.

Deletes radar_mode_controller.v, formal/fv_radar_mode_controller.v, and
tb/tb_radar_mode_controller.v. Build manifests (run_regression.sh,
scripts/200t/build_200t.tcl) updated. Receiver_final pins medium/track/
subframe_enable inputs to RP_DEF_* defaults until PR-G plumbs USB opcodes.

Verification:
- tb_rxb_fullchain_latency: peak |I|+|Q|=24033 at bin 0, ~80x peak/mean
  (up from PR-C's 15115 since matched filter now uses full 100 SHORT samples)
- tb_mti_canceller: 43/43 PASS with new wave_sel[1:0] input
- tb_radar_receiver_final: 8/8 PASS, ALL TESTS PASSED
- tb_system_e2e: 34/49 PASS - identical to pre-PR-D baseline (15 failures
  are pre-existing matched-filter cycle-budget skips); G8.2/G8.3 chirp_scheduler
  probes PASS
- tb_multiseg_cosim: 16/32 - same as pre-PR-D baseline
This commit is contained in:
Jason
2026-04-30 20:52:32 +05:45
parent 4238eb1b99
commit 8e8f3e60c4
15 changed files with 666 additions and 1718 deletions
Download Patch File Download Diff File Expand all files Collapse all files
9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v
-232
View File
@@ -1,232 +0,0 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: radar_mode_controller
// AERIS-10 Radar FPGA — 7-state beam scan FSM
// Target: SymbiYosys with smtbmc/z3
//
// Single-clock design: clk is an input wire, async2sync handles async reset.
// Each formal step = one clock edge.
//
// Timer parameters reduced to small values to keep BMC tractable.
// ============================================================================
module fv_radar_mode_controller (
input wire clk
);
// Reduced parameters for tractable BMC
localparam LONG_CHIRP_CYCLES = 5;
localparam LONG_LISTEN_CYCLES = 5;
localparam GUARD_CYCLES = 5;
localparam SHORT_CHIRP_CYCLES = 3;
localparam SHORT_LISTEN_CYCLES = 3;
localparam CHIRPS_PER_ELEVATION = 3;
localparam ELEVATIONS_PER_AZIMUTH = 2;
localparam AZIMUTHS_PER_SCAN = 2;
// Maximum timer value across all phases
localparam MAX_TIMER = LONG_CHIRP_CYCLES; // 5 (largest)
// State encoding (mirrors DUT localparams)
localparam S_IDLE = 3'd0;
localparam S_LONG_CHIRP = 3'd1;
localparam S_LONG_LISTEN = 3'd2;
localparam S_GUARD = 3'd3;
localparam S_SHORT_CHIRP = 3'd4;
localparam S_SHORT_LISTEN = 3'd5;
localparam S_ADVANCE = 3'd6;
`ifdef FORMAL
// ================================================================
// Clock is an input wire — smtbmc drives it automatically.
// async2sync (in .sby, default) converts async reset to sync.
// ================================================================
// ================================================================
// Past-valid tracker (for guarding $past usage)
// ================================================================
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge clk) f_past_valid <= 1'b1;
// ================================================================
// Reset: asserted (low) for cycle 0, deasserted from cycle 1
// ================================================================
reg reset_n;
initial reset_n = 1'b0;
always @(posedge clk) reset_n <= 1'b1;
// ================================================================
// DUT inputs — solver-driven each cycle
// ================================================================
(* anyseq *) wire [1:0] mode;
(* anyseq *) wire stm32_new_chirp;
(* anyseq *) wire stm32_new_elevation;
(* anyseq *) wire stm32_new_azimuth;
(* anyseq *) wire trigger;
// 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
// ================================================================
wire use_long_chirp;
wire mc_new_chirp;
wire mc_new_elevation;
wire mc_new_azimuth;
wire [5:0] chirp_count;
wire [5:0] elevation_count;
wire [5:0] azimuth_count;
wire scanning;
wire scan_complete;
wire [2:0] scan_state;
wire [17:0] timer;
// ================================================================
// DUT instantiation
// ================================================================
radar_mode_controller #(
.CHIRPS_PER_ELEVATION (CHIRPS_PER_ELEVATION),
.ELEVATIONS_PER_AZIMUTH (ELEVATIONS_PER_AZIMUTH),
.AZIMUTHS_PER_SCAN (AZIMUTHS_PER_SCAN),
.LONG_CHIRP_CYCLES (LONG_CHIRP_CYCLES),
.LONG_LISTEN_CYCLES (LONG_LISTEN_CYCLES),
.GUARD_CYCLES (GUARD_CYCLES),
.SHORT_CHIRP_CYCLES (SHORT_CHIRP_CYCLES),
.SHORT_LISTEN_CYCLES (SHORT_LISTEN_CYCLES)
) dut (
.clk (clk),
.reset_n (reset_n),
.mode (mode),
.stm32_new_chirp (stm32_new_chirp),
.stm32_new_elevation(stm32_new_elevation),
.stm32_new_azimuth (stm32_new_azimuth),
.trigger (trigger),
// 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),
.cfg_short_chirp_cycles (cfg_short_chirp_cycles),
.cfg_short_listen_cycles(cfg_short_listen_cycles),
.cfg_chirps_per_elev (cfg_chirps_per_elev),
.use_long_chirp (use_long_chirp),
.mc_new_chirp (mc_new_chirp),
.mc_new_elevation (mc_new_elevation),
.mc_new_azimuth (mc_new_azimuth),
.chirp_count (chirp_count),
.elevation_count (elevation_count),
.azimuth_count (azimuth_count),
.scanning (scanning),
.scan_complete (scan_complete),
.fv_scan_state (scan_state),
.fv_timer (timer)
);
// scan_state and timer are now accessed via formal output ports
// ================================================================
// PROPERTY 1: State encoding — state 7 is unreachable
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(scan_state <= 3'd6);
end
// ================================================================
// PROPERTY 2: Counter bounds
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
assert(chirp_count < CHIRPS_PER_ELEVATION);
assert(elevation_count < ELEVATIONS_PER_AZIMUTH);
assert(azimuth_count < AZIMUTHS_PER_SCAN);
end
end
// ================================================================
// PROPERTY 3: Timer bound
// Timer must never reach or exceed the maximum timer parameter.
// The timer counts from 0 to (PARAM - 1) before resetting.
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(timer < MAX_TIMER);
end
// ================================================================
// PROPERTY 4: Mode coherence
// In S_LONG_CHIRP / S_LONG_LISTEN, use_long_chirp must be 1.
// In S_SHORT_CHIRP / S_SHORT_LISTEN, use_long_chirp must be 0.
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
if (scan_state == S_LONG_CHIRP || scan_state == S_LONG_LISTEN)
assert(use_long_chirp == 1'b1);
if (scan_state == S_SHORT_CHIRP || scan_state == S_SHORT_LISTEN)
assert(use_long_chirp == 1'b0);
end
end
// ================================================================
// PROPERTY 5: Single-chirp returns to idle
// In mode 2'b10, after S_LONG_LISTEN completes (timer reaches
// max), scan_state returns to S_IDLE.
// ================================================================
always @(posedge clk) begin
if (reset_n && f_past_valid) begin
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);
end
end
// ================================================================
// PROPERTY 6: Auto-scan never stalls in S_IDLE
// In mode 2'b01, if the FSM is in S_IDLE on one cycle it must
// leave S_IDLE on the very next cycle.
// ================================================================
always @(posedge clk) begin
if (reset_n && f_past_valid) begin
if ($past(mode) == 2'b01 && $past(scan_state) == S_IDLE &&
$past(reset_n) && mode == 2'b01)
assert(scan_state != S_IDLE);
end
end
// ================================================================
// COVER 1: Full auto-scan completes
// ================================================================
always @(posedge clk) begin
if (reset_n)
cover(scan_complete && mode == 2'b01);
end
// ================================================================
// COVER 2: Each state is reachable
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
cover(scan_state == S_IDLE);
cover(scan_state == S_LONG_CHIRP);
cover(scan_state == S_LONG_LISTEN);
cover(scan_state == S_GUARD);
cover(scan_state == S_SHORT_CHIRP);
cover(scan_state == S_SHORT_LISTEN);
cover(scan_state == S_ADVANCE);
end
end
`endif // FORMAL
endmodule