FlintyLemming/PLFM_RADAR
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add SymbiYosys formal verification for 6 modules, fix 2 doppler bugs

Browse Source 
Formal verification (SymbiYosys + smtbmc/z3):
- cdc_single_bit: BMC PASS depth 80, cover PASS 3/3
- cdc_handshake: BMC PASS depth 100, cover PASS 4/4
- cdc_adc_to_processing: BMC PASS depth 80, cover PASS
- radar_mode_controller: BMC PASS depth 200, cover PASS 8/8
- range_bin_decimator: cover PASS 7/7, BMC running (step 61+)
- doppler_processor: cover running (step 133/150), BMC running (step 35+)

DUT bug fixes found by formal:
- doppler_processor: write_chirp_index overflow past CHIRPS_PER_FRAME-1
  in S_ACCUMULATE frame-complete branch (reset to 0)
- doppler_processor: read_doppler_index unclamped prefetch in S_LOAD_FFT
  causing OOB BRAM reads (clamped to DOPPLER_FFT_SIZE-1)

CDC fix (prior session, included):
- cdc_modules: async reset changed to sync reset on all CDC sync chains
  to prevent metastability on reset deassertion

RTL changes for formal observability:
- Added ifdef FORMAL output ports to cdc_handshake (6), cdc_adc (2),
  radar_mode_controller (2), range_bin_decimator (5), doppler_processor (11)
