Syntax at a glance
req && !busyHow it works
Logical AND combines two Boolean expressions at the same sampled cycle. A && B is true only when both operands are true. Its binary truth table is 0 && 0 = 0, 0 && 1 = 0, 1 && 0 = 0, and 1 && 1 = 1. Parentheses make the grouping easier to read.
In (req && !busy) |-> ack, the antecedent selects requests made while the interface is not busy. If req is 1 and busy is 0, ack must be 1 in that cycle. If busy is 1, the trigger is false, so this property does not constrain ack.
AND can also combine requirements in the consequent. For req |-> ##2 (ack && ready), ack and ready must both be high at t+2. Having ack at t+1 and ready at t+2 is insufficient: both conditions must hold at the same endpoint.
A common mistake is using req && ack as a complete property when the requirement is conditional. A standalone Boolean property must hold at every sampled cycle, so req && ack rejects idle cycles. Another mistake is replacing AND with OR: req || !busy triggers in many more situations than req && !busy.
In this evaluator, negation and equality bind more tightly than AND, while OR binds less tightly. Write explicit parentheses when mixing them. This is Boolean conjunction over binary samples; sequence conjunction and multibit bitwise operations are outside the current subset.