Q046FreeDesign Verification
Prove an elastic one-hot checker
Question
Write a checker for a one-entry elastic pipeline that classifies a grant mask as one-hot and reports the selected index. Prove function, ordering, stability, and reset behavior under arbitrary backpressure. WIDTH is positive, defaults to 8, and the supplied local IDX_W represents indices 0 through WIDTH-1 with at least one bit. This is a registered slot with no combinational bypass: an input accepted at edge C becomes available immediately after C and is observed as out_valid at the next sampled edge until retirement. At every sampled edge, out_valid equals the pre-edge ghost occupancy. Inputs and handshake controls are known and stable for sampling. Active-low reset is sampled on the rising edge. End the test only after the slot drains.
Implementation scaffold
module elastic_onehot_checker #(
parameter int unsigned WIDTH=8,
localparam int unsigned IDX_W=(WIDTH<=1)?1:$clog2(WIDTH)
)(
input logic clk, rst_n, in_valid, in_ready,
input logic [WIDTH-1:0] grant_mask,
input logic out_valid, out_ready, is_onehot,
input logic [IDX_W-1:0] grant_index
);
function automatic bit onehot_ref(logic [WIDTH-1:0] mask);
logic [WIDTH-1:0] one = {{(WIDTH-1){1'b0}}, 1'b1};
// TODO: Implement onehot_ref using the supplied arguments and local state.
endfunction
function automatic logic [IDX_W-1:0] index_ref(
logic [WIDTH-1:0] mask
);
logic [IDX_W-1:0] idx = '0;
// TODO: Implement index_ref using the supplied arguments and local state.
endfunction
bit ghost_valid;
bit ghost_onehot;
logic [IDX_W-1:0] ghost_index;
always @(posedge clk) begin : sample_transactions
bit take_in;
bit take_out;
// TODO: Process reset and accepted transactions in the required order.
end
initial assert (WIDTH >= 1 && IDX_W >= ((WIDTH<=1)?1:$clog2(WIDTH)));
property p_rsp_stable;
// TODO: Implement this named temporal check or coverage condition.
endproperty
assert_rsp_stable: assert property (p_rsp_stable);
property p_replace;
// TODO: Implement this named temporal check or coverage condition.
endproperty
cover_replace: cover property (p_replace);
property p_zero_mask;
// TODO: Implement this named temporal check or coverage condition.
endproperty
cover_zero_mask: cover property (p_zero_mask);
for (genvar covered_bit = 0; covered_bit < WIDTH; covered_bit++) begin
property p_onehot_bit;
// TODO: Implement this named temporal check or coverage condition.
endproperty
cover_onehot_bit: cover property (p_onehot_bit);
end
property p_multihot;
// TODO: Implement this named temporal check or coverage condition.
endproperty
cover_multihot: cover property (p_multihot);
final begin : check_finished
// TODO: Reject unretired or incomplete obligations when the test ends.
end
endmoduleTrace one case
accept mask=5'b00100 and stall its output; on retirement simultaneously accept replacement mask=5'b00110first output onehot=1,index=2 stays stable; replacement output onehot=0,index=0The ghost queue preserves ordering across simultaneous retire-and-replace, and a two-bit mask is classified invalid with deterministic index zero.
Requirements
- Treat a mask as one-hot only when it is nonzero and mask AND mask-minus-one is zero, with width-controlled arithmetic.
- Associate each accepted input with the next accepted output, including simultaneous retire-and-replace.
- Return the sole set-bit index for legal masks and zero for zero or multi-hot masks.
- Require out_valid and payload stability while stalled and never allow accepted outputs to exceed accepted inputs since reset.
- Clear the ghost obligation on reset and cover zero, each one-hot bit, multi-hot values, and simultaneous handshakes.