Topic (properties)
SVA is not just syntax—good assertions encode intent precisely, resist vacuity, and scale with a proof plan. I write SVA with explicit assumptions, clear temporal structure, and reusable patterns.
- Principles: clarity · vacuity resistance · minimal assumptions
- Patterns: interface contracts · invariants · refinement lemmas
What “good SVA” means in practice
- Signal discipline: assertions reference stable, meaningful signals (not accidental internals)
- Temporal intent: preconditions and consequences are separated clearly
- Assumptions are explicit: environment constraints are documented and reviewable
- Vacuity checks: proved properties should still be informative
Common patterns I use
- Interface contracts: request/ack, ready/valid, FIFO rules
- Safety properties: “this bad thing never happens”
- Liveness under assumptions: “eventually” properties only where appropriate
- Helper lemmas: small provable stepping stones for complex end-to-end goals
Where this shows up on my site
- Formal case studies (proof structure)
- Publications (property strategy and evaluation)
Need help structuring assertions for a block?
If you want to collaborate, discuss roles, or review artifacts, reach out.