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 |
|
Implication | Binds trigger to obligation, same or next cycle |
|
Property operators | Combine verdicts from the same start tick |
|
Temporal operators | Extend obligations over time, weak or strong |
|
Lesson | What it covers | Path |
|---|---|---|
Same-cycle vs next-cycle consequent start, one stimulus with opposite verdicts, and the desugared delay form. | Required | |
Passing assertions that check nothing, and the assert-plus-cover discipline that proves antecedents fired. | Required | |
Layer rules for | Recommended | |
Strong and weak families, | Optional | |
Edge-anchored triggers, qualifier placement, reusable clockless properties, and a review checklist. | Recommended |
Required lessons are the core first pass for writing working assertions. Recommended lessons are worth reading for most learners once the first pass works. Optional lessons are reference, specialist material or revision, and you can come back to them when a project needs them.
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.