Property Operators: not, and, or, if/else, implies

Two layers, same keywords

and and or exist at BOTH the sequence layer and the property layer, with different semantics. At the sequence layer they compose match threads (with length rules — previous topic). At the property layer the operands are properties — things that hold or fail — and the operators are plain logic over verdicts: p and q holds iff both hold from the start tick; p or q holds iff either holds. Which layer you are in is decided by the operand types, a resolution the compiler performs silently — which is exactly why mixed-up expressions compile and mislead.

// PROPERTY and: two obligations from the same start tick
property p_two_rules;
  @(posedge clk) start |->
    ((##[1:4] done) and (no_err throughout (busy [*1:$] ##1 done)));
endproperty

// PROPERTY or: alternative legal behaviors
property p_alt;
  @(posedge clk) req |-> ((##1 gnt) or (##1 retry ##1 req));
endproperty

// not: the property must NOT hold
property p_never_double_gnt;
  @(posedge clk) not (gnt ##1 gnt);
endproperty
a_ndg: assert property (p_never_double_gnt);

The not danger with nondeterministic sequences

not p holds exactly when p fails. For a sequence used as a property, the sequence holds if ANY match thread completes — so not s holds only if every thread of s fails to match. With ranged operators this is usually NOT what the writer meant: people read "not (req ##[1:3] gnt)" as "no grant in the window", which happens to align — but read "not (a ##[1:3] b)" under an implication and the negation-of-existence semantics interacts with vacuity and attempt threading in ways that surprise. The robust style: push negation down to booleans (!gnt throughout, ##[1:3] !b) and keep not for genuinely property-shaped negations.

WAVEFORM — not (a ##[1:2] b): ALL threads must fail

clk :  1    2    3    4
a   :  0    1    0    0
b   :  0    0    0    1
            A
inner threads from @2:  b@3? b=0 → dies   b@4? b=1 → MATCHES
sequence holds (one thread matched) → not(...) FAILS at tick 4.
A candidate who thinks "thread b@3 failed, so not passes" has
inverted per-thread instead of over the whole match set.

Compare the boolean-pushdown form  a |-> ##[1:2] !b :
  obligation: b LOW at tick 3 AND ... no — one thread suffices!
  ##[1:2] !b holds if !b on EITHER tick → b=1 @4 still PASSES via @3.
The two "negations" are NOT equivalent — choose deliberately:
  "b never in window"  →  a |-> (!b)[*2] (after ##1)  or  not (a ##[1:2] b)

The waveform shows the real lesson: negation over a nondeterministic sequence quantifies over ALL threads, while a negated boolean inside a ranged delay still quantifies over ANY thread. "No b in the whole window" must be written as a universal — not (a ##[1:2] b) or a |=> (!b)[*2] — never as a |-> ##[1:2] !b.

if/else, iff, and implies

Property if (expr) p else q selects an obligation by a boolean sampled at the attempt tick — protocol mode forks read naturally this way. e iff p style equivalences (and the boolean iff inside expressions) state two-way correspondence. p implies q is property-level implication: unlike |->, whose left side is a SEQUENCE whose every match endpoint launches the consequent, implies takes a PROPERTY on the left and simply requires "if p holds from this start tick, q holds from this same start tick" — no endpoint threading, no vacuity bookkeeping per match, both sides evaluated from the attempt tick.

// Mode-dependent obligation
property p_mode_resp;
  @(posedge clk) req |->
    if (fast_mode) ##1 gnt
    else           ##[2:4] gnt;
endproperty
a_mode: assert property (p_mode_resp);

// implies: relate two PROPERTIES from the same start tick
property p_stable_link; always (!link_err) ;          endproperty
property p_throughput;  s_eventually (cnt == 8);      endproperty
property p_rel;
  @(posedge clk) p_stable_link implies p_throughput;
endproperty

// Contrast with |->: left side is a sequence, consequent timed
// from each match ENDPOINT — implies has no such endpoint shift.

OPERATOR MAP — sequence layer vs property layer

  left operand a SEQUENCE, endpoint-driven:
      s |-> p      s |=> p          (implication, vacuity rules)
  both operands PROPERTIES, same start tick:
      p implies q  p and q  p or q  not p
  boolean-selected:
      if (e) p else q               e iff p (boolean equivalence)

  if it has an ENDPOINT that shifts time → sequence-layer thinking
  if it is a VERDICT combined logically → property-layer thinking

Interview angle and review

Interview angle

• "Is and between two sequences the same as between two properties?" — no: sequence and has length/endpoint rules (composite ends with the longer); property and is verdict conjunction from a common start tick.

• "Write 'b never occurs in the 2 cycles after a'." — not (a ##[1:2] b) or a |=> (!b)[*2]; explaining why a |-> ##[1:2] !b is wrong (existential thread semantics) is the senior answer.

• "implies vs |->?" — operand layer and timing: |-> takes a sequence antecedent and times the consequent from each match endpoint with vacuity semantics; implies relates two properties evaluated from the same start tick.

• "When do you reach for if/else in a property?" — mode-dependent consequents sampled at attempt time, instead of duplicating the assertion per mode.

Key takeaways

• Operand types pick the layer: identical keywords, different semantics at sequence vs property level.

• not over a sequence quantifies over ALL match threads — sequence holds if any thread matches, so not requires all to fail.

• "Never in window" needs a universal form (not(seq) or (!b)[*N]); a negated boolean in a ranged delay stays existential.

• implies is start-tick property implication; |-> is endpoint-shifting sequence implication with vacuity.

Common pitfalls

• a |-> ##[1:3] !b as "b absent for 3 cycles" — passes if b is low on ANY one tick of the window.

• Treating not as per-thread inversion — it negates the whole match-set verdict.

• Using |-> where both sides are conceptually properties — accidental endpoint shift and vacuity noise; implies was meant.

• Forgetting if (e) samples e at the attempt tick — a mode change mid-obligation does not re-select the branch.

• double negation not(not(s)) to "force" strength — it changes weak/strong classification in subtle LRM-defined ways; avoid.