Difficulty: Medium · Puzzle 6 of 6 · Topic: Assertion Debug Puzzles
Property intent: one cycle after a rises, both b and c checks should align in the same endpoint cycle via intersect. Timeline: C90 a rises, C91 b=1 c=0, C92 c=1. Determine the verdict.
property p_dual_same_cycle;
@(posedge clk) $rose(a) |-> ((##1 b) intersect (##1 c));
endpropertyBoth intersect branches must end in the same cycle (here, both at C91).
1) $rose(a) at C90 triggers consequent.
2) ##1 b checks b at C91 and succeeds.
3) ##1 c checks c at C91 and fails because c=0 there.
4) intersect therefore fails immediately.Answer: FAIL - intersect demands simultaneous success at the same endpoint cycle, but c misses at C91.
Engineers may glance at c=1 at C92 and incorrectly assume delayed recovery is acceptable.
What operator would allow b and c to complete on different endpoints from the same start?