Lesson 3.8 · SystemVerilog Assertions Essentials

Common SVA mistakes and how to avoid them

Mistake	Example	Why it hurts	Better
Using `\|->` where the spec means "next cycle"	`req \|-> gnt`	Requires grant in the same cycle	`req \|=> gnt`
Antecedent can never be true	`a && !a \|-> b`	Vacuous proof, checks nothing	Cover the antecedent
Forgetting reset	No `disable iff`	Spurious failures during or right after reset	Default `disable iff (rst)`
Using `==` on X in simulation	`data == 8'hxx`	Never true; use `$isunknown` or `===` in sim-only checks	`!$isunknown(data)`
Unbounded antecedent	`a ##[1:$] b \|-> c`	Many threads; slow or inconclusive	Track "a seen" with a flag
Assuming outputs of the DUT	`assume property (gnt[0])`	Constrains the design itself — may hide every bug	Assume inputs only
One huge property	Five requirements and-ed together	Hard to debug, slow to prove	One requirement per property
Confusing `[->n]` and `[*n]`	`ack[*2]` for "two acks"	`[2]` means two consecutive* cycles	`ack[->2]`
`$past` right after reset	`q == $past(d)`	Compares against pre-reset values	Guard with reset / antecedent

Chapter takeaways