Implication and Property Operators · SystemVerilog

Part 4 · Assertions (SVA) · Intermediate

5topics
5lessons

Sequences describe patterns, and properties state obligations about them. The workhorse is implication: when the antecedent sequence matches, the consequent must hold.

Piece	Role	Example
Antecedent	Sequence trigger; each match starts an obligation	`req`, `$rose(req)`, `(req ##1 ack)`
Implication	Binds trigger to obligation, same or next cycle	`ante \|-> cons`, `ante \|=> cons`
Property operators	Combine verdicts from the same start tick	`not p`, `p and q`, `p implies q`
Temporal operators	Extend obligations over time, weak or strong	`always p`, `s_eventually p`, `p until q`

Lesson	What it covers
Overlapped vs nonoverlapped	Same-cycle vs next-cycle consequent start, one stimulus with opposite verdicts, and the desugared delay form.
Vacuous Success	Passing assertions that check nothing, and the assert-plus-cover discipline that proves antecedents fired.
Property Operators	Layer rules for `not`, `and`, `or`, `if`/`else`, `iff`, and `implies`, plus the negation-over-threads trap.
Temporal operators	Strong and weak families, `until` timing to the tick, and safety versus liveness in simulation.
Designing Good Antecedents	Edge-anchored triggers, qualifier placement, reusable clockless properties, and a review checklist.

Check yourself Every assertion in a regression passes, yet a broken grant is never caught. What is checked first?

Whether the antecedents ever fired. A passing implication whose antecedent never matched is vacuous, so each assert needs a paired cover of its antecedent, with cover hits required at sign-off.

Up next|-> vs |=>

Practice this lesson Report an error

Piece

Role

Example

Antecedent

Sequence trigger; each match starts an obligation

req, $rose(req), (req ##1 ack)

Implication

Binds trigger to obligation, same or next cycle

ante |-> cons, ante |=> cons

Property operators

Combine verdicts from the same start tick

not p, p and q, p implies q

Temporal operators

Extend obligations over time, weak or strong

always p, s_eventually p, p until q

Lesson

What it covers

Overlapped vs nonoverlapped

Same-cycle vs next-cycle consequent start, one stimulus with opposite verdicts, and the desugared delay form.

Vacuous Success

Passing assertions that check nothing, and the assert-plus-cover discipline that proves antecedents fired.

Property Operators

Layer rules for not, and, or, if/else, iff, and implies, plus the negation-over-threads trap.

Temporal operators

Strong and weak families, until timing to the tick, and safety versus liveness in simulation.

Designing Good Antecedents

Edge-anchored triggers, qualifier placement, reusable clockless properties, and a review checklist.