Difficulty: Medium · Puzzle 6 of 6 · Topic: Implication Puzzles
Property intent: if either request source rises, grant must follow one cycle later. Timeline: C40 req_a stable 0, req_b rises 0->1 at C40, C41 grant=1. Determine the verdict.
property p_or_antecedent;
@(posedge clk) ($rose(req_a) or $rose(req_b)) |-> ##1 grant;
endpropertyOnly one side of the OR needs to trigger the implication.
1) At C40, $rose(req_b) is true while $rose(req_a) is false.
2) OR antecedent is therefore true, so a checking thread is spawned.
3) ##1 grant requires grant at C41.
4) grant is high at C41, satisfying the consequent.Answer: PASS - a valid antecedent trigger occurs via req_b, and grant meets the one-cycle-later requirement.
Under pressure, candidates may incorrectly treat OR antecedent as needing both rises in the same cycle.
If neither request rose, what exact verdict label should this property report?