SystemVerilog · Topic
SystemVerilog Assertions (SVA)
SystemVerilog assertions from immediate and deferred checks through sequences, properties, implication and vacuity — and why an assertion that never fails has never been shown to work.
An assertion is a claim about behaviour over time, and the hard part is not the syntax — it is that a badly-written assertion does not fail loudly, it stops discriminating. A property whose antecedent never matches passes on every run and reports nothing, which is indistinguishable from a design that is correct. That single failure mode explains most of what SVA's machinery exists for: the sampling rules that decide which value a property sees, the implication operators that separate 'when this happens' from 'this always happens', and the cover statements that prove an assertion was ever reached at all.