This repository contains examples to illustrate the basics of System Verilog Assertions (SVAs) from the perspective of Formal Verification (FV). These examples go over sequences, properties, assertions, assumptions and covers. This is introductory material that covers basic principals.
The examples are in src directory and the associated documentation is in docs directory. The documentation is autogenerated from the source using markdown script in tools repository.
Some of the testbenches here use features of 2012 SystemVerilog. Tool support may not be uniform for these.
- Introduction
- Concurrent assertions
- Immediate assertions
- Clocking
- Module binding
- Formal arguments
- "disable" keyword
- System functions
- Sampled value functions
- Delay operator
- Consecutive repetition operator
- Goto and non consecutive repetition operator
- "if" and "case" keywords
- Local variables
- Sequence operators
- Property operators
- Safety vs liveness
It is usually advisable to use constructs that match the use case. If multiple constructs can be used, the easiest to understand is the best.
If the requirements involve a lot of correlated checking across interfaces and state, it is a good idea to craft a synthesizable testbench that is self explanatory and write simpler assertions using the state and the outputs of the state machine. In such scenarios, numerous interrealed but separate SVAs become hard to understand and debug.
There need to be some caution excercised when crafting very complicated sequences. It is advisable to make shorter sequences and then use them to assemble larger sequences. Excessively complex sequences can be very hard do debug and often create overconstraints. Often their creator is the only one who can understands what they represent, and only on the day they get created. So maintanence is a problem with such sequences. These are akin to the regex contortions of the scripting world.