Difficulty: Hard · Puzzle 6 of 6 · Topic: Sequence Puzzles
Property intent: the ack then done response must complete inside the request window, which closes when end_win arrives 1 to 4 cycles after req. Timeline (all other samples are 0): C60 start=1 req=1, C63 ack=1, C64 done=1 end_win=1. Determine the verdict.
sequence resp_seq;
ack ##1 done;
endsequence
sequence win;
req ##[1:4] end_win;
endsequence
property p_within_win;
@(posedge clk) start |-> (resp_seq within win);
endpropertyCheck containment of the full resp sequence, and count the sampled cycles the window really covers.
1) start launches matching at C60. end_win is first high at C64, so win matches once: req at C60, ##4 end_win at C64, spanning C60 to C64 (5 sampled cycles, even though the range is [1:4]).
2) resp_seq: ack at C63, done at C64, so it spans C63 to C64.
3) within needs resp_seq to start no earlier than the window start and end no later than the window end. C63 >= C60 and C64 <= C64, so the boundary is inclusive and it is contained.
4) The property passes. A reader who takes the window as C60..C63 (4 cycles) wrongly fails it.
5) Tool note: Verilator 5.048 rejects this code (Unsupported: within with ranged cycle-delay operand). It only accepts fixed-delay windows such as req ##3 timeout, and for those it does not flag a response that ends after the window. Check within with a full SVA simulator or by reasoning.Answer: PASS - resp_seq (C63..C64) is enclosed by the one window that matches (C60..C64); the window end is inclusive.
Checked by running a model of the rule in Verilator 5 and a Python model. Verilator runs the fixed 4-cycle window (it rejects the ranged ##[1:4] form): resp_seq ending on the last window cycle is contained. A model of the LRM within rule for the ranged window: the response may end on the window's last cycle, but not one cycle later (the failing within case is model-only: Verilator misses a late window end).
##[1:4] means end_win may arrive up to 4 cycles after req, so the window spans up to 5 sampled cycles and both ends are inclusive. Counting a '4-cycle window' as C60..C63 gives a false FAIL on this waveform.
If done moved to C65 while end_win stayed at C64, what verdict would you expect? Model answer: FAIL. ack at C63 needs done at C64, so resp_seq never matches at all; even with ack at C64 and done at C65 the response would end one cycle after the only window end (C64), so containment fails.
I would first work out the window: req at C60, end_win at C64, so the matched window runs C60 to C64, five sampled cycles even though the range is one to four. The response, ack at C63 and done at C64, sits inside it, and the window end is inclusive, so the property passes. The trap is counting a four cycle window as C60 to C63 and reporting a false failure. I would check this one in a full simulator, since some free tools reject within with a ranged delay.