What You will learn in this paper
- A brief history of SystemVerilog Assertions
- SVA layers definition and examples
- Assertion types, sequential property operators
- A short description of liveness and safety properties
- Practical examples using the sequence builder module written by our CTO Claire Xen.
This Application Note was written with the intention of showing a brief introduction to SVA, and is definitely not a substitute for extensive training. To learn more about formal verification and SVA, it is recommended to book the course given by the FPV specialists at YosysHQ.
-
Section :ref:
Property Checking with SystemVerilog Assertions
contains a brief introduction of SVA and the description of some elementary terms. -
Section :ref:
Assertion Types
describes the different types of properties defined in the P1800, immediate and concurrent. It also presents both clock and disable conditions for concurrent assertions. -
Section :ref:
Elements of SVA
describes each layer of SVA: Boolean, Temporal, Property and Verification layers. This section also describes some sequence property operators and property types.