Syntax at a glance
req |-> ackHow it works
Overlapping implication expresses a conditional obligation: if A is true at a sampled cycle, B must match starting at that same cycle. In A |-> B, A is the antecedent (the trigger) and B is the consequent (the required behavior). The lab evaluates the property at every cycle, so each true antecedent creates a separate obligation.
For a |-> b, consider a = [0, 1, 0, 1] and b = [1, 1, 0, 1]. This trace passes: b is high at cycles 1 and 3, exactly where a is high. The extra b at cycle 0 is allowed. Change b at cycle 3 to zero and the trace fails.
If a is never high, there is no obligation to violate and the implication passes vacuously. This is useful conditional behavior, but it does not prove that the trigger ever happens. Hidden tests include actual triggers and illegal responses to distinguish useful properties from assertions that accept everything.
Do not substitute a && b: that demands both signals at every cycle, rejecting legal idle cycles. Do not reverse the implication either: b |-> a asks a different question. For binary samples, !a || b is equivalent to a |-> b.
A delay in the consequent changes the required response time without changing the trigger: req |-> ##2 ack checks ack at t+2 after a request at t. By contrast, |=> contributes an additional cycle before the consequent starts.