Implication & Property Operators

Overview

Sequences describe patterns; properties state obligations about them. The workhorse is implication: when the antecedent sequence matches, the consequent must hold. Almost every practical assertion is an implication, so the property layer is where the interview questions concentrate: same-cycle vs next-cycle consequent start, vacuous passes that check nothing, and the strong/weak operator families that separate simulation from formal.

Property operators look like sequence operators but live a layer up — not, and, or applied to properties have property semantics, and confusing the layers produces assertions that compile cleanly and check the wrong thing. This topic ends with antecedent design — the craft of writing triggers that are neither vacuous nor noisy.

Sub-topics

1. |-> vs |=> — overlapped vs non-overlapped implication, the classic discriminator.

2. Vacuous Success — passing assertions that check nothing, and the assert+cover discipline.

3. Property Operators — not, and, or, if/else, iff, implies at the property layer.

4. nexttime, always, s_eventually, until — strong/weak families, safety vs liveness.

5. Named & Parameterized Properties — formal arguments and a reusable property library.

6. Designing Good Antecedents — $rose vs level, gating, and attempt explosion.

THE PROPERTY LAYER

  boolean expr ─► sequence ─► PROPERTY ─► assert / assume / cover
                              │
        ┌─────────────────────┤
        │ implication         │ property operators
        │   ante |-> cons     │   not p          if (e) p else q
        │   ante |=> cons     │   p and q        e iff p
        │                     │   p or q         p implies q
        │ temporal            │
        │   nexttime p        │ strong (s_) = must finish → liveness
        │   always p          │ weak        = may pend    → safety
        │   s_eventually p    │
        │   p until q         │
        └─────────────────────┘
  attempt: every property is evaluated from EVERY clock tick
  (one evaluation attempt per tick) unless gated by its antecedent

Key takeaways

• Implication is the assertion workhorse: antecedent match obliges the consequent.

• Every clock tick starts a new evaluation attempt — antecedents are the gate.

• Property operators are a distinct layer above sequence operators with their own semantics.