nexttime, always, s_eventually, until

Strong and weak operator families

SVA temporal property operators come in pairs: weak (nexttime, always, eventually, until, until_with) and strong, prefixed s_ (s_nexttime, s_always, s_eventually, s_until, s_until_with). The split answers one question: what happens if evaluation ends while the obligation is still pending? Weak: pending-at-end is acceptable — no failure. Strong: the obligation MUST complete; end-of-evaluation with it pending is a failure. Simulation "end of evaluation" is end of simulation (or disable); in formal it is the unbounded horizon, where the distinction becomes the safety/liveness divide.

// Weak: if sim ends mid-wait, no failure
property p_weak_done;
  @(posedge clk) start |-> eventually [1:$] done;  // weak form (ranged)
endproperty

// Strong: done MUST occur; pending at end of evaluation = FAIL
property p_strong_done;
  @(posedge clk) start |-> s_eventually done;
endproperty

// always p: p at every tick from now on (weak — cannot fail "late")
property p_inv;
  @(posedge clk) always (!both_grants);   // invariant style
endproperty

// nexttime / s_nexttime: p at the next tick (strong requires the
// next tick to EXIST — relevant at end of finite traces)
property p_nt;  @(posedge clk) start |-> s_nexttime busy; endproperty

until family: waveform semantics

p until q — p holds at every tick up to but not necessarily including the first tick where q holds; weak, so q need never arrive provided p holds forever (or to end of sim). p s_until q additionally REQUIRES q to occur. p until_with q requires p to hold through and including the first q tick (overlap), again in weak and strong (s_until_with) flavors.

WAVEFORM — busy until done   /   busy until_with done

clk  :  1    2    3    4    5    6
busy :  0    1    1    1    0    0
done :  0    0    0    0    1    0
             A              q
until      : busy must hold ticks 2,3,4 (BEFORE first done @5).
             busy=0 @5 is FINE — q's tick not included → PASS
until_with : busy must hold ticks 2,3,4 AND 5 (q's tick included).
             busy=0 @5 → FAIL at tick 5
                            X

WAVEFORM — weak vs strong when done NEVER comes

clk  :  1    2    3    4   ...  end-of-sim
busy :  0    1    1    1   ...  1
done :  0    0    0    0   ...  0
until    : p held every tick, q absent → weak → PASS (no failure)
s_until  : q never occurred → STRONG → FAIL at end of evaluation
                                          F

// Bus busy must persist until (and including) the handoff cycle
property p_hold_through_handoff;
  @(posedge clk) $rose(busy) |-> busy s_until_with handoff;
endproperty
a_hold: assert property (p_hold_through_handoff);
// s_ flavor: a hang where handoff never comes is a FAILURE,
// not a silent pend — this is what you want in formal.

Safety vs liveness — and what simulation can see

Safety properties say "nothing bad ever happens" — any violation is exhibited by a finite trace prefix (the bad thing happened at tick K). Liveness properties say "something good eventually happens" — a violation is an INFINITE behavior (the good thing never comes), which no finite trace can conclusively demonstrate. Simulation runs finite traces, so it can only ever catch safety violations; a liveness failure in simulation appears only as the heuristic "still pending at end of sim", which weak operators deliberately forgive and strong operators report. This is why strong operators matter mostly in formal : a model checker reasons about infinite behaviors (loops) and can genuinely prove or refute s_eventually — e.g. exhibiting a starvation cycle where a requester loops forever without a grant.

SAFETY vs LIVENESS — who can catch what

  SAFETY  "never two grants"        not (gnt0 && gnt1)
     violation = finite witness (tick K shows both high)
     simulation: CAN catch ✓        formal: CAN prove ✓

  LIVENESS "every req eventually granted"   req |-> s_eventually gnt
     violation = infinite path (req loops forever ungranted)
     simulation: cannot conclude — only "pending at end" heuristic
     formal: finds a loop counterexample (starvation cycle) ✓

  practical simulation substitute for liveness:
     bound it →  req |-> ##[1:MAX_LAT] gnt   (turns it into safety)

Interview angle and review

Interview angle

• "until vs until_with?" — whether p must also hold ON the first q tick (until_with: yes, overlap; until: no). Draw the tick-5 waveform above.

• "Why can't simulation verify liveness?" — a liveness violation is an infinite behavior; finite traces can only leave it pending. Bounding the window converts it to checkable safety.

• "When do s_ operators change anything in simulation?" — only at end-of-evaluation: strong pendings become failures instead of silent drops; useful for catching hangs at end of test.

• "Classify: 'fifo never overflows' / 'every packet is eventually delivered'." — safety / liveness; then explain the bounded-latency rewrite of the second for simulation sign-off.

Key takeaways

• Weak operators forgive obligations still pending at end of evaluation; strong (s_) ones fail them.

• until excludes the q tick from p's obligation; until_with includes it — one tick, frequent bug.

• Safety violations have finite witnesses (simulation-catchable); liveness violations are infinite (formal territory).

• For simulation sign-off, bound liveness into safety: s_eventually x becomes ##[1:MAX] x.

Common pitfalls

• Using weak eventually/until in simulation and reading silence as proof — pending obligations vanish quietly at end of sim.

• until where the spec keeps the condition through the terminating event — off-by-one at the q tick; until_with was meant.

• Shipping s_eventually to a simulation-only flow and expecting mid-sim failures — strong operators report at end of evaluation, not earlier.

• Writing unbounded liveness assertions as the only check for latency-critical paths — add the bounded safety version for regression.

• Confusing always p (property, infinite obligation) with assert property(p) attempt-per-tick semantics — related but not identical mechanisms.