Handshake Drills

Drill 1 — ack exactly N cycles after req

Problem

Interviewer: 'We have a request/acknowledge pair. Whenever req rises, ack must be asserted exactly 3 cycles later — not earlier, not later. Write the assertion.'

Think it through

• 'Whenever req rises' — edge-triggered antecedent, so $rose(req), not the raw level req. A level antecedent would start a fresh attempt every cycle req stays high.

• 'Exactly 3 cycles later' — a fixed delay: ##3. A range ##[1:3] would accept early acks, which the spec forbids.

• 'Not earlier' — strictly, ##3 ack only checks cycle T+3; if early ack must also be illegal, add a second property (drill variation below).

• Sampled on a clock, disabled during reset — disable iff (!rst_n).

property p_ack_exact3;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##3 ack;
endproperty
a_ack_exact3: assert property (p_ack_exact3)
  else $error("ack not asserted exactly 3 cycles after req rise");

PASS trace                          FAIL trace
cycle :  0  1  2  3  4  5           cycle :  0  1  2  3  4  5
req   :  0  1  1  0  0  0           req   :  0  1  1  0  0  0
ack   :  0  0  0  0  1  0           ack   :  0  0  0  1  0  0

$rose(req) at cycle 1.              $rose(req) at cycle 1.
Consequent checks ack at 1+3 = 4.   ack high at cycle 3, low at cycle 4.
ack == 1 at cycle 4  → PASS         Assertion FAILS at cycle 4.
(only ONE attempt: edge antecedent  (note: the early ack at cycle 3 is
 fired once, at cycle 1)             NOT itself flagged by this property)

Variation — ack within a window [2:5], and no early ack

Follow-up: 'Now the spec says ack arrives between 2 and 5 cycles after req, and must NOT appear in the first cycle.' Two properties: a window for the arrival, and a no-early check.

// arrival window: 2 to 5 cycles after the rise
property p_ack_window;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[2:5] ack;
endproperty

