SystemVerilog Assertions and Functional Coverage

Frontmatter

Chapter 1. Introduction

Abstract

As is well known in the industry, the design complexity at 28 nm node and below is exploding. Small form factor requirements and conflicting demands of high performance and low power and small area result in ever so complex design architecture. Multi-core, multi-threading and Power, Performance and Area (PPA) demands exacerbate the design complexity and functional verification thereof.

Ashok B. Mehta

Chapter 2. System Verilog Assertions

Abstract

An assertion is simply a check against the specification of your design that you want to make sure never violates. If the specs are violated, you want to see a failure.

Ashok B. Mehta

Chapter 3. Immediate Assertions

Abstract

Immediate assertions are simple non-temporal domain assertions that are executed like statements in a procedural block. Interpret them as an expression in the condition of a procedural ‘if’ statement. Immediate assertions can be specified only where a procedural statement is specified.

Ashok B. Mehta

Chapter 4. Concurrent Assertions: Basics (Sequence, Property, Assert)

Abstract

These are temporal domain assertions that allow creation of complex sequences using clock (sampling) edge based semantics. This is in contrast to the immediate assertions that are purely combinatorial and do not allow temporal domain sequences.

Ashok B. Mehta

Chapter 5. Sampled Value Functions $rose, $fell

Abstract

These sampled value functions allow for antecedent and/or the consequent to be edge triggered. $rose means that the expression (in $rose(expression)) was sampled to be ‘0’ (or ‘x’ or ‘z’) at the previous clk edge (previous meaning the immediately preceding clk from current clk) and that it is sampled ‘1’ at this clk edge.

Ashok B. Mehta

Chapter 6. Operators

Abstract

Following lists all the operators offered by the language (IEEE-1800, 2005). We will discuss features of 1800-2009 LRM in a separate chapter. We will examine each operator in detail since these operators are the stronghold of the language.

Ashok B. Mehta

Chapter 7. System Functions and Tasks

Abstract

$onehot and $onehot0 are quite self explanatory and are explained in the Figure 7.1. Note that if the expression is ‘Z’ or ‘X’ that $onehot or $onehot0 will fail.

Ashok B. Mehta

Chapter 8. Multiple Clocks

Abstract

There are hardly any designs anymore that work only on a single clock domain. So far we have seen properties that work off of a single clock. But what if you need to check for a temporal domain condition that crosses clock boundaries. The so-called CDC (clock domain crossing) issues can be addressed by multiple clock assertions.

Ashok B. Mehta

Chapter 9. Local Variables

Abstract

Local variable is a feature you are likely to use very often. They can be used in both a sequence and a property.

Ashok B. Mehta

Chapter 10. Recursive Property

Abstract

Recursive property simply states that a condition holds. The property calls itself with a correct non-overlapping implication operator and correct antecedent and consequent relation.

Ashok B. Mehta

Chapter 11. Detecting and Using Endpoint of a Sequence

Abstract

Before we learn how .ended works, here’s what has changed in the 1800-2009 standard.

Ashok B. Mehta

Chapter 12. ‘expect’

Abstract

‘expect’ takes on the same syntax (not semantics) as ‘assert’ in a procedural block. Note that ‘expect’ must be used only in a procedural block. It cannot be used outside of a procedural block as in assert/property/sequence—but recall that ‘assert’ can be used both in the procedural block as well as outside. So, what’s the difference between ‘assert’ and ‘expect’?

Ashok B. Mehta

Chapter 13. ‘assume’ and Formal (Static Functional ) Verification

Abstract

This is an interesting operator. ‘assume’ specifies the property as an assumption for the environment. What’s an environment? The most useful ‘environment’ for ‘assume’ is that of static formal verification. Static formal is a method whereby the formal algorithm exercises all possible combinational and sequential possibilities of inputs to exercise all possible ‘logic cones’ of a given logic block and checks to see that the assertion holds. During such verification if you do not specify any constraints (i.e. for a 5 input (a, b, c, d, e) block, if you don’t specify any constraints such as ‘assume’ a=0 and b=1) then the static formal will try to explore all possible combinations of the 5 input both in combinatorial and temporal (if required) domain. Without any constraints provided via ‘assume’, the static formal tool may experience something called ‘state space explosion’. As the description suggests, the tool may give up if too many inputs are unconstrained. This is where the ‘assume’ statement comes into picture.

Ashok B. Mehta

Chapter 14. Other Important Topics

Abstract

Asynchronous FIFO (compared to synchronous FIFO) is a difficult proposition when it comes to writing assertions. The Read and the Write clocks are asynchronous which means the most important property to check for is data transfer from Write to Read clock. Other assertions are to check for fifo_full, fifo_empty, etc. conditions.

Ashok B. Mehta

Chapter 15. Asynchronous Assertions !!!

Abstract

So far in the book we have always used a synchronous clock edge as the sampling edge for the assertion. That is for good reason. The example presented here uses an asynchronous edge (perfectly legal) as the sampling edge. The problem statement goes something like “whenever (i.e. asynchronously) L2TxData==L2ErrorData that L2Abort is asserted”. Now that looks very logical to implement without the need for a clock. So, we write a property as shown in the Fig. 15.1. We simply say that @ (L2TxData) (i.e. whenever L2TxData changes) that we compare L2TxData == L2ErrorData and if that matches we imply that L2Abort == 1.

Ashok B. Mehta

Chapter 16. IEEE-1800-2009 Features

Abstract

IEEE-1880-2009 adds the notion of a strong and weak operator applied to sequence expressions. The idea behind these ‘strengths’ is very simple.

Ashok B. Mehta

Chapter 17. SystemVerilog Assertions LABs

Abstract

We will go through six simple labs that will solidify the practical features of properties and sequences.

Ashok B. Mehta

Chapter 18. System Verilog Assertions: LAB Answers

Abstract

LAB1: Answers : ‘bind’ and Implication Operators

Ashok B. Mehta

Chapter 19. Functional Coverage

Abstract

Ah, so you have done everything to check the design. But what have you done to check your test-bench? How do you know that your test-bench has indeed covered everything that needs to be covered? That’s where Functional Coverage comes into picture. But first let us make sure we understand the difference between the good old Code Coverage and the new Functional Coverage methodology.

Ashok B. Mehta

Chapter 20. Functional Coverage: Language Features

Abstract

We will cover the following features in the upcoming sections.

Ashok B. Mehta

Chapter 21. Performance Implications of Coverage Methodology

Abstract

Don’t cover the entire 32-bit address bus

Ashok B. Mehta

Chapter 22. Coverage Options (Reference Material)

Abstract

Coverage options—instance specific—example

Ashok B. Mehta

Backmatter