This commit is contained in:
Jason
2026-03-17 12:47:22 +02:00
parent a9c857c447
commit fb59e98737
17 changed files with 1979 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files
9_Firmware/9_2_FPGA/cdc_modules.v
+38 -9
View File
@@ -17,6 +17,10 @@ module cdc_adc_to_processing #(
input wire src_valid,
output wire [WIDTH-1:0] dst_data,
output wire dst_valid
`ifdef FORMAL
,output wire [WIDTH-1:0] fv_src_data_reg,
output wire [1:0] fv_src_toggle
`endif
);
// Gray encoding for safe CDC
@@ -50,8 +54,8 @@ module cdc_adc_to_processing #(
reg dst_valid_reg = 0;
reg [1:0] prev_dst_toggle = 2'b00;
// Source domain: capture data and toggle
always @(posedge src_clk or negedge reset_n) begin
// Source domain: capture data and toggle — synchronous reset
always @(posedge src_clk) begin
if (!reset_n) begin
src_data_reg <= 0;
src_toggle <= 2'b00;
@@ -97,8 +101,8 @@ module cdc_adc_to_processing #(
end
endgenerate
// Detect new data
always @(posedge dst_clk or negedge reset_n) begin
// Detect new data — synchronous reset
always @(posedge dst_clk) begin
if (!reset_n) begin
dst_data_reg <= 0;
dst_valid_reg <= 0;
@@ -120,10 +124,17 @@ module cdc_adc_to_processing #(
assign dst_data = dst_data_reg;
assign dst_valid = dst_valid_reg;
`ifdef FORMAL
assign fv_src_data_reg = src_data_reg;
assign fv_src_toggle = src_toggle;
`endif
endmodule
// ============================================================================
// CDC FOR SINGLE BIT SIGNALS
// Uses synchronous reset on sync chain to avoid metastability on reset
// deassertion. Matches cdc_adc_to_processing best practice.
// ============================================================================
module cdc_single_bit #(
parameter STAGES = 3
@@ -137,7 +148,7 @@ module cdc_single_bit #(
(* ASYNC_REG = "TRUE" *) reg [STAGES-1:0] sync_chain;
always @(posedge dst_clk or negedge reset_n) begin
always @(posedge dst_clk) begin
if (!reset_n) begin
sync_chain <= 0;
end else begin
@@ -151,6 +162,7 @@ endmodule
// ============================================================================
// CDC FOR MULTI-BIT WITH HANDSHAKE
// Uses synchronous reset to avoid metastability on reset deassertion.
// ============================================================================
module cdc_handshake #(
parameter WIDTH = 32
@@ -164,6 +176,14 @@ module cdc_handshake #(
output wire [WIDTH-1:0] dst_data,
output wire dst_valid,
input wire dst_ready
`ifdef FORMAL
,output wire fv_src_busy,
output wire fv_dst_ack,
output wire fv_dst_req_sync,
output wire [1:0] fv_src_ack_sync_chain,
output wire [1:0] fv_dst_req_sync_chain,
output wire [WIDTH-1:0] fv_src_data_reg_hs
`endif
);
// Source domain
@@ -179,8 +199,17 @@ module cdc_handshake #(
(* ASYNC_REG = "TRUE" *) reg [1:0] dst_req_sync_chain = 2'b00;
reg dst_ack = 0;
// Source clock domain
always @(posedge src_clk or negedge reset_n) begin
`ifdef FORMAL
assign fv_src_busy = src_busy;
assign fv_dst_ack = dst_ack;
assign fv_dst_req_sync = dst_req_sync;
assign fv_src_ack_sync_chain = src_ack_sync_chain;
assign fv_dst_req_sync_chain = dst_req_sync_chain;
assign fv_src_data_reg_hs = src_data_reg;
`endif
// Source clock domain — synchronous reset
always @(posedge src_clk) begin
if (!reset_n) begin
src_data_reg <= 0;
src_busy <= 0;
@@ -200,8 +229,8 @@ module cdc_handshake #(
end
end
// Destination clock domain
always @(posedge dst_clk or negedge reset_n) begin
// Destination clock domain — synchronous reset
always @(posedge dst_clk) begin
if (!reset_n) begin
dst_data_reg <= 0;
dst_valid_reg <= 0;
9_Firmware/9_2_FPGA/doppler_processor.v
+44 -1
View File
@@ -19,6 +19,21 @@ module doppler_processor_optimized #(
output wire processing_active,
output wire frame_complete,
output reg [3:0] status
`ifdef FORMAL
,
output wire [2:0] fv_state,
output wire [10:0] fv_mem_write_addr,
output wire [10:0] fv_mem_read_addr,
output wire [5:0] fv_write_range_bin,
output wire [4:0] fv_write_chirp_index,
output wire [5:0] fv_read_range_bin,
output wire [4:0] fv_read_doppler_index,
output wire [9:0] fv_processing_timeout,
output wire fv_frame_buffer_full,
output wire fv_mem_we,
output wire [10:0] fv_mem_waddr_r
`endif
);
// ==============================================
@@ -139,6 +154,20 @@ reg [DATA_WIDTH-1:0] mem_wdata_i, mem_wdata_q;
// Memory read data (registered for BRAM read latency)
reg [DATA_WIDTH-1:0] mem_rdata_i, mem_rdata_q;
`ifdef FORMAL
assign fv_state = state;
assign fv_mem_write_addr = mem_write_addr;
assign fv_mem_read_addr = mem_read_addr;
assign fv_write_range_bin = write_range_bin;
assign fv_write_chirp_index = write_chirp_index;
assign fv_read_range_bin = read_range_bin;
assign fv_read_doppler_index = read_doppler_index;
assign fv_processing_timeout = processing_timeout;
assign fv_frame_buffer_full = frame_buffer_full;
assign fv_mem_we = mem_we;
assign fv_mem_waddr_r = mem_waddr_r;
`endif
// ----------------------------------------------------------
// Separate always block for memory writes — NO async reset
// in sensitivity list, so Vivado can infer Block RAM.
@@ -242,6 +271,12 @@ always @(posedge clk or negedge reset_n) begin
read_range_bin <= 0;
read_doppler_index <= 0;
fft_sample_counter <= 0;
// Reset write pointers — no longer needed for
// this frame, and prevents stale overflow of
// write_chirp_index (which was just incremented
// past CHIRPS_PER_FRAME-1 above).
write_chirp_index <= 0;
write_range_bin <= 0;
end
end
end
@@ -302,7 +337,8 @@ always @(posedge clk or negedge reset_n) begin
// Present BRAM addr for chirp 2 (sub=1 reads chirp 1
// from the BRAM read we triggered in S_PRE_READ;
// we need chirp 2 ready for sub=2).
read_doppler_index <= 2;
read_doppler_index <= (2 < DOPPLER_FFT_SIZE) ? 2
: DOPPLER_FFT_SIZE - 1;
fft_sample_counter <= 1;
end else if (fft_sample_counter <= DOPPLER_FFT_SIZE) begin
// Sub 1..32
@@ -317,6 +353,9 @@ always @(posedge clk or negedge reset_n) begin
state <= S_FFT_WAIT;
fft_sample_counter <= 0;
processing_timeout <= 1000;
// Reset read index to prevent stale OOB address
// on BRAM read port during S_FFT_WAIT
read_doppler_index <= 0;
end else begin
// Sub 1..31: also compute new mult from current BRAM data
// mem_rdata_i = data[chirp = fft_sample_counter][rbin]
@@ -326,7 +365,11 @@ always @(posedge clk or negedge reset_n) begin
$signed(window_coeff[fft_sample_counter]);
// Advance BRAM read to chirp fft_sample_counter+2
// (so data is ready two cycles later when we need it)
// Clamp to DOPPLER_FFT_SIZE-1 to prevent OOB memory read
if (fft_sample_counter + 2 < DOPPLER_FFT_SIZE)
read_doppler_index <= fft_sample_counter + 2;
else
read_doppler_index <= DOPPLER_FFT_SIZE - 1;
fft_sample_counter <= fft_sample_counter + 1;
end
end
9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby
+22
View File
@@ -0,0 +1,22 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 80
cover: mode cover
cover: depth 200
[engines]
smtbmc z3
[script]
read_verilog -formal cdc_modules.v
read_verilog -formal fv_cdc_adc.v
prep -top fv_cdc_adc
clk2fflogic
[files]
../cdc_modules.v
fv_cdc_adc.v
9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v
+358
View File
@@ -0,0 +1,358 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: cdc_adc_to_processing
// AERIS-10 Radar FPGA — Multi-bit CDC with Gray Code
// Target: SymbiYosys with smtbmc/z3
// ============================================================================
module fv_cdc_adc;
parameter WIDTH = 8;
parameter STAGES = 3;
`ifdef FORMAL
// ================================================================
// Global formal clock
// ================================================================
(* gclk *) reg formal_clk;
// ================================================================
// Asynchronous clock generation via $anyseq
// ================================================================
reg src_clk_r = 1'b0;
reg dst_clk_r = 1'b0;
wire src_clk_en;
wire dst_clk_en;
assign src_clk_en = $anyseq;
assign dst_clk_en = $anyseq;
always @(posedge formal_clk) begin
if (src_clk_en) src_clk_r <= !src_clk_r;
if (dst_clk_en) dst_clk_r <= !dst_clk_r;
end
wire src_clk = src_clk_r;
wire dst_clk = dst_clk_r;
// ================================================================
// Clock liveness — each clock must toggle within 7 gclk cycles
// 4-bit counters with saturation.
// ================================================================
reg [3:0] src_stall_cnt = 0;
reg [3:0] dst_stall_cnt = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
src_stall_cnt <= 0;
dst_stall_cnt <= 0;
end else begin
if (src_clk_en)
src_stall_cnt <= 0;
else if (src_stall_cnt < 4'd15)
src_stall_cnt <= src_stall_cnt + 1;
if (dst_clk_en)
dst_stall_cnt <= 0;
else if (dst_stall_cnt < 4'd15)
dst_stall_cnt <= dst_stall_cnt + 1;
end
end
always @(posedge formal_clk) begin
if (reset_n) begin
assume(src_stall_cnt < 4'd7);
assume(dst_stall_cnt < 4'd7);
end
end
// ================================================================
// Edge detection
// ================================================================
reg src_clk_prev = 1'b0;
reg dst_clk_prev = 1'b0;
always @(posedge formal_clk) begin
src_clk_prev <= src_clk;
dst_clk_prev <= dst_clk;
end
wire src_posedge = src_clk && !src_clk_prev;
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).
// ================================================================
reg reset_n = 1'b0;
reg [4:0] reset_cnt = 0;
always @(posedge formal_clk) begin
if (reset_cnt < 5'd20)
reset_cnt <= reset_cnt + 1;
end
always @(*) begin
reset_n = (reset_cnt >= 5'd20);
end
// ================================================================
// DUT signals
// ================================================================
wire [WIDTH-1:0] src_data;
reg src_valid = 1'b0;
wire [WIDTH-1:0] dst_data;
wire dst_valid;
assign src_data = $anyseq;
// src_valid: driven freely by solver, but pulsed (single-cycle)
wire src_valid_next;
assign src_valid_next = $anyseq;
always @(posedge formal_clk) begin
if (!reset_n)
src_valid <= 1'b0;
else if (src_posedge)
src_valid <= src_valid_next;
end
// ================================================================
// DUT instantiation
// ================================================================
wire [WIDTH-1:0] fv_src_data_reg;
wire [1:0] fv_src_toggle;
cdc_adc_to_processing #(
.WIDTH (WIDTH),
.STAGES(STAGES)
) dut (
.src_clk (src_clk),
.dst_clk (dst_clk),
.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)
);
// ================================================================
// Past-valid tracker
// ================================================================
reg fv_past_valid = 1'b0;
always @(posedge formal_clk) begin
fv_past_valid <= 1'b1;
end
// ================================================================
// 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;
always @(posedge formal_clk) begin
if (!reset_n && src_posedge)
src_saw_posedge <= 1'b1;
end
always @(posedge formal_clk) begin
if (!reset_n && dst_posedge)
dst_saw_posedge <= 1'b1;
end
always @(posedge formal_clk) begin
src_reset_done <= src_saw_posedge;
dst_reset_done <= dst_saw_posedge;
end
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.
// ================================================================
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}});
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.
// ================================================================
reg fv_any_src_valid = 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;
end
always @(posedge formal_clk) begin
if (dut_initialized && !fv_any_src_valid) begin
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).
//
// 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.
//
// 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.
// ================================================================
reg [6:0] fv_src_cooldown = 0;
always @(posedge formal_clk) begin
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
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
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;
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;
end
end
// When dst_valid fires, dst_data must match fv_src_data_reg
// (the value the DUT's source domain actually captured).
always @(posedge formal_clk) begin
if (dut_initialized && dst_posedge && dst_valid) begin
assert(dst_data == fv_src_data_reg);
end
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).
// ================================================================
reg [6:0] fv_propagation_timer = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
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
fv_propagation_timer <= fv_propagation_timer + 1;
end else if (dst_posedge && dst_valid) begin
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
end
// ================================================================
// COVER properties
// ================================================================
always @(posedge formal_clk) begin
if (dut_initialized) begin
// Cover: src captures data
cover(src_posedge && src_valid);
// Cover: dst presents valid data
cover(dst_posedge && dst_valid);
// Cover: dst_valid seen after src_valid was asserted
cover(dst_posedge && dst_valid && fv_past_valid);
// Cover: two successive transfers complete
cover(dst_posedge && dst_valid && fv_transfer_count >= 1);
end
end
`endif // FORMAL
endmodule
9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.sby
+22
View File
@@ -0,0 +1,22 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 100
cover: mode cover
cover: depth 200
[engines]
smtbmc z3
[script]
read_verilog -formal cdc_modules.v
read_verilog -formal fv_cdc_handshake.v
prep -top fv_cdc_handshake
clk2fflogic
[files]
../cdc_modules.v
fv_cdc_handshake.v
9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v
+456
View File
@@ -0,0 +1,456 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: cdc_handshake
// AERIS-10 Radar FPGA — CDC Handshake (req/ack)
// Target: SymbiYosys with smtbmc/z3
//
// This is the most critical CDC module. The properties verify protocol
// correctness, data integrity, and liveness under multi-clock formal.
// ============================================================================
module fv_cdc_handshake;
parameter WIDTH = 8; // Reduced from 32 for faster formal solving
`ifdef FORMAL
// ================================================================
// Global formal clock
// ================================================================
(* gclk *) reg formal_clk;
// ================================================================
// Asynchronous clock generation
// $anyseq enables let the solver freely interleave clock edges.
// ================================================================
reg src_clk_r = 1'b0;
reg dst_clk_r = 1'b0;
wire src_clk_en;
wire dst_clk_en;
assign src_clk_en = $anyseq;
assign dst_clk_en = $anyseq;
always @(posedge formal_clk) begin
if (src_clk_en) src_clk_r <= !src_clk_r;
if (dst_clk_en) dst_clk_r <= !dst_clk_r;
end
wire src_clk = src_clk_r;
wire dst_clk = dst_clk_r;
// ================================================================
// Clock liveness: each clock must toggle within 7 gclk cycles
// Using 4-bit counters with saturation to avoid overflow.
// ================================================================
reg [3:0] src_stall_cnt = 0;
reg [3:0] dst_stall_cnt = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
src_stall_cnt <= 0;
dst_stall_cnt <= 0;
end else begin
if (src_clk_en)
src_stall_cnt <= 0;
else if (src_stall_cnt < 4'd15)
src_stall_cnt <= src_stall_cnt + 1;
if (dst_clk_en)
dst_stall_cnt <= 0;
else if (dst_stall_cnt < 4'd15)
dst_stall_cnt <= dst_stall_cnt + 1;
end
end
always @(posedge formal_clk) begin
if (reset_n) begin
assume(src_stall_cnt < 4'd7);
assume(dst_stall_cnt < 4'd7);
end
end
// ================================================================
// Edge detection for clock domains
// ================================================================
reg src_clk_prev = 1'b0;
reg dst_clk_prev = 1'b0;
always @(posedge formal_clk) begin
src_clk_prev <= src_clk;
dst_clk_prev <= dst_clk;
end
wire src_posedge = src_clk && !src_clk_prev;
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).
// ================================================================
reg reset_n = 1'b0;
reg [4:0] reset_cnt = 0;
always @(posedge formal_clk) begin
if (reset_cnt < 5'd20)
reset_cnt <= reset_cnt + 1;
end
always @(*) begin
reset_n = (reset_cnt >= 5'd20);
end
// ================================================================
// DUT signals
// ================================================================
wire [WIDTH-1:0] src_data;
reg src_valid = 1'b0;
wire src_ready;
wire [WIDTH-1:0] dst_data;
wire dst_valid;
reg dst_ready = 1'b0;
// Formal observation ports (exposed by DUT under `ifdef FORMAL)
wire fv_src_busy;
wire fv_dst_ack;
wire fv_dst_req_sync;
wire [1:0] fv_src_ack_sync_chain;
wire [1:0] fv_dst_req_sync_chain;
wire [WIDTH-1:0] fv_src_data_reg_hs;
assign src_data = $anyseq;
// src_valid: driven freely by the solver, using a hold-until-
// accepted pattern that mirrors real producer behaviour and avoids
// a combinational dependency on src_ready (which is a DUT output
// subject to clk2fflogic timing).
//
// Protocol:
// - When idle (!src_valid), the solver can freely assert or
// deassert src_valid on any src_posedge.
// - Once src_valid is asserted it is held high until the DUT
// accepts it (src_valid && src_ready on a src_posedge), after
// which it clears. This matches the valid/ready handshake
// convention and guarantees that src_valid is stable for the
// DUT to sample.
wire src_valid_next;
assign src_valid_next = $anyseq;
always @(posedge formal_clk) begin
if (!reset_n)
src_valid <= 1'b0;
else if (src_posedge) begin
if (src_valid && src_ready)
src_valid <= 1'b0; // accepted — clear
else if (!src_valid)
src_valid <= src_valid_next; // idle — solver drives
// else: src_valid is 1 but src_ready is 0 — hold
end
end
// dst_ready: driven freely by solver after reset
wire dst_ready_next;
assign dst_ready_next = $anyseq;
always @(posedge formal_clk) begin
if (!reset_n)
dst_ready <= 1'b0;
else if (dst_posedge)
dst_ready <= dst_ready_next;
end
// ================================================================
// DUT instantiation
// ================================================================
cdc_handshake #(
.WIDTH(WIDTH)
) dut (
.src_clk (src_clk),
.dst_clk (dst_clk),
.reset_n (reset_n),
.src_data (src_data),
.src_valid(src_valid),
.src_ready(src_ready),
.dst_data (dst_data),
.dst_valid(dst_valid),
.dst_ready(dst_ready),
.fv_src_busy (fv_src_busy),
.fv_dst_ack (fv_dst_ack),
.fv_dst_req_sync (fv_dst_req_sync),
.fv_src_ack_sync_chain(fv_src_ack_sync_chain),
.fv_dst_req_sync_chain(fv_dst_req_sync_chain),
.fv_src_data_reg_hs (fv_src_data_reg_hs)
);
// ================================================================
// Past-valid tracker
// ================================================================
reg fv_past_valid = 1'b0;
always @(posedge formal_clk) begin
fv_past_valid <= 1'b1;
end
// ================================================================
// 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. We need to delay
// by one extra cycle to avoid checking DUT state before it processes
// the reset.
// ================================================================
reg src_saw_posedge = 1'b0;
reg dst_saw_posedge = 1'b0;
reg src_reset_done = 1'b0;
reg dst_reset_done = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n && src_posedge)
src_saw_posedge <= 1'b1;
end
always @(posedge formal_clk) begin
if (!reset_n && dst_posedge)
dst_saw_posedge <= 1'b1;
end
// Delay by one cycle to let clk2fflogic-transformed DUT process
always @(posedge formal_clk) begin
src_reset_done <= src_saw_posedge;
dst_reset_done <= dst_saw_posedge;
end
wire dut_initialized = reset_n && src_reset_done && dst_reset_done;
// ================================================================
// PROPERTY 1: src_ready == !src_busy
// src_ready is defined as !src_busy in the RTL. Verify this
// structural invariant holds.
// ================================================================
always @(posedge formal_clk) begin
if (dut_initialized) begin
assert(src_ready == !fv_src_busy);
end
end
// ================================================================
// PROPERTY 2: Reset behavior
// During reset all outputs are deasserted, internal state is clear.
// ================================================================
always @(posedge formal_clk) begin
if (!reset_n && src_reset_done && dst_reset_done) begin
assert(src_ready == 1'b1); // src_busy == 0
assert(dst_valid == 1'b0);
assert(fv_dst_ack == 1'b0);
end
end
// ================================================================
// PROPERTY 3: dst_valid bounded duration
// dst_valid must not remain asserted indefinitely. After dst_valid
// goes high, it must clear within a bounded window (assuming
// dst_ready eventually fires — already constrained by Property 5).
//
// NOTE: We cannot assert "dst_valid == 0 on the next dst_clk
// after consumption" because: (a) clk2fflogic adds pipeline
// latency making exact-cycle checks unreliable, and (b) the DUT
// validly re-latches data if dst_req_sync is still high.
// Instead we use a bounded-duration check.
// ================================================================
reg [5:0] fv_dst_valid_duration = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_dst_valid_duration <= 0;
end else if (dst_posedge) begin
if (dst_valid)
fv_dst_valid_duration <= fv_dst_valid_duration + 1;
else
fv_dst_valid_duration <= 0;
end
end
// dst_valid must not stay high for more than 60 dst_clk edges.
// After dst_ready fires and dst_valid_reg clears, the DUT
// immediately re-asserts dst_valid on the next dst_clk if
// dst_req_sync is still high (waiting for ack round-trip).
// This loop continues until src_busy deasserts and propagates
// through 2-stage sync back to dst. Worst case with stall
// bound 7: ~4 sync stages × 14 gclk = ~56 gclk ≈ 28 dst edges,
// but with adversarial clock interleaving the effective count
// can exceed 30. Bound 60 provides margin.
always @(posedge formal_clk) begin
if (dut_initialized) begin
assert(fv_dst_valid_duration < 60);
end
end
// ================================================================
// PROPERTY 4: Data stability during dst_valid
// While dst_valid is asserted, dst_data must remain stable.
//
// NOTE: We cannot compare dst_data against fv_src_data_reg_hs
// (the DUT's current src_data_reg) because src_data_reg may
// change after dst captures it — the source becomes ready and
// can accept new data while the destination still presents the
// old value. Instead, we verify dst_data doesn't change while
// dst_valid is high, which proves no corruption during delivery.
// ================================================================
reg [WIDTH-1:0] fv_dst_data_snapshot;
reg fv_dst_valid_prev = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_dst_valid_prev <= 1'b0;
end else if (dst_posedge) begin
fv_dst_valid_prev <= dst_valid;
// Capture data on rising edge of dst_valid
if (dst_valid && !fv_dst_valid_prev)
fv_dst_data_snapshot <= dst_data;
end
end
// dst_data must remain stable throughout the dst_valid pulse
always @(posedge formal_clk) begin
if (dut_initialized && dst_posedge && dst_valid && fv_dst_valid_prev) begin
assert(dst_data == fv_dst_data_snapshot);
end
end
// ================================================================
// PROPERTY 5: src_ready eventually reasserts (bounded liveness)
// After src_busy goes high, it must come back low within a bounded
// number of gclk cycles, provided dst_ready eventually asserts.
//
// With 2-stage sync chains in both directions + protocol latency,
// the worst-case round-trip is roughly:
// src_busy -> 2 dst_clk sync -> dst processing -> dst_ack ->
// 2 src_clk sync -> src clears busy
// At ~4 gclk per clock edge, this is bounded by ~50 gclk cycles.
// ================================================================
reg [6:0] fv_busy_timer = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_busy_timer <= 0;
end else if (fv_src_busy) begin
fv_busy_timer <= fv_busy_timer + 1;
end else begin
fv_busy_timer <= 0;
end
end
// Assume dst_ready asserts within a bounded window when dst_valid
// is high (environment liveness assumption).
reg [3:0] fv_dst_valid_wait = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_dst_valid_wait <= 0;
end else if (dst_posedge && dst_valid && !dst_ready) begin
fv_dst_valid_wait <= fv_dst_valid_wait + 1;
end else begin
fv_dst_valid_wait <= 0;
end
end
always @(posedge formal_clk) begin
// Consumer must respond within 8 dst_clk-edges
if (reset_n) begin
assume(fv_dst_valid_wait < 8);
end
end
// With bounded consumer latency, busy must clear within 100 gclk
// (wider bound due to stall window of 7 instead of 4)
always @(posedge formal_clk) begin
if (dut_initialized) begin
assert(fv_busy_timer < 100);
end
end
// ================================================================
// PROPERTY 6: Protocol — dst_ack bounded duration
// dst_ack must not remain asserted indefinitely. Once src_busy
// deasserts (visible as !dst_req_sync), dst_ack will be cleared
// on the next dst_clk edge. We use a bounded-duration check
// rather than exact-cycle timing due to clk2fflogic latency.
// ================================================================
reg [6:0] fv_ack_duration = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
fv_ack_duration <= 0;
end else if (dst_posedge) begin
if (fv_dst_ack)
fv_ack_duration <= fv_ack_duration + 1;
else
fv_ack_duration <= 0;
end
end
// dst_ack must clear within a reasonable window.
// Worst case: src_busy propagates back through 2-stage sync,
// then dst_ack clears. Bounded by ~50 gclk (~25 dst edges).
always @(posedge formal_clk) begin
if (dut_initialized) begin
assert(fv_ack_duration < 50);
end
end
// ================================================================
// PROPERTY 7: No unbounded state growth
// The sync chain registers are bounded by construction (2-bit).
// Verify src_ack_sync_chain and dst_req_sync_chain stay in range.
// (They are 2-bit regs, so this is structural, but good to assert.)
// ================================================================
always @(posedge formal_clk) begin
if (dut_initialized) begin
assert(fv_src_ack_sync_chain <= 2'b11);
assert(fv_dst_req_sync_chain <= 2'b11);
end
end
// ================================================================
// COVER properties — reachability of key protocol states
// ================================================================
// Cover: full handshake completes (data accepted by src, delivered
// at dst, consumed, and src_ready re-asserts).
reg fv_cover_phase = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n)
fv_cover_phase <= 1'b0;
else if (dut_initialized && src_posedge && src_valid && src_ready)
fv_cover_phase <= 1'b1;
end
// Cover 1 & 2: not gated by dut_initialized because they're
// purely observational (no assertion content). They can fire
// before or after initialization.
always @(posedge formal_clk) begin
// Cover: src accepts data (after reset released)
if (reset_n) begin
cover(src_posedge && src_valid && src_ready);
end
end
always @(posedge formal_clk) begin
if (dut_initialized) begin
// Cover: dst presents valid data
cover(dst_posedge && dst_valid);
// Cover: dst consumes data
cover(dst_posedge && dst_valid && dst_ready);
// Cover: full round-trip — src back to ready after transfer
// that started AFTER dut_initialized
cover(fv_cover_phase && src_ready && !fv_src_busy);
end
end
`endif // FORMAL
endmodule
9_Firmware/9_2_FPGA/formal/fv_cdc_handshake_cover.sby
+19
View File
@@ -0,0 +1,19 @@
[tasks]
cover
[options]
cover: mode cover
cover: depth 200
[engines]
smtbmc z3
[script]
read_verilog -formal cdc_modules.v
read_verilog -formal fv_cdc_handshake.v
prep -top fv_cdc_handshake
clk2fflogic
[files]
../cdc_modules.v
fv_cdc_handshake.v
9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.sby
+22
View File
@@ -0,0 +1,22 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 80
cover: mode cover
cover: depth 80
[engines]
smtbmc z3
[script]
read_verilog -formal cdc_modules.v
read_verilog -formal fv_cdc_single_bit.v
prep -top fv_cdc_single_bit
clk2fflogic
[files]
../cdc_modules.v
fv_cdc_single_bit.v
9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.v
+217
View File
@@ -0,0 +1,217 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: cdc_single_bit
// AERIS-10 Radar FPGA — CDC Single-Bit Synchronizer
// Target: SymbiYosys with smtbmc/z3
// ============================================================================
module fv_cdc_single_bit;
parameter STAGES = 3;
`ifdef FORMAL
// ----------------------------------------------------------------
// Global formal clock — Yosys gclk drives all formal evaluation
// ----------------------------------------------------------------
(* gclk *) reg formal_clk;
// ----------------------------------------------------------------
// Asynchronous clock generation
// Use $anyseq to let the solver freely schedule clock edges,
// modeling truly asynchronous clock domains.
// ----------------------------------------------------------------
reg src_clk_r = 1'b0;
reg dst_clk_r = 1'b0;
wire src_clk_en;
wire dst_clk_en;
assign src_clk_en = $anyseq;
assign dst_clk_en = $anyseq;
always @(posedge formal_clk) begin
if (src_clk_en) src_clk_r <= !src_clk_r;
if (dst_clk_en) dst_clk_r <= !dst_clk_r;
end
wire src_clk = src_clk_r;
wire dst_clk = dst_clk_r;
// ----------------------------------------------------------------
// Liveness: clocks must toggle eventually (fairness constraints)
// Without this the solver could hold clocks static forever.
// ----------------------------------------------------------------
// Each clock must toggle within 7 gclk cycles. Using 4-bit
// counters with saturation to avoid overflow.
reg [3:0] src_no_toggle_cnt = 0;
reg [3:0] dst_no_toggle_cnt = 0;
always @(posedge formal_clk) begin
if (!reset_n) begin
src_no_toggle_cnt <= 0;
dst_no_toggle_cnt <= 0;
end else begin
if (src_clk_en)
src_no_toggle_cnt <= 0;
else if (src_no_toggle_cnt < 4'd15)
src_no_toggle_cnt <= src_no_toggle_cnt + 1;
if (dst_clk_en)
dst_no_toggle_cnt <= 0;
else if (dst_no_toggle_cnt < 4'd15)
dst_no_toggle_cnt <= dst_no_toggle_cnt + 1;
end
end
always @(posedge formal_clk) begin
if (reset_n) begin
assume(src_no_toggle_cnt < 4'd7);
assume(dst_no_toggle_cnt < 4'd7);
end
end
// ----------------------------------------------------------------
// DUT signals
// ----------------------------------------------------------------
reg reset_n = 1'b0;
wire src_signal;
wire dst_signal;
assign src_signal = $anyseq;
// ----------------------------------------------------------------
// Reset generation: hold reset for enough cycles to guarantee
// both clocks see at least one posedge during reset (with stall
// bound of 7, worst case is ~14 gclk cycles for one full period).
// ----------------------------------------------------------------
reg [4:0] reset_cnt = 0;
always @(posedge formal_clk) begin
if (reset_cnt < 5'd20)
reset_cnt <= reset_cnt + 1;
end
always @(*) begin
reset_n = (reset_cnt >= 5'd20);
end
// ----------------------------------------------------------------
// DUT instantiation
// ----------------------------------------------------------------
cdc_single_bit #(
.STAGES(STAGES)
) dut (
.src_clk (src_clk),
.dst_clk (dst_clk),
.reset_n (reset_n),
.src_signal(src_signal),
.dst_signal(dst_signal)
);
// ----------------------------------------------------------------
// Track dst_clk edges for property evaluation
// ----------------------------------------------------------------
reg dst_clk_prev = 1'b0;
wire dst_posedge;
always @(posedge formal_clk) begin
dst_clk_prev <= dst_clk;
end
assign dst_posedge = dst_clk && !dst_clk_prev;
// ----------------------------------------------------------------
// Property: Output is 0 during reset
// With synchronous reset, the sync_chain is only cleared on a
// dst_clk posedge while !reset_n. We must track whether at least
// one dst_clk posedge has occurred during reset before asserting.
// ----------------------------------------------------------------
reg dst_posedge_during_reset = 1'b0;
always @(posedge formal_clk) begin
if (reset_n)
dst_posedge_during_reset <= 1'b0;
else if (dst_posedge)
dst_posedge_during_reset <= 1'b1;
end
// ----------------------------------------------------------------
// DUT initialized flag
// The DUT uses synchronous reset, so registers are undefined until
// at least one dst_clk posedge occurs during reset. Properties
// should only fire after reset has been applied AND released.
//
// With clk2fflogic, the DUT's register updates are delayed one
// formal_clk cycle vs our edge detection. Add a pipeline delay.
// ----------------------------------------------------------------
reg dst_saw_posedge = 1'b0;
reg dst_reset_done = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n && dst_posedge)
dst_saw_posedge <= 1'b1;
end
always @(posedge formal_clk) begin
dst_reset_done <= dst_saw_posedge;
end
wire dut_initialized = reset_n && dst_reset_done;
always @(posedge formal_clk) begin
if (!reset_n && dst_posedge_during_reset) begin
assert(dst_signal == 1'b0);
end
end
// ----------------------------------------------------------------
// Property: Output only changes on dst_clk posedge
// If there was no dst_clk posedge, dst_signal must be stable.
// ----------------------------------------------------------------
reg dst_signal_prev = 1'b0;
reg past_valid = 1'b0;
always @(posedge formal_clk) begin
past_valid <= 1'b1;
dst_signal_prev <= dst_signal;
end
always @(posedge formal_clk) begin
if (dut_initialized && past_valid && !dst_posedge) begin
assert(dst_signal == dst_signal_prev);
end
end
// ----------------------------------------------------------------
// Cover: dst_signal transitions 0->1 after reset
// ----------------------------------------------------------------
reg seen_dst_low_after_reset = 1'b0;
always @(posedge formal_clk) begin
if (!reset_n)
seen_dst_low_after_reset <= 1'b0;
else if (dst_posedge && dst_signal == 1'b0)
seen_dst_low_after_reset <= 1'b1;
end
always @(posedge formal_clk) begin
if (dut_initialized) begin
// Cover a 0->1 transition
cover(past_valid && dst_posedge && dst_signal == 1'b1 && dst_signal_prev == 1'b0);
// Cover a 1->0 transition
cover(past_valid && dst_posedge && dst_signal == 1'b0 && dst_signal_prev == 1'b1);
end
end
// ----------------------------------------------------------------
// Cover: basic reachability — output can be 1 after reset
// ----------------------------------------------------------------
always @(posedge formal_clk) begin
if (dut_initialized) begin
cover(dst_signal == 1'b1);
end
end
`endif // FORMAL
endmodule
9_Firmware/9_2_FPGA/formal/fv_doppler_processor.sby
+27
View File
@@ -0,0 +1,27 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 150
cover: mode cover
cover: depth 150
[engines]
smtbmc z3
[script]
read_verilog -formal doppler_processor.v
read_verilog -formal xfft_32.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
../fft_engine.v
../fft_twiddle_32.mem
../fft_twiddle_1024.mem
fv_doppler_processor.v
9_Firmware/9_2_FPGA/formal/fv_doppler_processor.v
+223
View File
@@ -0,0 +1,223 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: doppler_processor_optimized
// AERIS-10 Radar FPGA — Doppler processing FSM with FFT
// Target: SymbiYosys with smtbmc/z3
//
// 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, DOPPLER_FFT_SIZE=4.
// Includes full xfft_32 and fft_engine sub-modules.
//
// Focus: memory address bounds (highest-value finding) and state encoding.
// ============================================================================
module fv_doppler_processor (
input wire clk
);
// Reduced parameters for tractable BMC
localparam RANGE_BINS = 4;
localparam CHIRPS_PER_FRAME = 4;
localparam DOPPLER_FFT_SIZE = 4;
localparam MEM_DEPTH = RANGE_BINS * CHIRPS_PER_FRAME; // 16
// State encoding (mirrors DUT localparams)
localparam S_IDLE = 3'b000;
localparam S_ACCUMULATE = 3'b001;
localparam S_PRE_READ = 3'b101;
localparam S_LOAD_FFT = 3'b010;
localparam S_FFT_WAIT = 3'b011;
localparam S_OUTPUT = 3'b100;
`ifdef FORMAL
// ================================================================
// Clock is an input wire — smtbmc drives it automatically.
// async2sync (in .sby, default) converts async reset to sync.
// ================================================================
// Past-valid tracker
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 [31:0] range_data;
(* anyseq *) wire data_valid;
(* anyseq *) wire new_chirp_frame;
// ================================================================
// DUT outputs
// ================================================================
wire [31:0] doppler_output;
wire doppler_valid;
wire [4:0] doppler_bin;
wire [5:0] range_bin;
wire processing_active;
wire frame_complete;
wire [3:0] status;
// Formal-only DUT outputs (internal state)
wire [2:0] state;
wire [10:0] mem_write_addr;
wire [10:0] mem_read_addr;
wire [5:0] write_range_bin;
wire [4:0] write_chirp_index;
wire [5:0] read_range_bin;
wire [4:0] read_doppler_index;
wire [9:0] processing_timeout;
wire frame_buffer_full;
wire mem_we;
wire [10:0] mem_waddr_r;
// ================================================================
// DUT instantiation
// ================================================================
doppler_processor_optimized #(
.DOPPLER_FFT_SIZE (DOPPLER_FFT_SIZE),
.RANGE_BINS (RANGE_BINS),
.CHIRPS_PER_FRAME (CHIRPS_PER_FRAME),
.WINDOW_TYPE (1), // Rectangular — simpler for formal
.DATA_WIDTH (16)
) dut (
.clk (clk),
.reset_n (reset_n),
.range_data (range_data),
.data_valid (data_valid),
.new_chirp_frame (new_chirp_frame),
.doppler_output (doppler_output),
.doppler_valid (doppler_valid),
.doppler_bin (doppler_bin),
.range_bin (range_bin),
.processing_active(processing_active),
.frame_complete (frame_complete),
.status (status),
.fv_state (state),
.fv_mem_write_addr (mem_write_addr),
.fv_mem_read_addr (mem_read_addr),
.fv_write_range_bin (write_range_bin),
.fv_write_chirp_index (write_chirp_index),
.fv_read_range_bin (read_range_bin),
.fv_read_doppler_index (read_doppler_index),
.fv_processing_timeout (processing_timeout),
.fv_frame_buffer_full (frame_buffer_full),
.fv_mem_we (mem_we),
.fv_mem_waddr_r (mem_waddr_r)
);
// Internals now accessed via formal output ports
// ================================================================
// Input assumptions
// ================================================================
// data_valid should not assert when frame buffer is already full
always @(posedge clk) begin
if (reset_n && frame_buffer_full)
assume(!data_valid);
end
// new_chirp_frame must be a clean pulse (not during active processing)
always @(posedge clk) begin
if (reset_n && state != S_IDLE)
assume(!new_chirp_frame);
end
// ================================================================
// PROPERTY 1: Memory write address bounds
// mem_waddr_r must be within MEM_DEPTH whenever mem_we is active
// ================================================================
always @(posedge clk) begin
if (reset_n && mem_we)
assert(mem_waddr_r < MEM_DEPTH);
end
// ================================================================
// PROPERTY 2: Memory read address bounds
// KEY BUG TARGET: read_doppler_index overflow from
// fft_sample_counter + 2 truncation (doppler_processor.v:329)
// causes wrong mem_read_addr.
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
if (state == S_PRE_READ || state == S_LOAD_FFT ||
state == S_FFT_WAIT)
assert(mem_read_addr < MEM_DEPTH);
end
end
// ================================================================
// PROPERTY 3: Write pointer bounds
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
assert(write_range_bin < RANGE_BINS);
assert(write_chirp_index < CHIRPS_PER_FRAME);
end
end
// ================================================================
// PROPERTY 4: State encoding — only 6 valid states
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
assert(state == S_IDLE ||
state == S_ACCUMULATE ||
state == S_PRE_READ ||
state == S_LOAD_FFT ||
state == S_FFT_WAIT ||
state == S_OUTPUT);
end
end
// ================================================================
// PROPERTY 5: Timeout bound
// processing_timeout is loaded with 1000 and counts down.
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(processing_timeout < 1001);
end
// ================================================================
// PROPERTY 6: Read range bin bound
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(read_range_bin < RANGE_BINS);
end
// ================================================================
// COVER 1: Complete processing of all range bins
// ================================================================
always @(posedge clk) begin
if (reset_n)
cover(frame_complete && f_past_valid);
end
// ================================================================
// COVER 2: Each state is reachable
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
cover(state == S_IDLE);
cover(state == S_ACCUMULATE);
cover(state == S_PRE_READ);
cover(state == S_LOAD_FFT);
cover(state == S_FFT_WAIT);
cover(state == S_OUTPUT);
end
end
`endif // FORMAL
endmodule
9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby
+21
View File
@@ -0,0 +1,21 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 200
cover: mode cover
cover: depth 200
[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
9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v
+214
View File
@@ -0,0 +1,214 @@
`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;
// ================================================================
// 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),
.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 &&
$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 scan completes (scan_complete pulses)
// ================================================================
always @(posedge clk) begin
if (reset_n)
cover(scan_complete);
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
9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.sby
+21
View File
@@ -0,0 +1,21 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 120
cover: mode cover
cover: depth 120
[engines]
smtbmc z3
[script]
read_verilog -formal range_bin_decimator.v
read_verilog -formal fv_range_bin_decimator.v
prep -top fv_range_bin_decimator
[files]
../range_bin_decimator.v
fv_range_bin_decimator.v
9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.v
+243
View File
@@ -0,0 +1,243 @@
`timescale 1ns / 1ps
// ============================================================================
// Formal Verification Wrapper: range_bin_decimator
// AERIS-10 Radar FPGA — 5-state decimation FSM
// Target: SymbiYosys with smtbmc/z3
//
// Single-clock design: clk is an input wire, async2sync handles async reset.
// Each formal step = one clock edge.
//
// Parameters reduced: 32 input bins -> 4 output bins, factor 8.
// ============================================================================
module fv_range_bin_decimator (
input wire clk
);
// Reduced parameters for tractable BMC
localparam INPUT_BINS = 32;
localparam OUTPUT_BINS = 4;
localparam DECIMATION_FACTOR = 8;
// State encoding (mirrors DUT localparams)
localparam ST_IDLE = 3'd0;
localparam ST_SKIP = 3'd1;
localparam ST_PROCESS = 3'd2;
localparam ST_EMIT = 3'd3;
localparam ST_DONE = 3'd4;
`ifdef FORMAL
// ================================================================
// Clock is an input wire — smtbmc drives it automatically.
// async2sync (in .sby, default) converts async reset to sync.
// ================================================================
// Past-valid tracker
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
// ================================================================
(* anyseq *) wire signed [15:0] range_i_in;
(* anyseq *) wire signed [15:0] range_q_in;
(* anyseq *) wire range_valid_in;
// decimation_mode and start_bin are constant per trace
(* anyconst *) wire [1:0] decimation_mode;
(* anyconst *) wire [9:0] start_bin;
// ================================================================
// DUT instantiation
// ================================================================
wire signed [15:0] range_i_out;
wire signed [15:0] range_q_out;
wire range_valid_out;
wire [5:0] range_bin_index;
wire [2:0] state;
wire [9:0] in_bin_count;
wire [3:0] group_sample_count;
wire [5:0] output_bin_count;
wire [9:0] skip_count;
range_bin_decimator #(
.INPUT_BINS (INPUT_BINS),
.OUTPUT_BINS (OUTPUT_BINS),
.DECIMATION_FACTOR (DECIMATION_FACTOR)
) dut (
.clk (clk),
.reset_n (reset_n),
.range_i_in (range_i_in),
.range_q_in (range_q_in),
.range_valid_in (range_valid_in),
.range_i_out (range_i_out),
.range_q_out (range_q_out),
.range_valid_out (range_valid_out),
.range_bin_index (range_bin_index),
.decimation_mode (decimation_mode),
.start_bin (start_bin),
.fv_state (state),
.fv_in_bin_count (in_bin_count),
.fv_group_sample_count (group_sample_count),
.fv_output_bin_count (output_bin_count),
.fv_skip_count (skip_count)
);
// Internals now accessed via formal output ports
// ================================================================
// Helper counters
// ================================================================
// Input valid pulse counter
reg [9:0] fv_valid_in_count;
initial fv_valid_in_count = 10'd0;
always @(posedge clk) begin
if (!reset_n)
fv_valid_in_count <= 10'd0;
else if (range_valid_in)
fv_valid_in_count <= fv_valid_in_count + 10'd1;
end
// Output valid pulse counter
reg [5:0] fv_valid_out_count;
initial fv_valid_out_count = 6'd0;
always @(posedge clk) begin
if (!reset_n)
fv_valid_out_count <= 6'd0;
else if (state == ST_IDLE)
fv_valid_out_count <= 6'd0;
else if (range_valid_out)
fv_valid_out_count <= fv_valid_out_count + 6'd1;
end
// ================================================================
// Input assumptions
// ================================================================
// No valid input after INPUT_BINS samples have been consumed
always @(posedge clk) begin
if (reset_n && fv_valid_in_count >= INPUT_BINS)
assume(!range_valid_in);
end
// No valid input when FSM is in ST_DONE
always @(posedge clk) begin
if (reset_n && state == ST_DONE)
assume(!range_valid_in);
end
// Constrain start_bin to sensible range
always @(*) begin
assume(start_bin < INPUT_BINS);
end
// Constrain decimation_mode to valid values (not reserved mode 11)
always @(*) begin
assume(decimation_mode != 2'b11);
end
// ================================================================
// PROPERTY 1: State encoding — states 5,6,7 unreachable
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(state <= 3'd4);
end
// ================================================================
// PROPERTY 2: Output bin count never exceeds OUTPUT_BINS
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(output_bin_count <= OUTPUT_BINS);
end
// ================================================================
// PROPERTY 3: Group sample count stays within decimation factor
// ================================================================
always @(posedge clk) begin
if (reset_n)
assert(group_sample_count < DECIMATION_FACTOR);
end
// ================================================================
// PROPERTY 4: No output in wrong states
// range_valid_out is a registered output set in ST_EMIT on cycle N,
// observed as high on cycle N+1 when state has already advanced.
// So check $past(state) was ST_EMIT.
// ================================================================
always @(posedge clk) begin
if (reset_n && f_past_valid && range_valid_out)
assert($past(state) == ST_EMIT);
end
// ================================================================
// PROPERTY 5: Exactly OUTPUT_BINS outputs per frame
// When state reaches ST_DONE, exactly OUTPUT_BINS valid output
// pulses must have been emitted.
//
// Timing: The last range_valid_out is registered in ST_EMIT and
// appears high on the same posedge that state transitions to
// ST_DONE. The wrapper's fv_valid_out_count absorbs that pulse
// via NBA on that edge, so it is only visible one cycle later.
// Check when $past(state) == ST_DONE (i.e. the cycle after entry)
// so the counter has resolved. At this point state == ST_IDLE,
// but the counter's ST_IDLE reset is also an NBA that hasn't
// resolved yet, so fv_valid_out_count still reads OUTPUT_BINS.
// ================================================================
always @(posedge clk) begin
if (reset_n && f_past_valid && $past(state) == ST_DONE)
assert(fv_valid_out_count == OUTPUT_BINS);
end
// ================================================================
// PROPERTY 6: Skip logic
// When start_bin > 0, the first output must not appear until
// at least start_bin input samples have been consumed.
// ================================================================
always @(posedge clk) begin
if (reset_n && start_bin > 10'd0 && fv_valid_in_count <= start_bin)
assert(!range_valid_out);
end
// ================================================================
// COVER 1: State reachability
// ================================================================
always @(posedge clk) begin
if (reset_n) begin
cover(state == ST_IDLE);
cover(state == ST_SKIP);
cover(state == ST_PROCESS);
cover(state == ST_EMIT);
cover(state == ST_DONE);
end
end
// ================================================================
// COVER 2: Complete frame with start_bin = 0, mode = 00 (decimate)
// ================================================================
always @(posedge clk) begin
if (reset_n)
cover(state == ST_DONE && start_bin == 10'd0 &&
decimation_mode == 2'b00);
end
// ================================================================
// COVER 3: Complete frame with peak detection mode
// ================================================================
always @(posedge clk) begin
if (reset_n)
cover(state == ST_DONE && decimation_mode == 2'b01);
end
`endif // FORMAL
endmodule
9_Firmware/9_2_FPGA/radar_mode_controller.v
+11
View File
@@ -75,6 +75,12 @@ module radar_mode_controller #(
// Status
output wire scanning, // 1 = scan in progress
output wire scan_complete // pulse when full scan done
`ifdef FORMAL
,
output wire [2:0] fv_scan_state,
output wire [17:0] fv_timer
`endif
);
// ============================================================================
@@ -94,6 +100,11 @@ localparam S_ADVANCE = 3'd6;
// Timing counter
reg [17:0] timer; // enough for up to 262143 cycles (~2.6ms at 100 MHz)
`ifdef FORMAL
assign fv_scan_state = scan_state;
assign fv_timer = timer;
`endif
// Edge detection for STM32 pass-through
reg stm32_new_chirp_prev;
reg stm32_new_elevation_prev;
9_Firmware/9_2_FPGA/range_bin_decimator.v
+17
View File
@@ -52,6 +52,15 @@ module range_bin_decimator #(
// Configuration
input wire [1:0] decimation_mode, // 00=decimate, 01=peak, 10=average
input wire [9:0] start_bin // First input bin to process
`ifdef FORMAL
,
output wire [2:0] fv_state,
output wire [9:0] fv_in_bin_count,
output wire [3:0] fv_group_sample_count,
output wire [5:0] fv_output_bin_count,
output wire [9:0] fv_skip_count
`endif
);
// ============================================================================
@@ -76,6 +85,14 @@ localparam ST_DONE = 3'd4;
// Skip counter for start_bin
reg [9:0] skip_count;
`ifdef FORMAL
assign fv_state = state;
assign fv_in_bin_count = in_bin_count;
assign fv_group_sample_count = group_sample_count;
assign fv_output_bin_count = output_bin_count;
assign fv_skip_count = skip_count;
`endif
// ============================================================================
// PEAK DETECTION (Mode 01)
// ============================================================================