Difficulty: Medium · Puzzle 4 of 6 · Topic: Sequence Puzzles
Property intent: from one start cycle, both sub-sequences must match: req ##1 gnt and req ##2 done. Timeline (all other samples are 0): C40 start=1 req=1, C41 gnt=1, C42 done=1. Determine the verdict.
property p_seq_and;
@(posedge clk) start |-> ((req ##1 gnt) and (req ##2 done));
endpropertyFor sequence and, both sequences share a start but may end at different cycles.
1) start triggers and launches both sequence branches at C40.
2) First branch req ##1 gnt matches (req at C40, gnt at C41).
3) Second branch req ##2 done matches (req at C40, done at C42).
4) Both branches match, so the and composition matches, ending at the later end, C42.Answer: PASS - both sequence branches succeed from the same start cycle, satisfying the sequence and operator.
Checked by running the code in Verilator 5; the printed output supports the answer above. Both branches match from C40 (ending C41 and C42), so sequence and passes.
A common mistake is assuming both branches must end on the same cycle (that is intersect, not and). With and, the composite match ends when the later branch ends (C42 here).
If done moved to C43, which part would fail first and why? Model answer: the second branch (req ##2 done) fails first, at C42, because it needs done two cycles after req and done is still low. The first branch has already matched, but and needs both, so the property FAILS.
I would start both branches at C40. The first, req then gnt, matches at C41, and the second, req then two cycles to done, matches at C42. Both match from the same start, so the and passes, ending at the later branch end, C42. The trap is thinking both branches must end on the same cycle; that is intersect, not and, so I would check which one the spec wants.