Q126FreeDesign Verification
Assert an integer square-root pipeline
Question
Check a 32-bit floor-square-root block with fixed 16-cycle latency, one outstanding request, and a backpressured response. Verify both protocol timing and the arithmetic result. LATENCY is a positive integer, default 16. Sample all known inputs at posedge clk. At most one request is outstanding, but an old due response may retire on the same edge that a new request is accepted. req_ready must be low while occupied unless that old response will be accepted on the current edge. If a request is accepted at C0, its response first appears in the sampled values at C_LATENCY, even if rsp_ready is low. Sampled active-low reset cancels the old request; unsolicited or early rsp_valid is illegal even while blocked.
Implementation scaffold
module sqrt_pipeline_checker #(
parameter int unsigned LATENCY = 16
) (
input logic clk,
input logic rst_n,
input logic req_valid,
input logic req_ready,
input logic [31:0] radicand,
input logic rsp_valid,
input logic rsp_ready,
input logic [15:0] root,
input logic [31:0] remainder
);
logic ghost_valid;
logic [31:0] ghost_x;
int unsigned cycles_left;
wire response_due = ghost_valid && cycles_left <= 1;
wire retiring = response_due && rsp_valid && rsp_ready;
initial assert (LATENCY >= 1) else $fatal(1, "LATENCY must be positive");
always_ff @(posedge clk) begin : track_request_and_response
// TODO: Apply sampled reset, check the old request and arithmetic, then capture any legal same-edge replacement.
end
property p_response_stable;
// TODO: Sampled-reset-disabled response stability through acceptance.
endproperty
a_response_stable: assert property (p_response_stable);
property p_blocked_then_accepted;
// TODO: Cover two blocked response samples followed by acceptance.
endproperty
property p_zero_request;
// TODO: Cover an accepted zero radicand.
endproperty
property p_maximum_request;
// TODO: Cover an accepted maximum 32-bit radicand.
endproperty
property p_perfect_square;
// TODO: Cover an accepted result with remainder zero.
endproperty
property p_near_square;
// TODO: Cover an accepted result with remainder one.
endproperty
c_blocked_then_accepted: cover property (p_blocked_then_accepted);
c_zero_request: cover property (p_zero_request);
c_maximum_request: cover property (p_maximum_request);
c_perfect_square: cover property (p_perfect_square);
c_near_square: cover property (p_near_square);
endmoduleTrace one case
accept radicand=27 at cycle0; response first asserts at cycle16 with root=5,remainder=2 and stalls until cycle18fixed latency PASS; arithmetic PASS; root/remainder/valid stable through acceptance at cycle18Five squared is 25 <= 27, six squared is 36 > 27, and remainder 27-25 is two; ready does not alter assertion latency.
Requirements
- Associate each accepted radicand with the response that first asserts exactly LATENCY cycles later, regardless of rsp_ready.
- Check root squared is at most the radicand and the next root squared is greater, using widened products that represent 65536 squared.
- Check remainder equals radicand minus root squared on every accepted response.
- Hold rsp_valid, root, and remainder stable throughout response stalls.
- Cancel pending latency obligations on reset and cover boundary, perfect-square, near-square, and stalled cases.