Syntax at a glance
a != bHow it works
Inequality is true when its Boolean operands differ. It succeeds for 0 != 1 and 1 != 0, and fails when both operands are zero or both are one. For binary values, this behaves like an exclusive choice between the two conditions.
In req |-> (ack != retry), every request requires exactly one of ack and retry to be high in the same cycle. If both are high, inequality fails. If neither is high, it also fails. This differs from ack || retry, which allows both to be high.
As a standalone property, a != b must hold at every sample. For a = [0, 1, 0, 1], b = [1, 0, 1, 0] passes. Changing any b sample to match a makes the trace fail. Place inequality behind an implication if the relationship should hold only under an enable condition.
A comparison against history can detect a change: data != $past(data). At cycles after zero, this detects either direction of transition. At cycle zero, however, $past(data) is zero, so an initial high data makes the comparison true. Edge functions use a different initialization rule and are false at cycle zero.
The operator compares Boolean samples in this lab; it does not implement multibit arithmetic or four-state inequality. Use explicit parentheses when combining it with negation, AND, or OR to make the intended grouping clear.