SV Assertions

What is an Assertion ?.

An Assertion is simply a check against the design specification that you would like to make sure never violates.

If the specification is violated, you would like to see an ERROR.

For example consider a sample situation below :

Consider a situation where a 5-bit 'state' value. Lets say that as paer the specification, this state must never assume the value 'd8.

Such checks are imperative to the correct functioning of the design as laid down by the specification. SVA (System Verilog Assertions) language is precisely designed to tackle such temporal domain scenarios.

Refer example below where such a check is modelled using SVA property.

Refer below a full working example code :

Refer snippet of the wave dump of the above example below (Simulated on Questa).

Could not load fig. Plz refresh
Assertion example wave dump

Modelling such a check is far easier in SVA than in Verilog.

NOTE : Assertions work in temporal domain and are concurrent as well as multi-threaded. These attributes is what makes SVA language so suitable for writing temporal domain checks.

Advantages of Assertions

Few advantages of SV assertions are :
  • They are easier to write than standard Verilog or System Verilog.
  • Easier to Debug.
  • Provide Functional Coverage.
  • Simulate faster compared to the same code written in either Verilog or System Verilog.
Assertions provide temporal domain Functional Coverage

Assertions not only help you find bugs, but also help you determine is you have covered (i.e. exercised) design logic, mainly temporal domain conditions.

Here's why this is important :

Not finding bugs in your design could mean one of two things :
  • There is indeed no bug left in the design (or)
  • You have not exercised (or covered) all the required functions of the design.

You could be continuously hitting the same piece of logic in which no further bugs remain. In other words, you could be reaching a wrong conclusion that 'all the bugs have been found'.

Coverage includes 3 components :
  • Code Coverage : which always needs to be 100%
  • Functional Coverage : which needs to be designed to cover functionality of the entire design and must also be completely covered.
  • Temporal Domain Coverage : using SVA 'cover' feature. Which needs to be carefully designed to fully cover all required temporal domain conditions of the design.

Refer the previous code fragment for the example assertion, (shown below) :

In this code, we can see that there is a 'cover' statement.

What it tells us is "Did you exercise this condition" or "Did you cover this property".

In other words, if the assertion never fires, that could be because of two reasons :
  • There is indeed no bug.
  • The condition was never exercised to begin with.

With the cover statement, if the condition gets exercised but does not fail you get that indication through the 'Assertion Covered' action block associated with the cover statement.

SVA supports the 'cover'construct that tells us if the assertion has been exercised (covered). Without this indication and in the absence of a failure, we would have no idea if we indeed exercised the required condition.

NOTE : User must always use 'cover' to full extent as part of their verification methodology.
Other benefits of Assertions
Other major benefits of System Verilog Assertions include :
  • SVA Laungaue supports Multi-CDC (Clock Domain Crossing) logic.
  • Assertions are readable, which makes them great for documenting and communicating design intent.
  • Reusability for future designs : Assertions can be parameterized and can be modelled outside the RTL and can be binded using 'bind'.
  • Assertions are Always ON : Assertions never go to sleep (unless you specifically turn them off).
  • Assertions find use in Emulations
  • Global Severity Levels : $Error, $Fatal etc.
  • Assertions can be globally turned ON/OFF.
  • Formal Verification depends on Assertions

Assertion Types

There are three kinds of assertions supported by SVA :
  • Immediate Assertions
  • Concurrent Assertions
  • Deferred Assertions
Immediate Assertions
  • Simple non-temporal domain assertionsthat are executed like statements in a procedural block.
  • Interpretted the same way as an expression in the conditional of a procedural 'if' statement.
  • Can be specified only where a procedural statement is specified.
Concurrent Assertions
  • These are temporal domain assertions that allow creation of complex sequences using clock (sampling edge) based semantics.
  • These are edge-sensitive and not level-sensitive. In other words, they must have a 'sampling-edge' on which it can sample the values of variables used in a sequence or property.
Deferred Assertions
  • Deferred Assertions are a type of Immediate Assertions.
NOTE : Immediate Assertions evaluate immediately without waiting for variables in its combinatorial expression to settle down. This also means that immediate assertions are very prone to glitches as the combinatorial expression settles down and may fire multiple times. On the other hand deferred-assertions do not evaluate their sequence expression until the end of the timestamp when all values have settled down.