grant has a requestNo orphan responsePart 4 · Protocol patterns
SystemVerilog AssertionsReusable protocol assertion patterns
Decompose handshakes, backpressure, bounded response, serialization, and ordering into small properties with precise diagnostics.
Question directory
Questions for Protocol patterns
Open a question at its supporting explanation. The complete property reference stays directly above each answer set.
Protocol patternsHow do you check an exact request-to-acknowledge contract?→Protocol patternsHow do you guarantee every request is granted within three sampled cycles?→Protocol patternsHow do you block a second request until the prior grant, and what do until and until_with change?→Protocol patternsHow do you assert ready-valid stability under backpressure?→Protocol patternsHow do you fail a ready-valid stall that lasts more than five cycles?→Protocol patternsHow do you prove a grant never occurs without a request?→Protocol patternsCan a local-variable SVA prove tagged matching and FIFO order?→
06 · Protocol patternsDecompose one interface contract at a time.
Check causality, bounded response, stability, exclusivity, and ordering separately so a failure points to one broken rule instead of one dense property.
Concept modelA handshake is several independent obligations
request reaches grantBounded latencyvalid and data holdBackpressure safeone response per IDNo loss or duplicationOne dense property can hide which obligation failed. Small contracts produce better diagnostics and compose cleanly.
Always-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Protocol method
Split one interface requirement into independent obligations.
A handshake is not one rule. Check trigger shape, causality, response latency, response pulse, stability, admission, and accounting separately so each failure identifies one broken contract.
No orphan response
Every response must have a legal outstanding cause.
Bounded progress
Each admitted request receives a response within the specified sampled window.
Offer remains valid
Control and payload remain stable while the receiver applies backpressure.
No loss or duplication
Each accepted request is consumed by exactly one matching response.
Recipe 01
Exact two-cycle request and acknowledgement.
The request is a one-cycle pulse, acknowledgement rises exactly two samples later, acknowledgement is a one-cycle pulse, and no second request is admitted before completion.
Decomposed exact-latency handshakeSystemVerilog
a_req_one_cycle: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=> !req
);
a_ack_exact: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##2 $rose(ack)
);
a_ack_one_cycle: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(ack) |=> !ack
);
a_no_second_req: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=>
!$rose(req) until_with $rose(ack)
);
Recipe 02
Every request receives a grant within three sampled cycles.
Trigger once on the request edge and choose whether same-edge grant is legal. This property checks latency, not response ownership.
- Using req instead of $rose(req) launches a new attempt on every high sample.
- Overlapping requests create overlapping attempts.
- One grant event may satisfy several attempts. Add IDs, credits, or outstanding-state accounting when that reuse is illegal.
- The finite upper bound already catches ordinary lateness. strong matters mainly for unfinished or unbounded eventuality semantics.
Bounded request-to-grant latencySystemVerilog
a_req_granted: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] $rose(gnt)
);
// Use ##[0:3] if same-edge grant is legal.
Recipe 03
Block a second request until the prior grant.
Admission control is separate from response timing. Endpoint choice determines whether a new request is legal on the grant sample.
| Operator | Does p include q sample? | Must q eventually occur? |
|---|---|---|
p until q | No | No: weak |
p until_with q | Yes | No: weak |
p s_until q | No | Yes: strong |
p s_until_with q | Yes | Yes: strong |
Single-outstanding admission ruleSystemVerilog
a_single_outstanding: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=>
!$rose(req) until_with $rose(gnt)
);
Recipe 04
Hold valid and payload while stalled.
The accepting sample is valid && ready. While valid is high and ready is low, the source must preserve the offered transaction into the next sample.
- ready may legally be high before valid. That is not an error unless the protocol forbids it.
- After an accepting valid && ready sample, the source may drop valid or present a new back-to-back transfer according to the protocol.
- $rose(valid) is not always one transaction when valid remains high across back-to-back accepted transfers.
- Do not make ready progress part of the source stability property unless the system contract guarantees a sink deadline.
Ready-valid source obligationsSystemVerilog
a_hold_valid: assert property (
@(posedge clk) disable iff (!rst_n)
valid && !ready |=> valid
);
a_hold_payload: assert property (
@(posedge clk) disable iff (!rst_n)
valid && !ready |=> $stable(payload)
);
Recipe 05
Allow five stalled samples and fail on the sixth.
Define stall as valid && !ready. If five consecutive stall samples occur, require the next sample to resolve the stall.
| Sampled stall trace | Verdict | Reason |
|---|---|---|
S S S S S R | Pass | Five stalls, resolved on the sixth sample |
S S S S S S | Fail | The sixth consecutive stalled sample is illegal |
S S R | No failure | The five-sample antecedent never completes |
S S S ready=1 | No failure | Acceptance resolves the stall early |
Five-cycle maximum backpressureSystemVerilog
sequence s_stall;
valid && !ready;
endsequence
a_stall_at_most_five: assert property (
@(posedge clk) disable iff (!rst_n)
s_stall[*5] |=> !s_stall
);
Recipe 06
A grant needs a corresponding request model.
The right property depends on whether request is held, pulsed, tagged, and allowed to overlap.
| Protocol shape | Useful check | Limitation |
|---|---|---|
req held through gnt | $rose(gnt) |-> req | Only valid when request is still asserted |
one pulsed req, bounded grant | $rose(gnt) |-> recent request history | History does not consume the request |
single outstanding | Track outstanding bit | Cannot represent multiple requests |
K outstanding | Credit or pending counter | Counts do not prove identity |
tagged outstanding | ID set or scoreboard | Must handle reuse and duplicate responses |
Recipe 07
Correlation is not consumption, and first_match is not FIFO.
A local variable can correlate one request attempt with a matching response value. It cannot reserve or consume that response, so overlapping attempts can still share one event.
- first_match chooses the earliest endpoint within one attempt. It does not choose the globally oldest request.
- Unique live IDs can prove identity without requiring FIFO when out-of-order responses are legal.
- A scalar counter can prove balance and bounds, but not which request a response belongs to.
- For unbounded eventual response, strong handles end-of-simulation completion; formal liveness also needs justified fairness.
Correlation property plus accounting modelSystemVerilog
property p_matching_response;
logic [ID_W-1:0] saved_id;
@(posedge clk) disable iff (!rst_n)
($rose(req), saved_id = req_id)
|-> ##[1:8]
($rose(rsp) && rsp_id == saved_id);
endproperty
// For one-to-one or FIFO behavior:
// 1. push every accepted req_id into a reference queue
// 2. require rsp_id == queue.front() when FIFO is required
// 3. pop exactly once per accepted response
// 4. assert no response when the queue is empty
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
Split the contract into an exact response edge, response pulse shape, and admission rule. Separate properties produce clearer failures and let the interface decide whether a new request is legal on the acknowledgement edge.
Why it works
- $rose(req) |=> !req checks that request itself is a one-cycle sampled pulse.
- $rose(req) |-> ##2 $rose(ack) checks an acknowledgement edge exactly two sampled clocks later.
- $rose(ack) |=> !ack checks that acknowledgement is a one-cycle sampled pulse.
- If no request may arrive until acknowledgement, express that policy separately with until or explicit outstanding state and decide whether the endpoint permits a simultaneous new request.
- Add reverse causality or outstanding-state accounting when an unsolicited acknowledgement must also fail.
What the interviewer is testing
Whether you decompose latency, pulse width, and serialization instead of assuming one implication proves all three.
Common trap
A response-timing property alone does not reject an early extra acknowledgement or a second request.
Four diagnostic protocol checksSystemVerilog
a_req_one_cycle: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=> !req
);
a_ack_exact: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##2 $rose(ack)
);
a_ack_one_cycle: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(ack) |=> !ack
);
a_no_new_req: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=>
!$rose(req) until_with $rose(ack)
);
Strong answer
Trigger once on the request edge and allow a grant on any of the next three sampled edges: $rose(req) |-> ##[1:3] $rose(gnt). Use ##[0:3] if same-edge grant is legal. This checks latency, not transaction ownership.
Why it works
- Using req instead of $rose(req) launches a new attempt on every sampled cycle that request remains high.
- Overlapping requests create independent property attempts, which is correct for a pipelined timing requirement.
- One grant may satisfy several attempts unless an ID, credit, or outstanding-state model prevents event reuse.
- The finite three-cycle upper bound already catches normal lateness. strong is mainly relevant to unfinished or unbounded eventuality semantics.
What the interviewer is testing
Whether you can encode the deadline, decide if cycle zero is legal, and distinguish response timing from one-to-one accounting.
Common trap
Changing |-> to |=> shifts each consequent; it does not prevent overlapping requests.
Bounded request-to-grant timingSystemVerilog
a_req_granted: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] $rose(gnt)
);
// Use ##[0:3] if same-edge grant is legal.
Strong answer
Assert admission separately from response timing. $rose(req) |=> !$rose(req) until_with $rose(gnt) forbids a new request through and including the grant sample. Endpoint-excluding until permits same-edge readmission. Use a strong-until form when this property must also require grant eventually.
Why it works
- until and until_with are weak: the right-hand event is not required to occur. s_until and s_until_with require eventual completion.
- until excludes the endpoint from the left-hand requirement; until_with includes it.
- Pair admission control with a bounded grant property so serialization does not hide a missing response.
- For up to K outstanding requests, track a pending or credit count and assert its legal bounds instead of forbidding all overlap.
What the interviewer is testing
Whether you can separate admission, progress, endpoint policy, and outstanding capacity.
Common trap
An implication operator alone does not serialize property attempts or consume a grant.
Single-outstanding admission ruleSystemVerilog
a_single_outstanding: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |=>
!$rose(req) until_with $rose(gnt)
);
| Operator | Left side includes grant sample | Grant required |
|---|---|---|
until | No | No |
until_with | Yes | No |
s_until | No | Yes |
s_until_with | Yes | Yes |
Strong answer
When valid is sampled high and ready low, require valid to remain high and payload to remain stable on the next sampled clock. Repeating this one-step invariant on every stalled edge naturally holds the transaction until acceptance.
Why it works
- The accepting edge is valid && ready. The source must not withdraw or alter the offered transfer before that edge.
- Use case equality or explicit unknown checks when X or Z on control signals must be reported rather than treated optimistically.
- A separate bounded-stall property belongs to the system's forward-progress contract, not the source stability rule.
What the interviewer is testing
Whether you distinguish source obligations from sink progress and keep payload stable through the accepting sample.
Common trap
Checking only valid misses data corruption while stalled. Requiring ready to rise is invalid unless the environment guarantees progress.
Hold the offer through a stallSystemVerilog
a_hold_valid: assert property (
@(posedge clk) disable iff (!rst_n)
valid && !ready |=> valid
);
a_hold_payload: assert property (
@(posedge clk) disable iff (!rst_n)
valid && !ready |=> $stable(payload)
);
Strong answer
Treat valid && !ready as the stall condition. If it is true for five consecutive sampled clocks, require it to be false on the next sample. A shorter stall never completes the five-cycle antecedent, so it creates no failure.
Why it works
- The property checks the progress limit separately from the source's obligation to hold valid and payload stable.
- With a five-cycle maximum, the sixth consecutive stalled sample is the first illegal one.
- Only assert a sink-progress deadline if the architecture guarantees one; otherwise the environment may legally hold ready low forever.
What the interviewer is testing
Whether you can count the allowed stalled samples and distinguish bounded progress from data stability.
Common trap
Triggering only on valid can accidentally count cycles before backpressure begins or ignore a legal early valid withdrawal policy.
Resolve by the sixth sampled edgeSystemVerilog
sequence s_stalled;
valid && !ready;
endsequence
a_stall_at_most_five: assert property (
@(posedge clk) disable iff (!rst_n)
s_stalled[*5] |=> !s_stalled
);
Strong answer
If request remains asserted through grant, gnt |-> req is enough. If request is a pulse and grant may arrive later, track outstanding state or check a bounded request history. The property must match the protocol's ownership model.
Why it works
- A same-cycle expression cannot remember a one-cycle request that legitimately preceded grant.
- A bounded lookback window proves recent causality but does not consume a request or prevent duplicate grants.
- An outstanding bit, credit counter, or ID-indexed scoreboard can enforce one-to-one accounting when several transactions may be active.
What the interviewer is testing
Whether you recognize when a temporal lookback is enough and when the protocol needs explicit state.
Common trap
gnt |-> req falsely rejects a legal delayed grant when request is only a pulse.
Bounded recent-request checkSystemVerilog
logic [2:0] req_history;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) req_history <= '0;
else req_history <= {req_history[1:0], req};
end
a_grant_has_request: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(gnt) |->
(req || |req_history)
);
Strong answer
A property-local variable can capture a request tag separately for every attempt and require a later matching response. That proves value correlation for each attempt, but it does not consume a response. Reused tags or overlapping attempts can let one response satisfy several obligations, so one-to-one and FIFO order need explicit state or a scoreboard.
Why it works
- Declare the local variable with the exact interface tag type and assign it in a sequence match item.
- Require unique outstanding tags if the temporal property relies on tag identity alone.
- first_match chooses one endpoint within an attempt. It does not reserve that grant for the oldest request or stop another attempt from matching the same event.
What the interviewer is testing
Whether you understand attempt-local storage and the boundary between temporal correlation and transaction accounting.
Common trap
first_match(##[1:$] gnt) does not prove FIFO order for multiple in-flight requests.
Capture a tag, then state the limitationSystemVerilog
typedef logic [ID_W-1:0] tag_t;
property p_tagged_response;
tag_t saved_id;
@(posedge clk) disable iff (!rst_n)
($rose(req), saved_id = req_id)
|-> strong(1'b1 ##[1:8]
(rsp && rsp_id == saved_id));
endproperty
a_tagged_response:
assert property (p_tagged_response);
// Also enforce unique outstanding IDs, or use
// a scoreboard for one-to-one and FIFO order.