From fb59e9873796e556579988be4f0bcff9532fcde8 Mon Sep 17 00:00:00 2001 From: Jason <83615043+JJassonn69@users.noreply.github.com> Date: Tue, 17 Mar 2026 12:47:22 +0200 Subject: [PATCH] Add SymbiYosys formal verification for 6 modules, fix 2 doppler bugs 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) --- 9_Firmware/9_2_FPGA/cdc_modules.v | 47 +- 9_Firmware/9_2_FPGA/doppler_processor.v | 53 +- 9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby | 22 + 9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v | 358 ++++++++++++++ .../9_2_FPGA/formal/fv_cdc_handshake.sby | 22 + 9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v | 456 ++++++++++++++++++ .../formal/fv_cdc_handshake_cover.sby | 19 + .../9_2_FPGA/formal/fv_cdc_single_bit.sby | 22 + .../9_2_FPGA/formal/fv_cdc_single_bit.v | 217 +++++++++ .../9_2_FPGA/formal/fv_doppler_processor.sby | 27 ++ .../9_2_FPGA/formal/fv_doppler_processor.v | 223 +++++++++ .../formal/fv_radar_mode_controller.sby | 21 + .../formal/fv_radar_mode_controller.v | 214 ++++++++ .../formal/fv_range_bin_decimator.sby | 21 + .../9_2_FPGA/formal/fv_range_bin_decimator.v | 243 ++++++++++ 9_Firmware/9_2_FPGA/radar_mode_controller.v | 11 + 9_Firmware/9_2_FPGA/range_bin_decimator.v | 17 + 17 files changed, 1979 insertions(+), 14 deletions(-) create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_handshake_cover.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.v create mode 100644 9_Firmware/9_2_FPGA/formal/fv_doppler_processor.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_doppler_processor.v create mode 100644 9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v create mode 100644 9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.sby create mode 100644 9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.v diff --git a/9_Firmware/9_2_FPGA/cdc_modules.v b/9_Firmware/9_2_FPGA/cdc_modules.v index a9e3c3d..0536154 100644 --- a/9_Firmware/9_2_FPGA/cdc_modules.v +++ b/9_Firmware/9_2_FPGA/cdc_modules.v @@ -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; @@ -119,11 +123,18 @@ 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 @@ -178,9 +198,18 @@ module cdc_handshake #( reg dst_req_sync = 0; (* ASYNC_REG = "TRUE" *) reg [1:0] dst_req_sync_chain = 2'b00; reg dst_ack = 0; + +`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 - always @(posedge src_clk or negedge reset_n) begin + // 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; diff --git a/9_Firmware/9_2_FPGA/doppler_processor.v b/9_Firmware/9_2_FPGA/doppler_processor.v index 322f7e4..270dd17 100644 --- a/9_Firmware/9_2_FPGA/doppler_processor.v +++ b/9_Firmware/9_2_FPGA/doppler_processor.v @@ -16,9 +16,24 @@ module doppler_processor_optimized #( output reg doppler_valid, output reg [4:0] doppler_bin, output reg [5:0] range_bin, - output wire processing_active, - output wire frame_complete, - output reg [3:0] status + 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) - read_doppler_index <= fft_sample_counter + 2; + // 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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby b/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby new file mode 100644 index 0000000..d3c9a30 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v b/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v new file mode 100644 index 0000000..186351e --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_adc.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.sby b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.sby new file mode 100644 index 0000000..f88cf48 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v new file mode 100644 index 0000000..f61c221 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake_cover.sby b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake_cover.sby new file mode 100644 index 0000000..283778f --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_handshake_cover.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.sby b/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.sby new file mode 100644 index 0000000..1daff9e --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.v b/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.v new file mode 100644 index 0000000..3728bd3 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_cdc_single_bit.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.sby b/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.sby new file mode 100644 index 0000000..3d9472c --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.v b/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.v new file mode 100644 index 0000000..8ed1279 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_doppler_processor.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby b/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby new file mode 100644 index 0000000..8aeb48e --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v b/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v new file mode 100644 index 0000000..d6a7d25 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_radar_mode_controller.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.sby b/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.sby new file mode 100644 index 0000000..b74542d --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.sby @@ -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 diff --git a/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.v b/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.v new file mode 100644 index 0000000..2df1353 --- /dev/null +++ b/9_Firmware/9_2_FPGA/formal/fv_range_bin_decimator.v @@ -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 diff --git a/9_Firmware/9_2_FPGA/radar_mode_controller.v b/9_Firmware/9_2_FPGA/radar_mode_controller.v index 6e75b6a..63bd9d9 100644 --- a/9_Firmware/9_2_FPGA/radar_mode_controller.v +++ b/9_Firmware/9_2_FPGA/radar_mode_controller.v @@ -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; diff --git a/9_Firmware/9_2_FPGA/range_bin_decimator.v b/9_Firmware/9_2_FPGA/range_bin_decimator.v index a49dcba..569f144 100644 --- a/9_Firmware/9_2_FPGA/range_bin_decimator.v +++ b/9_Firmware/9_2_FPGA/range_bin_decimator.v @@ -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) // ============================================================================