// no early ack in the cycle right after req
property p_no_early_ack;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |=> !ack [*0:0] or (!ack ##1 1);  // overkill — see simple form
endproperty
// Simple and preferred:
property p_no_early_ack_simple;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |=> !ack;   // cycle T+1 must not have ack
endproperty

Common wrong answers

• req |-> ##3 ack — level antecedent: a req held high 4 cycles spawns 4 attempts, each demanding its own ack 3 cycles later. One real ack, three false failures.

• $rose(req) |=> ##3 ack — |=> already advances one cycle, so this checks cycle T+4. Classic off-by-one.

• $rose(req) |-> ##[1:3] ack — accepts ack at T+1 or T+2; 'exactly' became 'within'. Read the spec word.

Drill 2 — req stays stable (held high) until ack

Problem

Interviewer: 'Once req is asserted, it must stay asserted until ack is received. req and ack may overlap in the final cycle. Write it.'

Think it through

• This is a stability-until-event requirement: until_with is the textbook operator (the condition must hold up to AND including the cycle ack arrives).

• until would require req high strictly BEFORE the ack cycle — req could legally drop in the ack cycle itself. The spec says they overlap, so until_with.

• An equivalent one-cycle invariant exists: 'req high and no ack means req still high next cycle'. Interviewers love seeing you know both.

// Form 1: until_with — reads like the spec
property p_req_stable;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> req until_with ack;
endproperty

// Form 2: equivalent local invariant — no temporal depth
property p_req_stable_inv;
  @(posedge clk) disable iff (!rst_n)
  (req && !ack) |=> req;
endproperty

PASS trace                          FAIL trace
cycle :  0  1  2  3  4  5           cycle :  0  1  2  3  4  5
req   :  0  1  1  1  1  0           req   :  0  1  1  0  0  0
ack   :  0  0  0  0  1  0           ack   :  0  0  0  0  1  0

req rises at 1, ack at 4.           req drops at cycle 3 with no ack yet.
req high cycles 1..4 inclusive      Form 1 FAILS: req not held until ack.
(overlaps with ack)  → PASS         Form 2 FAILS at cycle 3:
                                    (req && !ack) at 2, but !req at 3.

Variation — req must DROP in the cycle after ack

property p_req_drops_after_ack;
  @(posedge clk) disable iff (!rst_n)
  (req && ack) |=> !req;
endproperty
// Pairs with p_req_stable: together they pin down the whole req lifetime.

Common wrong answers

• $rose(req) |-> req until ack — until excludes the ack cycle; legal overlapping-drop traces now fail, and a same-cycle req/ack pulse is mishandled.

• $rose(req) |-> req throughout ack[->1] — actually correct and a nice alternative, but candidates often write throughout ack (no [->1]), which is not a sequence end-point and checks nothing useful.

• Forgetting that until/until_with are WEAK: if ack never arrives, the property passes at end of simulation. If the spec demands ack eventually arrives, that is a separate liveness property (s_until_with in formal, bounded window in sim).

Drill 3 — no new req until previous ack

Problem

Interviewer: 'req is a one-cycle pulse. After a request is launched, the master must not issue another request pulse until ack has been seen. Write the assertion.'

Think it through

• Pulse protocol — so a 'new request' is a fresh rise: $rose(req).

• The forbidden window opens the cycle after the pulse and closes when ack arrives. 'No new rise until ack' — until again, and here plain until is right: a new req in the SAME cycle as ack is usually legal (back-to-back).

• Start checking from the cycle after the pulse (|=>), otherwise the original rise would violate its own check.

property p_no_new_req;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |=> (!$rose(req)) until ack;
endproperty
a_no_new_req: assert property (p_no_new_req);

PASS trace                          FAIL trace
cycle :  0  1  2  3  4  5           cycle :  0  1  2  3  4  5
req   :  0  1  0  0  0  1           req   :  0  1  0  1  0  0
ack   :  0  0  0  0  1  0           ack   :  0  0  0  0  1  0

Pulse at 1; window is 2..3          Second rise at cycle 3, but ack
(cycles strictly before ack at 4).  not seen until 4. FAIL at cycle 3.
No rise in 2..3; new req at 5 is
after ack  → PASS

Variation — allow exactly one outstanding, count-based

Follow-up: 'What if up to 2 requests may be outstanding?' Pure sequence operators get painful; switch to an auxiliary counter — covered in depth in the Counting & Window drills. Knowing WHEN to abandon pure SVA for modeling code is a senior signal.

Common wrong answers

• $rose(req) |=> !req until ack — forbids the LEVEL, not a new rise. Equivalent here only because req is a 1-cycle pulse; breaks the moment req can legally stay high.

• $rose(req) |-> !$rose(req) until ack — with |-> the check starts in the rise cycle itself, where $rose(req) is true → instant self-contradiction unless ack overlaps.

• Using until_with — would also forbid a back-to-back request in the ack cycle, which this spec permits.

Drill 4 — ack never without req

Problem

Interviewer: 'The slave must never acknowledge when there is no request outstanding. Write the check — first for a level-held req, then tell me what changes for a pulsed req.'

Think it through

• Level-held req: trivial same-cycle invariant, ack |-> req. No temporal operators needed — do not over-engineer.

• Pulsed req: req is long gone by the time ack arrives, so the pin alone cannot tell you whether a request is outstanding. You need a tracking flag (auxiliary state).

• Auxiliary modeling code next to the assertion is normal and expected — it is not cheating.

// Level protocol: one line
a_no_orphan_ack: assert property (
  @(posedge clk) disable iff (!rst_n) ack |-> req);

// Pulse protocol: track 'outstanding' with aux state
logic outstanding;
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n)        outstanding <= 1'b0;
  else if (req)      outstanding <= 1'b1;   // pulse launches
  else if (ack)      outstanding <= 1'b0;   // ack retires
end

a_no_orphan_ack_pulse: assert property (
  @(posedge clk) disable iff (!rst_n)
  ack |-> (outstanding || req));   // req: same-cycle launch+ack corner

FAIL trace (pulse protocol, orphan ack)
cycle       :  0  1  2  3  4  5
req         :  0  1  0  0  0  0
ack         :  0  0  0  1  0  1   ← second ack at 5
outstanding :  0  0  1  1  0  0

ack at 3: outstanding==1 → PASS.
ack at 5: outstanding==0 and req==0 → FAIL. Orphan ack caught.

Common wrong answers

• ack |-> $past(req) — only looks back exactly one cycle; an ack 3 cycles after the pulse passes nothing.

• ack |-> req for a pulse protocol — fails on every legitimate delayed ack; candidate confused level and pulse semantics.

• Putting the aux flag update inside the property — local variables cannot persist ACROSS attempts; cross-attempt state must live in procedural code.

Key takeaways

• Edge antecedent ($rose) for pulse events; level antecedent only when each high cycle truly restates the obligation.

• until_with includes the terminating cycle, until excludes it — pick from the spec's overlap rule, and say so out loud.

• When the pin no longer carries the protocol state (pulse protocols, multiple outstanding), add auxiliary modeling state and assert on that.

Common pitfalls

• req |-> ... on a held request — one attempt per high cycle, false failures or huge attempt storms.

• |=> stacked with ##N — double delay; count the cycles on a drawn trace before declaring done.

• Weak until/until_with silently pass if the terminating event never comes — pair with a bounded-arrival property when the spec requires delivery.

• Forgetting disable iff (!rst_n) — reset glitches on req/ack become assertion noise that masks real bugs.