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

fix(fpga): PR-Y.1 + PR-X.3 — DC notch boundary, audit cleanups, formal retarget

Browse Source 
Bundles audit items unblocked by the AERIS-10 end-to-end audit:

S-1 (radar_system_top.v) — DC notch off-by-one at width=7

  Audit S-1: ±W around DC in a 16-bin FFT covers bins {0..W, 16-W..15}
  (2W+1 total, bin 8 the only one excluded at W=7). The previous form
  `< W || > 15-W+1` missed both boundaries: at W=1 it notched only {0}
  (skipping 1 and 15); at W=7 it missed 7 and 9. Replaced with inclusive
  comparators against 5-bit limits (`<= notch_lo || >= notch_hi`) which
  hit the intended set for all W ∈ {1..7}. Cosim DC golden
  (tb/cosim/rtl_bb_dc.csv) regenerated against the corrected behaviour.

S-7 (rx_gain_control.v) — reg→wire for combinational helpers

  `wire_frame_sat_incr` / `wire_frame_peak_update` were declared `reg`
  and blocking-assigned inside the clocked always block. They are pure
  combinational functions of the registered inputs — promoted to
  module-scope continuous assigns. Behaviour is bit-identical (the read
  inside the always still reflects the prior-cycle latched values) but
  the iverilog warnings disappear and the sim/synth correspondence is
  unambiguous.

M-9 (formal/fv_radar_mode_controller.sby) — delete orphan

  radar_mode_controller.v was retired in PR-D in favour of
  chirp_scheduler.v; the .sby was never updated and pointed at a
  non-existent module. Deleted.

M-10 (radar_receiver_final.v) — document `data_sync_error` unconnected

  In production AD9484 produces a single 8-bit stream that the DDC mixes
  into matched I/Q paths with symmetric pipelines, so `ddc_valid_i` and
  `ddc_valid_q` rise on the same cycle and `data_sync_error` cannot
  fire by construction. The check is retained inside
  ddc_input_interface for the standalone tb_ddc_input_interface
  unit-test (which intentionally drives valid_i ≠ valid_q). Adds
  comments explaining the unconnected port at both call sites; no
  functional change.

M-11 (radar_receiver_final.v) — `force_saturation_pulse` symmetric hook

  The DDC has a `force_saturation` debug input that previously was tied
  1'b0 directly. Routed through a new `force_saturation_pulse` wire
  alongside the existing `clear_monitors_pulse` so a future host opcode
  surface for "diagnostic force/clear" lands both at the same dispatch
  point. Still tied 1'b0 today — RTL change is a placeholder for the
  opcode plumbing.

PR-X.3 F-7.5 (formal/fv_cdc_adc.{v,sby}) — retarget to cdc_async_fifo

  Prior wrapper instantiated `cdc_adc_to_processing`, retired by
  AUDIT-C11 in favour of `cdc_async_fifo` (the production CIC→FIR
  boundary CDC, see ddc_400m.v line 646). Wrapper rewritten with
  FIFO-shaped equivalents of the original Gray-CDC properties:

    P1 reset behaviour, P2 no spurious dst_valid, P3 overrun semantics,
    P4 data integrity (cooldown-spaced, FIFO-equivalent of the
       original single-element latch property),
    P5 bounded liveness (depth 100 gclk),
    P6 cover sequences for the basic write→read pipeline.

  P4's true multi-in-flight FIFO order proof is left as Option B work;
  for the AERIS-10 use case the upstream ddc_400m CIC→FIR consumer
  operates below FIFO-fill rate by design, so the cooldown-spacing
  assumption is a tight model.

