// ============================================================================ // CV-X1 Pro (Ironwood-X1 Subsystem IP) — Synthesizable Timing-Balanced // 3-Stage Pipelined 8-Lane Asymmetric INT4xINT8 KV-Cache Dot-Product Engine // ============================================================================ // Microarchitecture Features: // 1. 4-Bank Interleaved On-Chip SRAM (4 Banks x 16 Rows x 32-bit = 512 INT4 KV) // 2. 4-Entry Elastic Ingress Skid/Prefetch FIFO with AXI4-Stream Slave Handshake // 3. Timing-Balanced 3-Stage Registered Pipeline with Global Backpressure Stall: // - Stage 1 (SRAM Fetch & Dequant): 4-Bank SRAM Read + INT4x8 Unpack + Asymmetric // Zero-Point Subtraction (deq_kv[i] = sext(kv[i]) - sext(zp)) // - Stage 2 (8-Lane MAC Tree): 8 Parallel 5x8 Signed Multipliers + Balanced // 8-Input Binary Adder Tree -> 16-Bit Signed Raw Dot-Product // - Stage 3 (Scale & Saturating Accumulator): Group Scale Multiply (16x9->25-bit) // + 33-Bit Extended Signed Accumulator with 32-Bit Saturation Clamp // 4. Hardware Performance & Telemetry Counters (MAC Tiles, Stalls, Bank Conflicts) // ============================================================================ `timescale 1ns/1ps module cv_x1_pro_subsystem ( input wire clk, input wire rst_n, // --- 4-Bank Interleaved SRAM Write Port --- input wire sram_we, input wire [5:0] sram_waddr, // [1:0]=bank_sel, [5:2]=row_addr input wire [31:0] sram_wdata, // 8 packed signed INT4 KV elements // --- AXI4-Stream Slave (Query Vector + Tile Control Descriptor) --- input wire s_axis_tvalid, output wire s_axis_tready, input wire [63:0] s_axis_tdata, // 8 packed signed INT8 Query elements input wire [19:0] s_axis_tuser, // [5:0]=kv_addr, [13:6]=scale, [17:14]=zp, [18]=clr, [19]=sat input wire s_axis_tlast, // --- AXI4-Stream Master (Accumulated Attention Score Output) --- output reg m_axis_tvalid, input wire m_axis_tready, output reg signed [31:0] m_axis_tdata, output reg m_axis_tlast, output reg [1:0] m_axis_tbank, // --- Telemetry & Status Outputs --- output reg [2:0] fifo_count, output reg sat_overflow_sticky, output reg [15:0] perf_mac_tiles, output reg [15:0] perf_stall_cycles, output reg [15:0] perf_bank_conflicts ); // ======================================================================== // 1. 4-Bank Interleaved On-Chip SRAM (4 Banks x 16 Rows x 32-Bit) // ======================================================================== reg [31:0] sram_bank0 [0:15]; reg [31:0] sram_bank1 [0:15]; reg [31:0] sram_bank2 [0:15]; reg [31:0] sram_bank3 [0:15]; wire [1:0] wr_bank = sram_waddr[1:0]; wire [3:0] wr_row = sram_waddr[5:2]; integer idx; // ======================================================================== // 2. 4-Entry Elastic Ingress FIFO (85 bits per entry: last[1]+user[20]+data[64]) // ======================================================================== reg [84:0] fifo_mem [0:3]; reg [1:0] fifo_wr_ptr; reg [1:0] fifo_rd_ptr; // Global downstream backpressure stall signal wire pipe_stall = m_axis_tvalid && !m_axis_tready; assign s_axis_tready = (fifo_count < 3'd4); wire fifo_push = s_axis_tvalid && s_axis_tready; wire fifo_pop = (fifo_count > 3'd0) && !pipe_stall; wire [84:0] fifo_head = fifo_mem[fifo_rd_ptr]; wire [63:0] head_qdata = fifo_head[63:0]; wire [19:0] head_tuser = fifo_head[83:64]; wire head_tlast = fifo_head[84]; wire [5:0] head_kv_addr = head_tuser[5:0]; wire [1:0] head_bank = head_kv_addr[1:0]; wire [3:0] head_row = head_kv_addr[5:2]; wire [7:0] head_scale = head_tuser[13:6]; wire signed [3:0] head_zp = head_tuser[17:14]; wire head_clr_acc = head_tuser[18]; wire head_sat_mode = head_tuser[19]; // ======================================================================== // 3. Stage 1 Combinational: 4-Bank SRAM Read & Asymmetric INT4 Zero-Point Sub // ======================================================================== reg [31:0] sram_rdata_mux; always @(*) begin case (head_bank) 2'd0: sram_rdata_mux = sram_bank0[head_row]; 2'd1: sram_rdata_mux = sram_bank1[head_row]; 2'd2: sram_rdata_mux = sram_bank2[head_row]; 2'd3: sram_rdata_mux = sram_bank3[head_row]; endcase end wire signed [3:0] kv0 = sram_rdata_mux[3:0]; wire signed [3:0] kv1 = sram_rdata_mux[7:4]; wire signed [3:0] kv2 = sram_rdata_mux[11:8]; wire signed [3:0] kv3 = sram_rdata_mux[15:12]; wire signed [3:0] kv4 = sram_rdata_mux[19:16]; wire signed [3:0] kv5 = sram_rdata_mux[23:20]; wire signed [3:0] kv6 = sram_rdata_mux[27:24]; wire signed [3:0] kv7 = sram_rdata_mux[31:28]; wire signed [4:0] zp_ext = {head_zp[3], head_zp}; wire signed [4:0] deq_kv0 = {kv0[3], kv0} - zp_ext; wire signed [4:0] deq_kv1 = {kv1[3], kv1} - zp_ext; wire signed [4:0] deq_kv2 = {kv2[3], kv2} - zp_ext; wire signed [4:0] deq_kv3 = {kv3[3], kv3} - zp_ext; wire signed [4:0] deq_kv4 = {kv4[3], kv4} - zp_ext; wire signed [4:0] deq_kv5 = {kv5[3], kv5} - zp_ext; wire signed [4:0] deq_kv6 = {kv6[3], kv6} - zp_ext; wire signed [4:0] deq_kv7 = {kv7[3], kv7} - zp_ext; // Stage 1 Pipeline Registers (40-bit packed dequantized KV + 64-bit Q + metadata) reg s1_valid; reg [39:0] s1_deq_kv_packed; reg [63:0] s1_q_packed; reg [7:0] s1_scale; reg s1_clr_acc; reg s1_sat_mode; reg s1_tlast; reg [1:0] s1_bank; // ======================================================================== // 4. Stage 2 Combinational: 8-Lane Parallel Multiply + Balanced Adder Tree // ======================================================================== wire signed [4:0] s1_dk0 = s1_deq_kv_packed[4:0]; wire signed [4:0] s1_dk1 = s1_deq_kv_packed[9:5]; wire signed [4:0] s1_dk2 = s1_deq_kv_packed[14:10]; wire signed [4:0] s1_dk3 = s1_deq_kv_packed[19:15]; wire signed [4:0] s1_dk4 = s1_deq_kv_packed[24:20]; wire signed [4:0] s1_dk5 = s1_deq_kv_packed[29:25]; wire signed [4:0] s1_dk6 = s1_deq_kv_packed[34:30]; wire signed [4:0] s1_dk7 = s1_deq_kv_packed[39:35]; wire signed [7:0] s1_q0 = s1_q_packed[7:0]; wire signed [7:0] s1_q1 = s1_q_packed[15:8]; wire signed [7:0] s1_q2 = s1_q_packed[23:16]; wire signed [7:0] s1_q3 = s1_q_packed[31:24]; wire signed [7:0] s1_q4 = s1_q_packed[39:32]; wire signed [7:0] s1_q5 = s1_q_packed[47:40]; wire signed [7:0] s1_q6 = s1_q_packed[55:48]; wire signed [7:0] s1_q7 = s1_q_packed[63:56]; wire signed [12:0] prod0 = {{8{s1_dk0[4]}}, s1_dk0} * {{5{s1_q0[7]}}, s1_q0}; wire signed [12:0] prod1 = {{8{s1_dk1[4]}}, s1_dk1} * {{5{s1_q1[7]}}, s1_q1}; wire signed [12:0] prod2 = {{8{s1_dk2[4]}}, s1_dk2} * {{5{s1_q2[7]}}, s1_q2}; wire signed [12:0] prod3 = {{8{s1_dk3[4]}}, s1_dk3} * {{5{s1_q3[7]}}, s1_q3}; wire signed [12:0] prod4 = {{8{s1_dk4[4]}}, s1_dk4} * {{5{s1_q4[7]}}, s1_q4}; wire signed [12:0] prod5 = {{8{s1_dk5[4]}}, s1_dk5} * {{5{s1_q5[7]}}, s1_q5}; wire signed [12:0] prod6 = {{8{s1_dk6[4]}}, s1_dk6} * {{5{s1_q6[7]}}, s1_q6}; wire signed [12:0] prod7 = {{8{s1_dk7[4]}}, s1_dk7} * {{5{s1_q7[7]}}, s1_q7}; wire signed [13:0] pair01 = {prod0[12], prod0} + {prod1[12], prod1}; wire signed [13:0] pair23 = {prod2[12], prod2} + {prod3[12], prod3}; wire signed [13:0] pair45 = {prod4[12], prod4} + {prod5[12], prod5}; wire signed [13:0] pair67 = {prod6[12], prod6} + {prod7[12], prod7}; wire signed [14:0] quad_lo = {pair01[13], pair01} + {pair23[13], pair23}; wire signed [14:0] quad_hi = {pair45[13], pair45} + {pair67[13], pair67}; wire signed [15:0] raw_dot_w = {quad_lo[14], quad_lo} + {quad_hi[14], quad_hi}; // Stage 2 Pipeline Registers reg s2_valid; reg signed [15:0] s2_raw_dot; reg [7:0] s2_scale; reg s2_clr_acc; reg s2_sat_mode; reg s2_tlast; reg [1:0] s2_bank; reg prev_pop_valid; reg [1:0] prev_pop_bank; // ======================================================================== // 5. Stage 3 Combinational: Group Scale Multiply + 33-Bit Saturating Accum // ======================================================================== wire signed [8:0] s2_scale_s = {1'b0, s2_scale}; wire signed [24:0] s2_scaled_dot = {{9{s2_raw_dot[15]}}, s2_raw_dot} * {{16{s2_scale_s[8]}}, s2_scale_s}; wire signed [31:0] acc_base = s2_clr_acc ? 32'sd0 : m_axis_tdata; wire signed [32:0] acc_ext_sum = {acc_base[31], acc_base} + {{8{s2_scaled_dot[24]}}, s2_scaled_dot}; wire pos_ovf = !acc_ext_sum[32] && acc_ext_sum[31]; wire neg_udf = acc_ext_sum[32] && !acc_ext_sum[31]; wire any_ovf = pos_ovf || neg_udf; wire signed [31:0] acc_next_val = (s2_sat_mode && pos_ovf) ? 32'sh7FFF_FFFF : (s2_sat_mode && neg_udf) ? -32'sh8000_0000 : acc_ext_sum[31:0]; // ======================================================================== // 6. Sequential State Update (FIFO, SRAM, 3-Stage Pipeline, Telemetry) // ======================================================================== always @(posedge clk or negedge rst_n) begin if (!rst_n) begin for (idx = 0; idx < 16; idx = idx + 1) begin sram_bank0[idx] <= 32'h0000_0000; sram_bank1[idx] <= 32'h0000_0000; sram_bank2[idx] <= 32'h0000_0000; sram_bank3[idx] <= 32'h0000_0000; end for (idx = 0; idx < 4; idx = idx + 1) begin fifo_mem[idx] <= 85'd0; end fifo_wr_ptr <= 2'd0; fifo_rd_ptr <= 2'd0; fifo_count <= 3'd0; s1_valid <= 1'b0; s1_deq_kv_packed <= 40'd0; s1_q_packed <= 64'd0; s1_scale <= 8'd0; s1_clr_acc <= 1'b0; s1_sat_mode <= 1'b0; s1_tlast <= 1'b0; s1_bank <= 2'd0; s2_valid <= 1'b0; s2_raw_dot <= 16'sd0; s2_scale <= 8'd0; s2_clr_acc <= 1'b0; s2_sat_mode <= 1'b0; s2_tlast <= 1'b0; s2_bank <= 2'd0; m_axis_tvalid <= 1'b0; m_axis_tdata <= 32'sd0; m_axis_tlast <= 1'b0; m_axis_tbank <= 2'd0; prev_pop_valid <= 1'b0; prev_pop_bank <= 2'd0; sat_overflow_sticky <= 1'b0; perf_mac_tiles <= 16'd0; perf_stall_cycles <= 16'd0; perf_bank_conflicts <= 16'd0; end else begin // --- SRAM Bank Write --- if (sram_we) begin case (wr_bank) 2'd0: sram_bank0[wr_row] <= sram_wdata; 2'd1: sram_bank1[wr_row] <= sram_wdata; 2'd2: sram_bank2[wr_row] <= sram_wdata; 2'd3: sram_bank3[wr_row] <= sram_wdata; endcase end // --- Ingress Elastic FIFO Push/Pop --- if (fifo_push) begin fifo_mem[fifo_wr_ptr] <= {s_axis_tlast, s_axis_tuser, s_axis_tdata}; fifo_wr_ptr <= fifo_wr_ptr + 2'd1; end if (fifo_pop) begin fifo_rd_ptr <= fifo_rd_ptr + 2'd1; prev_pop_valid <= 1'b1; prev_pop_bank <= head_bank; if (prev_pop_valid && (prev_pop_bank == head_bank)) begin perf_bank_conflicts <= perf_bank_conflicts + 16'd1; end end else if (!pipe_stall) begin prev_pop_valid <= 1'b0; end case ({fifo_push, fifo_pop}) 2'b10: fifo_count <= fifo_count + 3'd1; 2'b01: fifo_count <= fifo_count - 3'd1; default: fifo_count <= fifo_count; endcase // --- Telemetry: Backpressure Stall Counter --- if (pipe_stall) begin perf_stall_cycles <= perf_stall_cycles + 16'd1; end // --- 3-Stage Registered Pipeline Advance (Frozen on pipe_stall) --- if (!pipe_stall) begin // Stage 1 Latch (SRAM Read + Asymmetric Zero-Point Subtract) s1_valid <= fifo_pop; if (fifo_pop) begin s1_deq_kv_packed <= {deq_kv7, deq_kv6, deq_kv5, deq_kv4, deq_kv3, deq_kv2, deq_kv1, deq_kv0}; s1_q_packed <= head_qdata; s1_scale <= head_scale; s1_clr_acc <= head_clr_acc; s1_sat_mode <= head_sat_mode; s1_tlast <= head_tlast; s1_bank <= head_bank; end // Stage 2 Latch (8-Lane Parallel Multiply + Balanced Adder Tree) s2_valid <= s1_valid; if (s1_valid) begin s2_raw_dot <= raw_dot_w; s2_scale <= s1_scale; s2_clr_acc <= s1_clr_acc; s2_sat_mode <= s1_sat_mode; s2_tlast <= s1_tlast; s2_bank <= s1_bank; end // Stage 3 (Master Output & Saturating Accumulator) Latch if (s2_valid) begin m_axis_tvalid <= 1'b1; m_axis_tdata <= acc_next_val; m_axis_tlast <= s2_tlast; m_axis_tbank <= s2_bank; perf_mac_tiles <= perf_mac_tiles + 16'd1; if (s2_sat_mode && any_ovf) begin sat_overflow_sticky <= 1'b1; end end else if (m_axis_tvalid && m_axis_tready) begin m_axis_tvalid <= 1'b0; m_axis_tlast <= 1'b0; end end end end `ifdef FORMAL // ======================================================================== // 7. Formal Verification Properties (Yosys-SMTBMC + Z3 SMT Solver) // Scope: Proven across BMC (14 steps) and Temporal k-Induction (12 steps) // under initial reset (step 0: rst_n=0, step >=1: rst_n=1). // ======================================================================== reg f_past_valid = 1'b0; reg f_prev_rst_n = 1'b0; reg f_prev_m_valid = 1'b0; reg f_prev_m_ready = 1'b0; reg signed [31:0] f_prev_m_data = 32'sd0; reg f_prev_m_last = 1'b0; reg [1:0] f_prev_m_bank = 2'd0; // Full Stage 1 & Stage 2 payload + metadata shadow registers for P4 reg f_prev_s1_valid = 1'b0; reg [39:0] f_prev_s1_dk = 40'd0; reg [63:0] f_prev_s1_q = 64'd0; reg [7:0] f_prev_s1_scale = 8'd0; reg f_prev_s1_clr = 1'b0; reg f_prev_s1_sat = 1'b0; reg f_prev_s1_last = 1'b0; reg [1:0] f_prev_s1_bank = 2'd0; reg f_prev_s2_valid = 1'b0; reg signed [15:0] f_prev_s2_raw = 16'sd0; reg [7:0] f_prev_s2_scale = 8'd0; reg f_prev_s2_clr = 1'b0; reg f_prev_s2_sat = 1'b0; reg f_prev_s2_last = 1'b0; reg [1:0] f_prev_s2_bank = 2'd0; reg [1:0] f_prev_rd_ptr = 2'd0; reg f_prev_fifo_pop = 1'b0; reg f_prev_ovf_trig = 1'b0; reg f_prev_ovf_sticky = 1'b0; always @(posedge clk) begin f_past_valid <= 1'b1; f_prev_rst_n <= rst_n; f_prev_m_valid <= m_axis_tvalid; f_prev_m_ready <= m_axis_tready; f_prev_m_data <= m_axis_tdata; f_prev_m_last <= m_axis_tlast; f_prev_m_bank <= m_axis_tbank; f_prev_s1_valid <= s1_valid; f_prev_s1_dk <= s1_deq_kv_packed; f_prev_s1_q <= s1_q_packed; f_prev_s1_scale <= s1_scale; f_prev_s1_clr <= s1_clr_acc; f_prev_s1_sat <= s1_sat_mode; f_prev_s1_last <= s1_tlast; f_prev_s1_bank <= s1_bank; f_prev_s2_valid <= s2_valid; f_prev_s2_raw <= s2_raw_dot; f_prev_s2_scale <= s2_scale; f_prev_s2_clr <= s2_clr_acc; f_prev_s2_sat <= s2_sat_mode; f_prev_s2_last <= s2_tlast; f_prev_s2_bank <= s2_bank; f_prev_rd_ptr <= fifo_rd_ptr; f_prev_fifo_pop <= fifo_pop; f_prev_ovf_trig <= (!pipe_stall && s2_valid && s2_sat_mode && any_ovf); f_prev_ovf_sticky <= sat_overflow_sticky; end wire [1:0] f_ptr_diff = fifo_wr_ptr - fifo_rd_ptr; always @(posedge clk) begin if (!f_past_valid) begin assume(!rst_n); end else begin assume(rst_n); end if (rst_n) begin // P1: Elastic FIFO Bounds & Overflow/Underflow Freedom assert(fifo_count <= 3'd4); assert(!(fifo_push && !fifo_pop && (fifo_count == 3'd4))); assert(!(fifo_pop && (fifo_count == 3'd0))); // P2: FIFO Modular Pointer / Count Consistency Invariant assert(f_ptr_diff == fifo_count[1:0]); if (fifo_count == 3'd0 || fifo_count == 3'd4) begin assert(fifo_wr_ptr == fifo_rd_ptr); end // P5A: Combinational 32-Bit Signed Saturation Clamp & Wrap Correctness if (s2_sat_mode && pos_ovf) begin assert(acc_next_val == 32'sh7FFF_FFFF); end else if (s2_sat_mode && neg_udf) begin assert(acc_next_val == -32'sh8000_0000); end else begin assert(acc_next_val == acc_ext_sum[31:0]); end // P6A: Stage 1 Dequantized Value Range Invariant ([-15, +15]) assert(deq_kv0 >= -5'sd15 && deq_kv0 <= 5'sd15); assert(deq_kv7 >= -5'sd15 && deq_kv7 <= 5'sd15); end if (f_past_valid && f_prev_rst_n && rst_n) begin // P3: AXI4-Stream Master Handshake Hold Invariant (ARM IHI0051A Sec 2.2.1) if (f_prev_m_valid && !f_prev_m_ready) begin assert(m_axis_tvalid == 1'b1); assert(m_axis_tdata == f_prev_m_data); assert(m_axis_tlast == f_prev_m_last); assert(m_axis_tbank == f_prev_m_bank); end // P4: Complete Pipeline Stall Conservation Invariant (All Stage 1 & Stage 2 payload + metadata) if (f_prev_m_valid && !f_prev_m_ready) begin assert(s1_valid == f_prev_s1_valid); assert(s1_deq_kv_packed == f_prev_s1_dk); assert(s1_q_packed == f_prev_s1_q); assert(s1_scale == f_prev_s1_scale); assert(s1_clr_acc == f_prev_s1_clr); assert(s1_sat_mode == f_prev_s1_sat); assert(s1_tlast == f_prev_s1_last); assert(s1_bank == f_prev_s1_bank); assert(s2_valid == f_prev_s2_valid); assert(s2_raw_dot == f_prev_s2_raw); assert(s2_scale == f_prev_s2_scale); assert(s2_clr_acc == f_prev_s2_clr); assert(s2_sat_mode == f_prev_s2_sat); assert(s2_tlast == f_prev_s2_last); assert(s2_bank == f_prev_s2_bank); assert(fifo_rd_ptr == f_prev_rd_ptr); end // P5B: Sticky Saturation Overflow Trigger & Monotonic Retention if (f_prev_ovf_trig || f_prev_ovf_sticky) begin assert(sat_overflow_sticky == 1'b1); end // P6B & P7: Non-Stalled Stage-to-Stage Metadata Transfer & Forward Progress if (!(f_prev_m_valid && !f_prev_m_ready)) begin assert(s1_valid == f_prev_fifo_pop); assert(s2_valid == f_prev_s1_valid); if (f_prev_s1_valid) begin assert(s2_scale == f_prev_s1_scale); assert(s2_clr_acc == f_prev_s1_clr); assert(s2_sat_mode== f_prev_s1_sat); assert(s2_tlast == f_prev_s1_last); assert(s2_bank == f_prev_s1_bank); end if (f_prev_s2_valid) begin assert(m_axis_tvalid == 1'b1); assert(m_axis_tlast == f_prev_s2_last); assert(m_axis_tbank == f_prev_s2_bank); end end end end `endif endmodule