// barrett_mul.v - Barrett modular multiplication (a * b mod Q)
//
// Computes product = a * b mod Q using Barrett reduction.
// Q = 3329, k = floor(2^24 / Q) = 5039
//
// Pure combinational, single-cycle latency.
// All multiplication widths explicitly controlled to avoid Verilog truncation.

module barrett_mul (
    input  [11:0] a,
    input  [11:0] b,
    output [11:0] product
);
    localparam Q = 3329;
    localparam K = 5039;   // floor(2^24 / 3329)
    localparam R = 24;

    // Full product: a * b (both < 3329, product < 11,082,241 < 2^24)
    // Force 24-bit evaluation by extending operand
    wire [23:0] p;
    assign p = {12'd0, a} * b;

    // Extend p to 37 bits for multiplication with K
    wire [36:0] p_ext;
    assign p_ext = {13'd0, p};

    // Compute t_shifted = (p * K) >> 24
    // Use explicit wire for the product to control width
    /* verilator lint_off UNUSEDSIGNAL */
    wire [36:0] t_product;
    /* verilator lint_on UNUSEDSIGNAL */
    assign t_product = p_ext * K;
    wire [12:0] t_shifted;
    assign t_shifted = t_product[36:R];

    // q_approx = t_shifted * Q
    wire [24:0] q_approx;
    assign q_approx = t_shifted * Q;

    // r = p - q_approx
    wire [24:0] r0;
    assign r0 = {1'b0, p} - q_approx;

    // Conditional subtract Q (at most twice)
    wire [24:0] r1;
    assign r1 = (r0 >= Q) ? (r0 - Q) : r0;

    wire [11:0] r2;
    assign r2 = (r1[11:0] >= Q) ? (r1[11:0] - Q) : r1[11:0];

    assign product = (r1 >= Q) ? r2 : r1[11:0];

endmodule