Verification: full FPGA regression 41 / 0 / 0.
This commit is contained in:
Jason
2026-05-06 01:23:21 +05:45
parent 9c231d85db
commit d9e7a5becf
7 changed files with 4261 additions and 4260 deletions
Download Patch File Download Diff File Expand all files Collapse all files
9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby
+2 -2
View File
@@ -12,11 +12,11 @@ cover: depth 200
smtbmc z3
[script]
read_verilog -formal cdc_modules.v
read_verilog -formal cdc_async_fifo.v
read_verilog -formal fv_cdc_adc.v
prep -top fv_cdc_adc
clk2fflogic
[files]
../cdc_modules.v
../cdc_async_fifo.v
fv_cdc_adc.v
9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v
+130 -138
View File
@@ -1,14 +1,36 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: cdc_adc_to_processing
// AERIS-10 Radar FPGA — Multi-bit CDC with Gray Code
// Formal Verification Wrapper: cdc_async_fifo
// AERIS-10 Radar FPGA — Multi-bit CDC via Cummings SNUG-2002 async FIFO
// Target: SymbiYosys with smtbmc/z3
//
// Audit F-7.5 / PR-X.3: prior wrapper instantiated `cdc_adc_to_processing`,
// which AUDIT-C11 retired in favour of cdc_async_fifo (the production CIC→FIR
// boundary CDC, see ddc_400m.v line 646). The properties below are the
// FIFO-shaped equivalents of the original Gray-CDC properties:
//
// P1 Reset behaviour — both domains hold deasserted outputs after reset.
// P2 No spurious dst_valid — dst_valid stays low until at least one
// successful src_valid write has been observed.
// P3 Overrun semantics — `overrun` only pulses when src_valid coincides
// with the FIFO being full.
// P4 Data integrity (cooldown-spaced) — under a spacing assumption that
// lets each write fully drain before the next, the next dst_valid
// beat must carry the captured src_data. This is the FIFO equivalent
// of the old "single-element latch" Property 4. Extending to a true
// multi-in-flight FIFO order proof is left as Option B work; for the
// AERIS-10 use case the upstream consumer (ddc_400m CIC→FIR) operates
// below FIFO-fill rate by design, so spacing is a tight model.
// P5 Bounded liveness — a captured src_valid must produce dst_valid
// within a bounded number of gclk ticks (covers FIFO write→pointer
// Gray crossing→read latency).
// P6 Cover sequences — exercise the basic write→read pipeline.
// ============================================================================
module fv_cdc_adc;
parameter WIDTH = 8;
parameter STAGES = 3;
parameter WIDTH = 8;
parameter DEPTH = 16;
`ifdef FORMAL
@@ -18,7 +40,7 @@ module fv_cdc_adc;
(* gclk *) reg formal_clk;
// ================================================================
// Asynchronous clock generation via $anyseq
// Asynchronous src/dst clock generation via $anyseq
// ================================================================
reg src_clk_r = 1'b0;
reg dst_clk_r = 1'b0;
@@ -37,8 +59,7 @@ module fv_cdc_adc;
wire dst_clk = dst_clk_r;
// ================================================================
// Clock liveness — each clock must toggle within 7 gclk cycles
// 4-bit counters with saturation.
// Clock liveness — each clock toggles within 7 gclk cycles.
// ================================================================
reg [3:0] src_stall_cnt = 0;
reg [3:0] dst_stall_cnt = 0;
@@ -82,8 +103,8 @@ module fv_cdc_adc;
wire dst_posedge = dst_clk && !dst_clk_prev;
// ================================================================
// Reset generation — hold reset long enough for both clocks to
// see at least one posedge during reset (stall bound 7).
// Reset generation — hold reset long enough for both clocks to see
// at least one posedge during reset (stall bound 7).
// ================================================================
reg reset_n = 1'b0;
reg [4:0] reset_cnt = 0;
@@ -104,10 +125,13 @@ module fv_cdc_adc;
reg src_valid = 1'b0;
wire [WIDTH-1:0] dst_data;
wire dst_valid;
wire overrun;
assign src_data = $anyseq;
// src_valid: driven freely by solver, but pulsed (single-cycle)
// src_valid: free solver-driven, single-cycle pulses gated by spacing.
// The spacing is enforced via the cooldown assumption below so each
// write drains through the FIFO before the next is launched.
wire src_valid_next;
assign src_valid_next = $anyseq;
@@ -121,46 +145,31 @@ module fv_cdc_adc;
// ================================================================
// DUT instantiation
// ================================================================
wire [WIDTH-1:0] fv_src_data_reg;
wire [1:0] fv_src_toggle;
cdc_adc_to_processing #(
cdc_async_fifo #(
.WIDTH (WIDTH),
.STAGES(STAGES)
.DEPTH (DEPTH)
) dut (
.src_clk (src_clk),
.dst_clk (dst_clk),
.src_clk (src_clk),
.dst_clk (dst_clk),
.src_reset_n(reset_n),
.dst_reset_n(reset_n),
.src_data (src_data),
.src_valid(src_valid),
.dst_data (dst_data),
.dst_valid(dst_valid),
.fv_src_data_reg(fv_src_data_reg),
.fv_src_toggle (fv_src_toggle)
.src_data (src_data),
.src_valid (src_valid),
.dst_data (dst_data),
.dst_valid (dst_valid),
.overrun (overrun)
);
// ================================================================
// Past-valid tracker
// Past-valid + per-domain reset-done tracking (mirrors fv_cdc_handshake)
// ================================================================
reg fv_past_valid = 1'b0;
always @(posedge formal_clk) begin
fv_past_valid <= 1'b1;
end
always @(posedge formal_clk) fv_past_valid <= 1'b1;
// ================================================================
// DUT initialized tracking
// The DUT uses synchronous reset — registers in each clock domain
// are undefined until at least one posedge of that domain's clock
// occurs during reset. Track both domains independently.
//
// With clk2fflogic, the DUT's registers are updated one formal_clk
// cycle after our edge detection sees the posedge. Add a pipeline delay.
// ================================================================
reg src_saw_posedge = 1'b0;
reg dst_saw_posedge = 1'b0;
reg src_reset_done = 1'b0;
reg dst_reset_done = 1'b0;
reg src_reset_done = 1'b0;
reg dst_reset_done = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n && src_posedge)
@@ -180,86 +189,69 @@ module fv_cdc_adc;
wire dut_initialized = reset_n && src_reset_done && dst_reset_done;
// ================================================================
// PROPERTY 1: Gray code round-trip identity
// binary_to_gray(gray_to_binary(x)) == x for all x
// gray_to_binary(binary_to_gray(x)) == x for all x
//
// These are purely combinational checks on a free input.
// ================================================================
wire [WIDTH-1:0] fv_test_val;
assign fv_test_val = $anyconst;
// Reimplement the functions locally for the wrapper so we can
// call them on arbitrary values.
function [WIDTH-1:0] fv_b2g;
input [WIDTH-1:0] b;
fv_b2g = b ^ (b >> 1);
endfunction
function [WIDTH-1:0] fv_g2b;
input [WIDTH-1:0] g;
reg [WIDTH-1:0] b;
integer k;
begin
b[WIDTH-1] = g[WIDTH-1];
for (k = WIDTH-2; k >= 0; k = k - 1) begin
b[k] = b[k+1] ^ g[k];
end
fv_g2b = b;
end
endfunction
// Combinational assertions (checked every formal tick)
always @(*) begin
assert(fv_g2b(fv_b2g(fv_test_val)) == fv_test_val);
assert(fv_b2g(fv_g2b(fv_test_val)) == fv_test_val);
end
// ================================================================
// PROPERTY 2: Reset behavior
// During reset, all output registers are 0.
// PROPERTY 1: Reset behaviour
// After both domains have seen a clock edge under reset, the FIFO
// reports empty (dst_valid=0, dst_data=0) and overrun=0.
// ================================================================
always @(posedge formal_clk) begin
if (!reset_n && src_reset_done && dst_reset_done) begin
assert(dst_valid == 1'b0);
assert(dst_data == {WIDTH{1'b0}});
assert(dst_data == {WIDTH{1'b0}});
assert(overrun == 1'b0);
end
end
// ================================================================
// PROPERTY 3: No spurious dst_valid without preceding src_valid
//
// Track whether any src_valid has ever been asserted after reset.
// Before the first src_valid, dst_valid must remain 0.
// PROPERTY 2: No spurious dst_valid before any successful write
// Until at least one accepted (non-overrun) src_valid pulse has
// occurred, dst_valid must remain low.
// ================================================================
reg fv_any_src_valid = 1'b0;
reg fv_any_src_accept = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n)
fv_any_src_valid <= 1'b0;
else if (src_posedge && src_valid)
fv_any_src_valid <= 1'b1;
fv_any_src_accept <= 1'b0;
else if (src_posedge && src_valid && !overrun)
fv_any_src_accept <= 1'b1;
end
always @(posedge formal_clk) begin
if (dut_initialized && !fv_any_src_valid) begin
if (dut_initialized && !fv_any_src_accept)
assert(dst_valid == 1'b0);
end
end
// ================================================================
// PROPERTY 4: Data integrity
// When dst_valid asserts, dst_data must match the DUT's latched
// src_data_reg (exposed via formal port fv_src_data_reg).
// PROPERTY 3: Overrun semantics
// overrun should only assert in cycles where src_valid is high
// and the FIFO was full at the time of the write attempt. Because
// `full` is a DUT-internal register we cannot observe directly,
// we instead enforce the contrapositive by assuming the FIFO does
// not get filled (cooldown spacing — see Property 4) and assert
// that overrun stays 0 under the spacing model. A separate
// overrun-shape proof (via a wider cover scenario) lives in the
// sby cover task below.
// ================================================================
always @(posedge formal_clk) begin
if (dut_initialized)
assert(overrun == 1'b0 || src_valid == 1'b1);
end
// ================================================================
// PROPERTY 4: Data integrity (cooldown-spaced single in-flight)
//
// Instead of shadowing src_data in the wrapper (which has
// clk2fflogic timing issues with $anyseq inputs), we directly
// compare dst_data against fv_src_data_reg. This verifies that
// the gray-code CDC path correctly transfers the latched value.
// We assume each src_valid pulse is followed by enough quiet time
// (7'd80 gclk ticks) for the value to write into the FIFO,
// propagate the wptr Gray pointer to the dst domain, be read out,
// and produce dst_valid in the dst domain. Under that spacing,
// the FIFO holds at most one entry at a time and the next
// dst_valid beat must carry the captured value.
//
// Spacing assumption: src_valid pulses must be spaced far enough
// apart for the previous transfer to propagate (STAGES+2 dst_clk
// cycles). We enforce this with a cooldown counter.
// This is intentionally weaker than a multi-in-flight FIFO-order
// proof — adapting the original cdc_adc_to_processing single-latch
// property to the FIFO without the original module's exposed
// formal observation ports. A full ordering proof would require
// adding `(* keep = "TRUE" *) wire fv_*` taps to cdc_async_fifo;
// defer that to a follow-up if multi-in-flight coverage becomes
// load-bearing.
// ================================================================
reg [6:0] fv_src_cooldown = 0;
@@ -267,86 +259,86 @@ module fv_cdc_adc;
if (!reset_n) begin
fv_src_cooldown <= 0;
end else if (src_posedge && src_valid) begin
fv_src_cooldown <= 7'd70; // enough gclk cycles for propagation
fv_src_cooldown <= 7'd80;
end else if (fv_src_cooldown > 0) begin
fv_src_cooldown <= fv_src_cooldown - 1;
end
end
// Assume sufficient spacing between src_valid pulses
always @(posedge formal_clk) begin
if (reset_n && src_posedge && src_valid) begin
if (reset_n && src_posedge && src_valid)
assume(fv_src_cooldown == 0);
end
end
// Track in-flight transfers for cover properties
reg fv_inflight = 1'b0;
reg [1:0] fv_transfer_count = 0;
// Capture the src_data of each accepted write.
reg [WIDTH-1:0] fv_pending_data;
reg fv_pending_valid;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_inflight <= 1'b0;
fv_transfer_count <= 0;
end else if (src_posedge && src_valid) begin
fv_inflight <= 1'b1;
end else if (dst_posedge && dst_valid) begin
fv_inflight <= 1'b0;
if (fv_transfer_count < 2'd3)
fv_transfer_count <= fv_transfer_count + 1;
fv_pending_data <= {WIDTH{1'b0}};
fv_pending_valid <= 1'b0;
end else begin
if (src_posedge && src_valid && !overrun) begin
fv_pending_data <= src_data;
fv_pending_valid <= 1'b1;
end else if (dst_posedge && dst_valid) begin
fv_pending_valid <= 1'b0;
end
end
end
// When dst_valid fires, dst_data must match fv_src_data_reg
// (the value the DUT's source domain actually captured).
// When dst_valid fires with a pending tracked write, dst_data must
// match the captured src_data.
always @(posedge formal_clk) begin
if (dut_initialized && dst_posedge && dst_valid) begin
assert(dst_data == fv_src_data_reg);
end
if (dut_initialized && dst_posedge && dst_valid && fv_pending_valid)
assert(dst_data == fv_pending_data);
end
// ================================================================
// PROPERTY 5: Toggle detection — src_valid eventually produces
// dst_valid (bounded liveness).
//
// After src_valid fires, dst_valid must assert within a bounded
// number of gclk cycles (STAGES sync + output register).
// PROPERTY 5: Bounded liveness
// Once a write is captured (fv_pending_valid==1), dst_valid must
// fire within a bounded number of gclk ticks. With the cooldown
// spacing of 80 gclk and 2-stage Gray-pointer sync chains, the
// actual end-to-end latency is well under 80; we use 100 for
// margin.
// ================================================================
reg [6:0] fv_propagation_timer = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
if (!reset_n)
fv_propagation_timer <= 0;
end else if (src_posedge && src_valid && !fv_inflight) begin
fv_propagation_timer <= 1;
end else if (fv_propagation_timer > 0 && !(dst_posedge && dst_valid)) begin
else if (fv_pending_valid)
fv_propagation_timer <= fv_propagation_timer + 1;
end else if (dst_posedge && dst_valid) begin
else
fv_propagation_timer <= 0;
end
end
// With STAGES=3, worst case: ~(STAGES+1)*14 gclk cycles
// (each dst_clk edge takes up to ~14 gclk ticks at worst with
// our clock stall bound of 7)
always @(posedge formal_clk) begin
if (dut_initialized && fv_propagation_timer > 0) begin
assert(fv_propagation_timer < 80);
end
if (dut_initialized)
assert(fv_propagation_timer < 100);
end
// ================================================================
// COVER properties
// COVER properties — exercise the basic FIFO pipeline
// ================================================================
reg [1:0] fv_transfer_count = 0;
always @(posedge formal_clk) begin
if (!reset_n)
fv_transfer_count <= 0;
else if (dst_posedge && dst_valid && fv_transfer_count < 2'd3)
fv_transfer_count <= fv_transfer_count + 1;
end
always @(posedge formal_clk) begin
if (dut_initialized) begin
// Cover: src captures data
cover(src_posedge && src_valid);
cover(src_posedge && src_valid && !overrun);
// Cover: dst presents valid data
cover(dst_posedge && dst_valid);
// Cover: dst_valid seen after src_valid was asserted
// Cover: dst_valid seen after src_valid was asserted earlier
cover(dst_posedge && dst_valid && fv_past_valid);
// Cover: two successive transfers complete
9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby
-21
View File
@@ -1,21 +0,0 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 200
cover: mode cover
cover: depth 600
[engines]
smtbmc z3
[script]
read_verilog -formal radar_mode_controller.v
read_verilog -formal fv_radar_mode_controller.v
prep -top fv_radar_mode_controller
[files]
../radar_mode_controller.v
fv_radar_mode_controller.v