Syntax at a glance
a || bHow it works
Logical OR is true when at least one operand is true. It is inclusive: A || B also succeeds when both A and B are true. The only failing binary combination is A = 0 and B = 0.
For req |-> (ack || retry), each high request requires either acknowledgement or retry in the same cycle. A response with both signals high also satisfies this expression. If the design requires exactly one response, express that different requirement explicitly; with binary signals, ack != retry checks that they differ.
The placement of OR matters. In (a || b) |-> ready, either input can trigger a ready obligation. In a |-> (b || ready), only a triggers an obligation, and either b or ready can satisfy it.
For a same-cycle Boolean implication, !a || b is equivalent to a |-> b. If a is zero, !a makes the OR true. If a is one, b must be one. This equivalence explains why an assertion can receive a perfect match even when it uses different text from the reference. It does not remove delays from temporal implications.
AND binds more tightly than OR in the lab, so a || b && c groups as a || (b && c). Write (a || b) && c if both the disjunction and c are required. OR combines Boolean conditions at one sample; temporal sequence alternatives are outside the current grammar.