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 (all other samples are 0): 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 (reported at C91).Answer: FAIL - intersect demands simultaneous success at the same endpoint cycle, but c misses at C91.
Checked by running the code in Verilator 5; the printed output supports the answer above. intersect needs both branches to succeed with the same end point; c is low at C91, so it fails.
Engineers may glance at c=1 at C92 and incorrectly assume delayed recovery is acceptable. Both branches are fixed one-cycle delays, so C92 can never be an end point.
What operator would allow b and c to complete on different endpoints from the same start? Model answer: sequence and, for example (##1 b) and (##[1:2] c). Both branches start together and the composite ends at the later end, so b at C91 and c at C92 PASS.
I would check both branches from C90. The first, one cycle then b, succeeds at C91. The second, one cycle then c, checks c at C91 and it is low, so it fails, and the intersect fails at C91. Intersect needs both branches to succeed with the same start and end, and both are fixed one cycle delays, so c at C92 can never count. The trap is assuming a delayed recovery is acceptable. I would check whether the spec wanted and instead of intersect.