Q072FreeDesign Verification
Verify signed maximum-product ranges
Question
Verify an accelerator that returns the maximum product over every nonempty contiguous range of signed factors. Build an exhaustive reference model, match tagged responses, and check protocol behavior. The supplied interface has a 4-bit ID, a 32-bit unsigned count, twelve signed 5-bit factors, a signed 61-bit result, and 4-bit endpoints. Counts 1 through 12 are legal; other counts set bad_count and zero every result field. Accepted IDs and inputs are known. Results may reorder by ID, but a response may be valid only for an already outstanding request, even when stalled or reporting bad_count. There is no same-edge response to a newly accepted request. Retire an old response before accepting a replacement with the same ID on that edge. Reset is sampled on rising edges and flushes the checker; the environment must prevent old responses from entering a later reset epoch through an external generation or quarantine policy. The supplied checker covers factor boundaries, counts, and response stalls; describe additional combinations in the test plan.
Implementation scaffold
typedef struct packed {
bit bad_count;
logic signed [60:0] product;
logic [3:0] first_idx;
logic [3:0] last_idx;
} product_expect_t;
function automatic product_expect_t predict_max_product(
input logic signed [4:0] factor[12],
input int unsigned count
);
// TODO: Implement this oracle or scoreboard method.
endfunction
module product_scoreboard_checker (
input logic clk, rst_n, req_valid, req_ready,
input logic [3:0] req_id,
input logic [31:0] count,
input logic signed [4:0] factor[12],
input logic rsp_valid, rsp_ready,
input logic [3:0] rsp_id,
input logic bad_count,
input logic signed [60:0] product,
input logic [3:0] first_idx, last_idx
);
product_expect_t pending_product[16];
logic [3:0] pending_count[16];
bit id_is_outstanding[16];
always @(posedge clk) begin
// TODO: Track reset and accepted transactions; compare/retire old responses first.
end
property p_legal_response_range;
// TODO: Implement this named temporal obligation.
endproperty
property p_rsp_stable;
// TODO: Implement this named temporal obligation.
endproperty
assert property (p_legal_response_range);
assert property (p_rsp_stable);
final begin
// TODO: Reject incomplete outstanding work at test end.
end
property p_req_stable;
// TODO: Implement this named temporal obligation.
endproperty
assert_req_stable: assert property(p_req_stable);
for(genvar i=0;i<12;i++)begin: g_factor_checks
wire signed [4:0] factor_at_index = factor[i];
property p_factor_stable;
// TODO: Implement this named temporal obligation.
endproperty
assert_factor_stable: assert property(p_factor_stable);
cover_factor_zero: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_factor_one: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_factor_minus_one: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_factor_min: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_factor_max: cover property (
// TODO: Cover this named accepted-transaction condition.
);
end
cover_invalid_low: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_invalid_high: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_full: cover property (
// TODO: Cover this named accepted-transaction condition.
);
cover_rsp_stall: cover property (
// TODO: Cover this named accepted-transaction condition.
);
endmoduleTrace one case
signed factors=[-2,3,-4]maximum_product=24; start=0; end=2The full range product is positive 24 and exceeds every shorter range; widened signed arithmetic avoids truncation.
Requirements
- Use an independent O(n²) oracle with 64-bit intermediate products.
- Break ties by lowest start index, then lowest end index; invalid count returns zero.
- Target zeros, ±1, extrema, sign changes, ties, and invalid counts.
- Match responses by ID, flush on reset, and define generation or quarantine behavior for ID reuse.
- Check payload stability, legal ranges, ordering, reset behavior, and coverage.