Arithmetic verification answers two different questions. Does the RTL do exactly what the numeric contract says? And does that contract meet the accuracy target? A bit-exact integer model answers the first. A high-precision real model answers the second. Neither can stand in for the other.
Read the chart from the top: the same accepted inputs go to all three boxes in the second row, and each compare box has one job.
Exact compare: any difference in the 42-bit sum, the 16-bit code, the saturation flag or the out_valid cycle is a bug, however small.
Budget check: the real model measures how far the chosen rounding lands from the true value. It runs only on unclipped frames.
Report: a single PASS line plus maximum, mean and RMS error, so a regression in accuracy is visible even when it still passes.
Evidence | Scope |
|---|---|
Bit-exact integer model | Checks specified widths, rounding and saturation for the exercised transactions |
High-precision model | Checks output error against a stated budget, separating clipped results |
Boundary vectors | Exercise min/max, zero, ties and overflow; divide exceptions need divider-specific tests |
Varied constrained vectors | Exercise selected numerical combinations and traffic patterns |
Latency-aware scoreboard | Checks value and valid alignment through final drain |
Synthesis report | Separately establishes actual inference and implementation timing |
Quantity | Budget | Applies to |
|---|---|---|
Frame sum, output code, saturation flag | Exact match with the integer model | Every frame |
Clipped output | 32767 or -32768 with the flag set | Clipped frames only |
Output error against the real sum | At most 2^-16, half an output LSB (about 1.53e-5) | Unclipped frames |
| One pulse, one edge after the 1024th accepted input | Every cycle |
Input quantization, system tolerance | Separate budgets | Not covered by this bench |
The MAC accepts without backpressure. Completion becomes visible after the edge following the 1024th accepted input; the combinational quantizer adds no registered cycle. A downstream clocked consumer sees that qualified result at its next edge. For unclipped outputs the allowed error is 2^-16 relative to the exact sum of the stored samples. Clipped outputs must match the specified limits and saturation flag instead; input quantization and application-level clipping tolerance require separate budgets.
Three frames from the bench below, with the output in Q1.15 LSBs (one LSB is 2^-15). The budget is 0.5 LSB. Each column is a version of the quantizer: the correct nearest-even design, a half-up mutant, and a truncating mutant.
Frame: exact value | Nearest-even (correct) | Half-up mutant | Truncating mutant |
|---|---|---|---|
Frame 0: +0.5 LSB | 0, error 0.5 LSB: pass | 1, error 0.5 LSB: budget passes, exact compare fails | 0: pass |
Frame 1: -1.5 LSB | -2, error 0.5 LSB: pass | -1, error 0.5 LSB: budget passes, exact compare fails | -2: pass |
Frame 4: -9.48 LSB | -9: pass | -9: pass | -10, error 0.52 LSB: both checks fail |
Read across a row. The correct design lands exactly on the 0.5 LSB budget at the two ties, which is why the bench reports a maximum error of 2^-16. The half-up mutant moves the same ties the other way, by the same distance, so its error is also exactly 0.5 LSB and the budget check passes it. Only the exact compare against the integer model catches it. The truncating mutant is caught by both, because frame 4 is more than half an LSB from the truncated result.
The complete standalone example below joins the same frame_mac and signed_quantizer used earlier. Six frames exercise positive/negative ties, both clipping directions, deterministic varied samples, alternating extrema and bubbles. A 64-bit reference uses division toward zero and a sign-aware tie correction, independent of the DUT's floor/remainder implementation. A separate real-valued sum multiplies the interpreted Q1.15 inputs.
module frame_mac (
input logic clk, rst_n, in_valid,
input logic signed [15:0] a_i, b_i,
output logic out_valid,
output logic signed [41:0] frame_sum
);
logic v1_q;
logic signed [31:0] product_q;
logic signed [41:0] acc_q, next_sum;
logic [9:0] count_q;
assign next_sum = acc_q + product_q; // signed product extends to 42 bits
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
v1_q <= 1'b0;
out_valid <= 1'b0;
acc_q <= '0;
count_q <= '0;
frame_sum <= '0;
end else begin
v1_q <= in_valid;
out_valid <= 1'b0;
if (in_valid) product_q <= a_i * b_i;
if (v1_q) begin
if (count_q == 10'd1023) begin
frame_sum <= next_sum;
out_valid <= 1'b1;
acc_q <= '0;
count_q <= '0;
end else begin
acc_q <= next_sum;
count_q <= count_q + 1'b1;
end
end
end
end
endmodule
module signed_quantizer #(
parameter int IW = 42, OW = 16, F = 15
) (
input logic signed [IW-1:0] value_i,
output logic signed [OW-1:0] value_o,
output logic saturated_o
);
generate
if (IW < 2 || OW < 2 || OW > IW + 1 || F < 0 || F >= IW) begin : g_bad
$error("Require IW>=2, 2<=OW<=IW+1 and 0<=F<IW");
assign value_o = '0;
assign saturated_o = 1'b0;
end else begin : g_valid
localparam logic signed [IW:0] HI = $signed({1'b0, {(OW-1){1'b1}}});
localparam logic signed [IW:0] LO = $signed({1'b1, {(OW-1){1'b0}}});
logic signed [IW:0] floor_wide, rounded_wide;
logic round_up;
assign floor_wide = $signed({value_i[IW-1], value_i}) >>> F;
if (F == 0) begin : g_integer
assign round_up = 1'b0;
end else begin : g_fraction
localparam logic [F-1:0] HALF = {1'b1, {(F-1){1'b0}}};
wire [F-1:0] remainder_bits = value_i[F-1:0];
assign round_up = (remainder_bits > HALF) ||
((remainder_bits == HALF) && floor_wide[0]);
end
assign rounded_wide = floor_wide + $signed({{IW{1'b0}}, round_up});
always_comb begin
saturated_o = 1'b0;
if (rounded_wide > HI) begin
value_o = HI[OW-1:0]; saturated_o = 1'b1;
end else if (rounded_wide < LO) begin
value_o = LO[OW-1:0]; saturated_o = 1'b1;
end else value_o = rounded_wide[OW-1:0];
end
end
endgenerate
endmodule
Test one LSB below, at, and above every rounding and saturation boundary.
Track maximum absolute error, mean error, RMS error, and saturation frequency.
Run constant, impulse, alternating-extreme, and long random sequences.
Mutate one shift, sign extension, and valid delay to prove the testbench fails.
The bit-exact model proves implementation conformance; the high-precision model measures whether the chosen quantization architecture meets system-level accuracy.
Scope: six directed and varied frame checks. This is not a proof over all possible 1024-sample sequences, physical timing or a production accuracy qualification. The smaller quantizer sweep isolates rounding boundaries; the integration test checks the actual 42-bit path and output timing. Statistics describe this stimulus set only.
Run with Icarus Verilog 13.0 (2026-10-17): the bench prints PASS with a maximum unclipped error of 1.525879e-05 (2^-16). Two mutants of the quantizer were run on the same bench: half-up rounding failed the exact compare on frames 0 and 1 while staying inside the 2^-16 budget; truncation failed both checks on frame 4. Shift and valid-delay mutants were not run.