Q103FreeDesign Verification
Verify unique zero-sum triplets
Question
Complete the supplied checker for an accelerator that streams every unique sorted three-value combination whose widened sum is zero, in strict dictionary order. Parameters satisfy N=1..12 and W=1..32, defaulting to 12 each. The four-bit count may be invalid; active values are signed W-bit numbers and duplicate inputs are allowed. Observe signals immediately before updates at each rising edge; rst_n is known at every sampled edge. Known request fields are snapshotted on req_valid && req_ready, after at least one sampled reset. Inputs may then change. An output cannot belong to a request accepted on that same edge. rst_n=0 is a sampled cancellation of all checker and device work.

Implementation scaffold
module triplet_checker #(
parameter int N=12, W=12, FIRST_BOUND=32, GAP_BOUND=8
)(
input logic clk, rst_n, req_valid, req_ready,
input logic [3:0] count,
input logic signed [W-1:0] value[N],
input logic out_valid, out_ready, out_first, out_last, out_empty, out_error,
input logic signed [W-1:0] a,b,c
);
typedef struct { int signed a,b,c; } triplet_t;
triplet_t expected[$];
bit pending, expected_error, expected_empty, held;
int unsigned beat_index;
longint unsigned gap_age, total_age, total_bound;
logic [3*W+3:0] held_fields;
wire [3*W+3:0] output_fields={out_first,out_last,out_empty,out_error,a,b,c};
initial begin
if (N<1 || N>12 || W<1 || W>32 || FIRST_BOUND<1 || GAP_BOUND<1)
$fatal(1,"Require N=1..12, W=1..32 and positive progress bounds");
end
function automatic bit triplet_before(input triplet_t left,right);
// TODO: compare signed fields in dictionary order.
endfunction
function automatic void predict_triplets(
input logic signed [W-1:0] values[N], input int unsigned n,
output triplet_t result[$], output bit error_value, empty_value
);
// TODO: enumerate, widen, normalize, deduplicate and order; build special responses.
endfunction
task automatic check_cycle();
// TODO: implement sampled reset, ownership, held output, response and progress checks.
endtask
task automatic check_finished();
// TODO: report any unfinished owned stream.
endtask
always @(posedge clk) check_cycle();
final check_finished();
endmodule
Trace one case
Accept count=6 with [-1,0,1,2,-1,-4] at C0. out_ready=1 on C1 and C2.At C1 accept (-1,-1,2), FIRST=1, LAST=0; at C2 accept (-1,0,1), FIRST=0, LAST=1. EMPTY=ERROR=0 on both.The two normalized value triples are unique and dictionary ordered. req_ready remains low at C1 and C2; a new request may be admitted on a later edge.
Requirements
- Counts 0 through N are legal, including counts below three. Enumerate all distinct index triples, widen each operand to signed 64 bits before addition, sort each value triple, and deduplicate equal triples by values. Preserve duplicate input elements; they can supply distinct indices for repeated values in a legal triplet.
- Stream normal triples in strict signed dictionary order by a, then b, then c. Check FIRST only on the first beat and LAST only on the final beat. A legal request with no solutions owns one beat with FIRST=LAST=EMPTY=1, ERROR=0 and a=b=c=0. Count>N owns one beat with FIRST=LAST=ERROR=1, EMPTY=0 and a=b=c=0.
- Only one request may be active. Keep req_ready low through the final output acceptance; a new request can be accepted on a later edge. Retain out_valid and every payload/marker through a stall and its accepting edge. Reject any unowned out_valid, even when out_ready=0. Compare accepted outputs using four-state equality; reset cancels a held output.
- Count progress only on subsequent edges where out_ready=1; counters pause on out_ready=0. The first accepted beat is due by ready opportunity FIRST_BOUND (default 32), and every later beat within GAP_BOUND (default 8) further opportunities. Acceptance on the bound is legal. Total completion is due within FIRST_BOUND+(expected beat count-1)*GAP_BOUND opportunities. Both bounds are positive. Reset cancels deadlines; report unfinished work at end of test. Without response IDs, an identical stale response after a new request is indistinguishable, so reset must flush the device stream.
