Difficulty: Hard · Puzzle 3 of 6 · Topic: Assertion Debug Puzzles
Property intent: every req must be granted within 1 to 5 cycles. Directed test (all other samples are 0): C10 req=1, gnt never asserts, and the testbench calls $finish right after the C13 edge. What do p_weak and p_strong report at the end of simulation?
property p_weak;
@(posedge clk) req |-> ##[1:5] gnt;
endproperty
property p_strong;
@(posedge clk) req |-> strong(##[1:5] gnt);
endpropertyThe window of the C10 attempt runs C11..C15, but the simulation stops at C13. What happens to an attempt that is still waiting?
1) The C10 attempt has window C11..C15. At C13 the window has not closed and gnt has not been seen, so the attempt is still pending when simulation ends.
2) A sequence used as a property operand is weak by default: an attempt that has not completed at the end of the trace is not a failure. p_weak reports no failure.
3) strong(...) demands that the sequence actually complete. An attempt that never completes is a failure at the end of simulation, so p_strong FAILS (formal tools show it as an unproven or failing liveness-style obligation).
4) If the test had run to C15 both would fail at C15 for the closed window. Tool note: Verilator 5.048 rejects strong(); the weak result was confirmed there, the strong one follows the LRM.Answer: p_weak: no failure (the attempt is left pending); p_strong: FAIL at end of simulation - the grant never completed.
Checked by running a model of the rule in Verilator 5 and a Python model. Weak property, test stops after C13: the attempt is still pending and Verilator reports no failure. Same weak property but the test runs past the window: the failure is reported at C15. Verilator rejects strong(), so a model of the LRM weak/strong rule is used; its weak and full-window results match the two Verilator runs above.
A green log at the end of a short test does not mean the grant happened: with weak semantics the unfinished attempt just vanishes. Many testbenches stop a few cycles after the last stimulus and never see the window close.
When does the weak vs strong choice really matter, and what would you write for an open-ended grant? Model answer: for a bounded range the window eventually closes, so a long enough run fails the weak form too. For an unbounded wait, req |-> ##[1:$] gnt weak can never fail in a finite run, while strong(##[1:$] gnt) fails if gnt never comes before the end. Prefer a bounded range as a safety check, and use strong only when you want liveness (mainly in formal).
I would see that at the end of the test the window for the request at C10 has not closed, so the attempt is still pending. The plain property is weak, so an unfinished attempt is not a failure and it reports nothing. The strong version requires the grant to actually complete, so it fails at the end of simulation. The trap is a green log from a test that stopped too early. I would run the test past the window and keep the strong form for liveness style checks.