Difficulty: Hard · Puzzle 6 of 6 · Topic: Sequence Puzzles
Property intent: ack ##1 done must complete within either a 4-cycle or 5-cycle request window. Timeline: C60 start=1 req=1, C62 ack=1, C63 done=1, C64 end_win=1. Determine the verdict.
sequence resp_seq;
ack ##1 done;
endsequence
sequence win4;
req ##[1:4] end_win;
endsequence
sequence win5;
req ##[1:5] end_win;
endsequence
property p_within_or;
@(posedge clk) start |-> (resp_seq within (win4 or win5));
endpropertyCheck containment of the full resp sequence, not just ack.
1) start launches matching at C60.
2) resp_seq spans C62 to C63.
3) win4 can match as req at C60 and end_win at C64, spanning C60 to C64.
4) resp_seq is fully contained inside that window; or is satisfied by win4 alone.Answer: PASS - resp_seq is fully enclosed by a valid request window, so within succeeds via the win4 branch of the or composition.
Engineers often evaluate only start alignment and forget that within requires full-sequence containment.
If done moved to C65 while end_win stayed at C64, what verdict would you expect?