Difficulty: Hard · Puzzle 2 of 6 · Topic: Assertion Debug Puzzles
Property intent: when req_src rises in the src_clk domain, ack_dst must be seen within 0 to 1 dst_clk edges. dst_clk runs about 3x faster than src_clk. ack_dst is a dst_clk-domain register: it only changes just after a dst_clk edge and is cleanly sampled at the next one. Timeline: req_src is sampled rising at S100. The first dst_clk edge after S100 is D200, then D201, D202 and D203; S101 falls between D202 and D203. ack_dst is high only at D202 (low at D200, D201, D203). Determine the verdict.
property p_multiclk_ack;
@(posedge src_clk) $rose(req_src)
|-> @(posedge dst_clk) ##[0:1] ack_dst;
endproperty##[0:1] counts ticks of the clock in force at that point of the consequent. Which clock is that, and how many of its edges fit in the window?
1) The source-domain rise at S100 starts the consequent, which switches to dst_clk; its first tick is D200, the first dst edge after S100.
2) ##[0:1] counts dst_clk edges, so the window is D200 and D201 only.
3) ack_dst is low at both of those samples. It goes high at D202, one dst edge too late.
4) No legal match in the window, so the property FAILS. Counting the window as one src_clk cycle (D200..D202) would wrongly pass it.
5) Tool note: multiclock properties are not supported by every free tool (Verilator 5.048 has no multiclock support); this verdict comes from the LRM clocking rules.Answer: FAIL - the window is two dst_clk edges (D200, D201), and ack_dst arrives at D202, one dst edge late.
Not run here: Multiclock property: Verilator 5.048 has no multiclock sequence support and the free simulators cannot sample two clock domains faithfully, so the verdict rests on the LRM clocking rules.. The answer follows the language rules and the solution steps above.
The delay range is in dst_clk cycles, not src_clk cycles. With dst_clk about 3x faster the window is roughly two thirds of a src cycle, so an ack that looks 'within one cycle' by src_clk standards is already late for this checker. Debuggers who fix the RTL first miss that the bound is in the wrong unit.
If the spec allows the ack up to one full src_clk cycle after the rise, what is the fix? Model answer: change the bound to count dst edges in that period (here ##[0:2], after confirming the clock ratio and boundary alignment), or move the check to src_clk using a synchronised copy of ack_dst and include the synchroniser latency in the bound. Stretching the pulse or synchronising in the DUT changes the design, not the checker.
I would count in destination clock edges, not source ones. The consequent switches to the destination clock, whose first edge after the source rise is D200, so the zero to one window is D200 and D201. The ack is low at both and goes high at D202, one edge late, so the property fails. The trap is counting the window in source clock cycles, which would wrongly pass it. I would check that the bound is in the right unit before touching the RTL.