Q111FreeDesign Verification
Verify a rotated-table minimum finder
Interview prompt
Question
Implement legal-by-construction stimulus, a linear oracle, a one-request scoreboard, and exact-latency assertions for a rotated sorted-table minimum finder. The supplied transaction uses sixteen known unsigned 12-bit values and a 32-bit unsigned count. The generator creates legal counts only; drive invalid counts separately. Values in the active prefix are a cyclic rotation of a strictly increasing array. A response cannot bypass request acceptance, and req_ready remains low through the response-accepting edge, so the next request is accepted on a later edge. Reset is sampled at rising edges and cancels the checker's pending prediction.
Candidate starting point
Implementation scaffold
class rotated_table_item;
localparam int N=16, W=12;
rand int unsigned count;
rand int unsigned rotation;
rand logic [W-1:0] base[N];
logic [W-1:0] values[N];
constraint c_count {
// TODO: Legal count and independently chosen valid rotation.
}
constraint c_increasing {
// TODO: Strictly increasing active base values.
}
function void post_randomize();
// TODO: Implement this oracle or scoreboard method.
endfunction
endclass
function automatic void predict_min(
input logic [11:0] values[16],
input int unsigned count,
output bit bad_count,
output logic [11:0] min_value,
output logic [3:0] min_index
);
// TODO: Implement this oracle or scoreboard method.
endfunction
module rotated_min_checker (
input logic clk,rst_n,req_valid,req_ready,
input logic [31:0] count,
input logic [11:0] values[16],
input logic rsp_valid,rsp_ready,bad_count,
input logic [11:0] min_value,
input logic [3:0] min_index
);
bit min_pending;
bit expected_bad_count;
logic [11:0] expected_min_value;
logic [3:0] expected_min_index;
always @(posedge clk) begin
// TODO: Track reset and accepted transactions; compare/retire old responses first.
end
for (genvar c = 1; c <= 16; c++) begin : g_count_latency
localparam int L = 2 + $clog2(c);
property p_legal_latency;
// TODO: Implement this named temporal obligation.
endproperty
assert_legal_latency: assert property(p_legal_latency);
end
property p_invalid_latency;
// TODO: Implement this named temporal obligation.
endproperty
assert_invalid_latency: assert property(p_invalid_latency);
property p_rsp_stable;
// TODO: Implement this named temporal obligation.
endproperty
assert_rsp_stable: assert property(p_rsp_stable);
property p_no_bypass;
// TODO: Implement this named temporal obligation.
endproperty
assert_no_bypass: assert property(p_no_bypass);
property p_ready_blocked;
// TODO: Implement this named temporal obligation.
endproperty
assert_ready_blocked: assert property(p_ready_blocked);
property p_reset_cancels;
// TODO: Implement this named temporal obligation.
endproperty
assert_reset_cancels: assert property(p_reset_cancels);
final begin
// TODO: Reject incomplete outstanding work at test end.
end
endmoduleReviewed example
Trace one case
Input
sorted table=[1,3,5,8,11], randomized rotation=2Expected output
One valid result: rotated=[5,8,11,1,3], minimum_index=3A left rotation by two preserves cyclic order and places the original minimum at index three. Other rotation amounts remain valid stimulus.
What to cover
Requirements
- Generate a strictly increasing active base prefix base[0..count-1], choose a legal rotation independently, and copy the rotated active values into the request. Inactive base entries at indices count through 15 are outside the ordering requirement and do not participate in the rotated request; a count-one active value of 4095 must remain legal. The generator must permit every legal count/rotation pair, including count one, unrotated, and rotations one and count minus one when valid. The supplied harness calls randomize and drives directed boundary cases; implementing that driver loop is not part of this scaffold.
- Predict the minimum with a linear scan, independent of the DUT's likely binary search, and select the lowest physical index deterministically.
- Counts outside 1 through 16 return bad_count with zeroed results one cycle after acceptance; duplicates or unsorted data are out of contract and must not be overchecked.
- For legal count, assert first response exactly 2 + ceil(log2(count)) cycles after acceptance, keep req_ready low through and including the response-handshake edge, and hold the response under stall.
- Reset cancels pending work; identify count, rotation, minimum index, value extrema, stalls, latency, reset phase, and invalid-count classes as follow-up coverage.