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
01Causalitygrant has a requestNo orphan response02Deadlinerequest reaches grantBounded latency03Stabilityvalid and data holdBackpressure safe04Accountingone response per IDNo loss or duplication
One dense property can hide which obligation failed. Small contracts produce better diagnostics and compose cleanly.
Request, response, backpressure, payload, and outstanding state each need their own observable contract and failure message.Reference, examples and proof details
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.
Causality
No orphan response
Every response must have a legal outstanding cause.
Deadline
Bounded progress
Each admitted request receives a response within the specified sampled window.
Stability
Offer remains valid
Control and payload remain stable while the receiver applies backpressure.
Accounting
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.
The right property depends on whether request is held, pulsed, tagged, and allowed to overlap.
Protocol shape
Useful check
Limitation
Protocol shapereq held through gnt
Useful check$rose(gnt) |-> req
LimitationOnly valid when request is still asserted
Protocol shapeone pulsed req, bounded grant
Useful check$rose(gnt) |-> recent request history
LimitationHistory does not consume the request
Protocol shapesingle outstanding
Useful checkTrack outstanding bit
LimitationCannot represent multiple requests
Protocol shapeK outstanding
Useful checkCredit or pending counter
LimitationCounts do not prove identity
Protocol shapetagged outstanding
Useful checkID set or scoreboard
LimitationMust 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) disableiff (!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.
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: assertproperty ( @(posedge clk) disableiff (!rst_n)$rose(req) |->##[1:3]$rose(gnt));// Use ##[0:3] if same-edge grant is legal.
request
grant
bounded latency
overlap
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.
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.
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.
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.
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
typedeflogic [ID_W-1:0] tag_t;property p_tagged_response; tag_t saved_id; @(posedge clk) disableiff (!rst_n) ($rose(req), saved_id = req_id)|->strong(1'b1##[1:8] (rsp && rsp_id == saved_id));endpropertya_tagged_response:assertproperty (p_tagged_response);// Also enforce unique outstanding IDs, or use// a scoreboard for one-to-one and FIFO order.
