|-> vs |=>

The antecedent/consequent model

An implication property has two halves: the antecedent (left), a sequence acting as the trigger, and the consequent (right), a sequence or property stating the obligation. The evaluation contract: at every clock tick an attempt starts; if the antecedent does not match from that tick, the attempt passes vacuously (next lesson). If the antecedent matches — possibly on several threads — the consequent must hold from EACH match's endpoint. The two implication operators differ only in where the consequent clock starts relative to that endpoint.

// Overlapped: consequent starts ON the antecedent end cycle
property p_ovl;
  @(posedge clk) req |-> gnt;        // gnt same cycle as req
endproperty

// Non-overlapped: consequent starts the NEXT cycle
property p_novl;
  @(posedge clk) req |=> gnt;        // gnt one cycle after req
endproperty

a_ovl:  assert property (p_ovl);
a_novl: assert property (p_novl);

Identical waveforms, different verdicts

The classic interview discriminator: one stimulus, both operators. |-> fuses the consequent onto the antecedent endpoint (it is ##0 at the property boundary); |=> inserts one tick (##1).

STIMULUS A — gnt in the SAME cycle as req

clk :  1    2    3    4
req :  0    1    0    0
gnt :  0    1    0    0
            A
req |-> gnt : consequent checked at tick 2 → gnt=1 → PASS
            P
req |=> gnt : consequent checked at tick 3 → gnt=0 → FAIL
                 F

STIMULUS B — gnt one cycle AFTER req

clk :  1    2    3    4
req :  0    1    0    0
gnt :  0    0    1    0
            A
req |-> gnt : checked at tick 2 → gnt=0 → FAIL at tick 2
            F
req |=> gnt : checked at tick 3 → gnt=1 → PASS
                 P

Same RTL, opposite verdicts — the operator IS the spec.

With a multi-cycle antecedent the rule reads from the antecedent's end tick: in (req ##1 ack) |-> done, done is checked on the ack cycle; with |=> it is checked one tick after ack.

The equivalence: |=> is |-> ##1

The two operators are not independent primitives: a |=> b is exactly a |-> ##1 b. This matters practically — any non-overlapped check can be rewritten overlapped with an explicit delay, which is the form you need when the consequent delay is data-dependent or ranged. The reverse direction also works: a |-> b equals a ##1 1 |=> b only with contortions — so |-> is the more primitive operator; treat |=> as convenient sugar for the common one-cycle case.

// These two are IDENTICAL in meaning:
property p_sugar;    @(posedge clk) req |=> gnt;       endproperty
property p_desugar;  @(posedge clk) req |-> ##1 gnt;   endproperty

// The desugared form generalizes; the sugar does not:
property p_window;   @(posedge clk) req |-> ##[1:3] gnt; endproperty
// There is no "|=> [0:2]" — ranged consequents use |-> ##[M:N].

WAVEFORM — req |=> gnt  ≡  req |-> ##1 gnt

clk :  1    2    3    4    5
req :  0    1    0    0    0
gnt :  0    0    1    0    0
            A    M
Both forms: antecedent ends @2, one tick inserted, gnt
required @3 → identical attempt, identical match tick,
identical failure reporting. Tools display both the same way.

Choosing between them in protocols

Decision guide

• Spec says "in the same cycle" (combinational guarantee, e.g. valid && ready handshake rules): |->.

• Spec says "on the next cycle" (registered response, pipelined grant): |=>.

• Spec gives a window ("within 1 to 3 cycles"): |-> ##[1:3] — overlapped plus explicit range.

• Consequent must observe the same data the antecedent saw: |-> with $past, or sample into local variables (later topic); |=> shifts the observation point and often forces $past arithmetic.

• Chained phase checks where the next phase begins on the end cycle of the previous: |-> mirrors the ##0 fusion of sequence land.

Interview angle

• "Difference between |-> and |=>?" — same-cycle vs next-cycle consequent start, measured from the antecedent END tick. Then draw stimulus A/B above; the waveform is the expected proof.

• "Rewrite a |=> b without |=>." — a |-> ##1 b. Instant follow-up: "and a window of 2 to 4?" — a |-> ##[2:4] b.

• "Multi-cycle antecedent — where does the consequent start?" — from the antecedent endpoint, not its first cycle; many candidates miss this.

• "Which is 'overlapped' and why the name?" — |->: the consequent's first observation overlaps the antecedent's last cycle.

Key takeaways

• |-> checks the consequent starting ON the antecedent's end tick; |=> starts one tick later.

• a |=> b is precisely a |-> ##1 b — |-> plus explicit delays is the general form.

• Consequent timing is measured from the antecedent ENDPOINT, not from its first cycle.

• Pick the operator from the spec's wording: same-cycle wording → |->, next-cycle wording → |=>.

Common pitfalls

• Writing |=> for a same-cycle ready/valid rule — the check lands one cycle late and passes broken RTL.

• Writing |-> gnt for a registered grant — guaranteed false failures on correct hardware.

• Measuring consequent delay from the antecedent's START with multi-cycle antecedents — off-by-N checks.

• Trying to range |=> directly — there is no ranged form; desugar to |-> ##[M:N].

• Forgetting each antecedent match thread obliges its own consequent — a ranged antecedent fans out obligations.