Difficulty: Hard · Puzzle 2 of 6 · Topic: Assertion Debug Puzzles
Property intent: when req_src rises in src_clk domain, ack_dst must be seen within 0 to 1 dst_clk edges. Timeline: req_src rises at S100, ack_dst pulses between D200 and D201 but is low at both sampled dst edges. Determine the verdict.
property p_multiclk_ack;
@(posedge src_clk) $rose(req_src)
|-> @(posedge dst_clk) ##[0:1] ack_dst;
endpropertyConsequent sampling occurs only at dst clock edges declared in the consequent clocking event.
1) Source-domain rise triggers the multiclock consequent.
2) ack_dst is evaluated only at D200 and D201 samples.
3) Pulse exists between edges but is not high at either sampled edge.
4) No legal match in ##[0:1] destination window.Answer: FAIL - asynchronous pulse is not captured at destination sampling edges, so acknowledgment is considered missing.
Candidates often debug RTL first, but the real issue is sampling visibility without pulse stretching/synchronization.
Would synchronizing ack_dst into src_clk or stretching pulse width fix this checker failure?