Syntax at a glance
req |=> ackHow it works
Non-overlapping implication adds one clock cycle between a Boolean antecedent and the start of its consequent. In A |=> B, if A is true at cycle t, B starts at cycle t+1. This differs from overlapping implication, |->, which starts at t.
For req |=> ack, req = [0, 1, 0, 0] and ack = [0, 0, 1, 0] pass. The request at cycle 1 requires acknowledgement at cycle 2. An acknowledgement only in the request cycle does not meet the next-cycle obligation.
In the lab's Boolean-antecedent subset, req |=> ack and req |-> ##1 ack express the same behavior. Explicit delays add to that implicit shift: req |=> ##2 ack requires ack three cycles after req, not two. This off-by-one distinction is a common source of errors.
As with overlapping implication, a false antecedent creates no obligation. Extra ack pulses are allowed, and each sampled high req independently creates a next-cycle check. A request that remains high for several cycles therefore creates several obligations. Use an edge function when only transitions should trigger.
A request on the final trace cycle cannot satisfy a next-cycle obligation within that trace. The evaluator fails it and Studio warns about the unresolved reference behavior. The current grammar supports Boolean antecedents; it does not implement the additional timing rules needed for temporal sequences in the antecedent.