Difficulty: Hard · Puzzle 5 of 6 · Topic: Sequence Puzzles
Property intent: after a, a b within 1 to 3 cycles must be accompanied by c in the same cycle, but only the earliest b should be checked. Timeline (all other samples are 0): C10 a=1, C11 b=1 c=1, C13 b=1 (c=0 at C13). Evaluate both properties.
property p_all_matches;
@(posedge clk) (a ##[1:3] b) |-> c;
endproperty
property p_first_only;
@(posedge clk) first_match(a ##[1:3] b) |-> c;
endpropertyA ranged sequence in the antecedent can match more than once. Count the matches and where each one ends.
1) The antecedent a ##[1:3] b has two matches from the attempt at C10: one ending at C11 (##1) and one ending at C13 (##3).
2) p_all_matches: the implication spawns a consequent check for every antecedent match. c is checked at C11 (high, ok) and at C13 (low), so it FAILS, reported at C13.
3) p_first_only: first_match keeps only the earliest match (end C11), so only c at C11 is checked and the property PASSES.
4) Tool note: Verilator 5.048 does not report the C13 failure for a ranged antecedent, so this answer comes from the LRM semantics checked with an exact trace interpreter.Answer: p_all_matches FAILS (at C13), p_first_only PASSES - a ranged antecedent matches once per end point, and first_match keeps only the earliest.
Checked by running a model of the rule in Verilator 5 and a Python model. Verilator confirms the first_match form passes: only the match ending at C11 is checked. Verilator does not report the second match of a ranged antecedent, so this model of the LRM semantics shows both matches and the C13 failure.
Candidates read a ##[1:3] b as 'wait for the first b' and treat the second b as irrelevant. The antecedent spawns a separate consequent obligation for every match, so the late b at C13 needs c too. first_match is what limits it to one match.
If c were high at C11 and C13, what would each property report, and what if c were high only at C13? Model answer: with c at C11 and C13 both properties PASS (the plain form needs c at every match end, first_match only at C11). With c only at C13 both FAIL at C11, because the first match ends at C11 in both forms.
I would first note that the antecedent a followed by b within one to three cycles has two matches, ending at C11 and at C13. Without first_match, the implication checks c for every match, so c is fine at C11 but missing at C13 and the property fails at C13. With first_match only the earliest match counts, so only C11 is checked and it passes. The trap is treating the ranged antecedent as wait for the first b; I would next confirm whether the spec wants every b or only the first.