Introduction to Assertion-Based Verification – Part 1

modemdesign

Introduction to Assertion-Based Verification – Part 1 [Copy link]

Introduction to Assertion-Based Verification – Part 1

Assertion-based verification (ABV) is a technique that can significantly reduce the verification process compared to traditional methods.

ABV is primarily used in the ASIC space, but is proving to be equally critical in the FPGA verification flow due to the increasing complexity of FPGA devices.

However, before we start celebrating the possibility of dramatically shortening chip project verification cycles, we need to understand assertions and how to effectively integrate them into verification methodologies.

For ease of technical digestion, this introduction to assertions will be divided into two parts. Part I will explain what assertions are, discuss the language, and develop the basic terminology and ideas. In Part II, we will dig deeper and introduce the use of entailment and the concept of "empty truth" as well as assertions and overwriting.

What is an assertion?

The simplest definition of an assertion is "an abstract representation of device behavior useful in specification, verification, and implementation..."

We'll see later that this definition can be expanded to be more accurate, but let's use this definition for now.

There are two languages that can be used to express practical applications of assertions, namely the Property Specification Language (PSL) and the SystemVerilog Assertions subset (SVA) .

PSL is available for VHDL, Verilog, SystemVerilog, and SystemC, and is a subset of VHDL-2008.

SVA is an assertion-related subset of the SystemVerilog language, based on contributions from Superlog and OpenVera. Its assertion and property capabilities also draw on PSL.

Both languages are IEEE standards.

Which language?

VHDL designers can use both SVA and PSL, but usually choose PSL because it can be dropped directly into VHDL code and helps with design documentation, while SVA cannot. In addition, PSL is now part of the VHDL standard (2008), so this means that only one language needs to be used.

Verilog designers can use both PSL and SVA, but typically use SVA because it has more features available than PSL when dropped directly into Verilog code. In addition, SystemVerilog and Verilog are now merged into one standard - SystemVerilog.

The good news is that PSL and SVA attributes look almost identical.

Why use assertions?

Assertions have become an established and popular verification methodology in ASIC design, so FPGA design can learn from this area. Importantly, they are governed by IEEE standards (PSL, SystemVerilog, and VHDL).

It is much easier to deal with classes, objects, inheritance, etc. in object-oriented programming. They are based on design conventions that you as a designer are familiar with, so they are easier to implement.

Assertions create an extra layer of safety in simulations because they are references to the original specification and are very useful when doing iterations between synthesis and implementation.

Assertions essentially create "living documentation" in the way they are written, which makes management of designs much easier. They are very easy to read and interpret, which makes sharing with design teams much more manageable.

Where to put assertions?

All tools allow you to place assertions in separate cells or files and "tie" them to the regular RTL code. Verification engineers like this idea because it allows file independence, while HDL designers usually prefer to put assertions directly into the code to reduce the amount of files required.

Most simulators allow you to place assertions directly in your RTL code. For PSL, this is expressed as comments. For SystemVerilog, assertions can be placed directly in the code.

For example: – psl property p1 is ... or // psl property p2 is ...

VHDL-2008 allows PSL assertions to be placed directly into the code (without comments).

You need to be careful when putting assertions into your code because synthesis tools often do not support some assertions, so you need to use synthesis pragmas to manage them.

Develop basic terminology and ideas

The term "assertion-based verification" (ABV) is often used to describe the entire verification process, but it involves more than just assertions.

The process consists of sequences, properties, assertions, and overrides.

The basic idea of ABV is “attribute.” A property is a formal description of a specific behavior of a design, such as “a broken window triggers the alarm” or “security responds to the alarm within 30 seconds.”

Verification tools can use properties in a variety of ways, by "asserting" the property to verify that nothing bad will happen, such as "assert that a broken window will always trigger the alarm."

Or, use "Override" to verify that something good happened, such as "The response to the triggered alarm was overridden within 30 seconds."

Digging deeper into these attributes, if you look at a typical digital design specification, it is already full of design attributes expressed in plain English. As a designer, you can rewrite these attributes into HDL, taking into account the correct hardware implementation.

Hence, properties, assertions and covers represent the pure behavior (desired or not) of the design. As we said, they can serve as very effective design documentation and as a reference during design verification. They are also accepted by various functional and formal verification tools.

We now need to understand how to define a property and how it uses the principles of "temporal logic".

Temporal logic can be thought of as Boolean logic with the added dimension of time.

If we use "discrete time", then the properties represent the "sequence of states" of the design. Note that all popular property-based design (PBD)/ABV solutions operate on sampled values of the objects in the design.

To express this relationship in time, properties use “temporal” or “modal” operators such as next, finally, globally, until, and so on.

Next we need to understand how to construct properties.

The Boolean type expressions we are all familiar with are part of the attribute composition, but they are the simplest part. We also need to understand "sequences".

A "sequence" is generally considered to be the basic temporal building block that represents the properties of a series of design states at discrete points in time.

A typical sequence represents a simple execution path in a design.

To create a real property from a simple sequence you can:

"Fused" sequences, where one sequence ends at the same moment another begins.

"Connect" sequences, where one sequence ends and the other starts at the next point in time

Saying that a sequence is "implied" by another sequence

"AND" or "OR" sequence

Checks if one sequence is contained in another

Checks if a sequence repeats a given number of times (continuously or not)

Once design properties are formalized, all tools can use these properties in one of two directives:

figure 1

Assertions - raise an alert when a property does not hold.

Override - confirms that the property was tested successfully.

Some tools (mostly formal verification, but also some simulators) allow more directives, such as controlling the design stimulus or constraining the environmental conditions (assumptions, restrictions, fairness, etc.).

Building useful assertions

Now that we understand the basic elements of properties and sequences, let's look at how to build actual assertions.

As we mentioned, the most fundamental property is "sequence" with a strictly linear time flow.

Simulation requires a linear flow of time, so it is not possible for properties to jump back and forth in time, as this would make the simulation impossible.

Each node of the sequence represents a state of your design:

Required value for some signal

Conditions that must be met

In order to complete the sequence, you have to specify how to connect these nodes together. So, let's look at some "sequence" property facts.

The simplest sequences are Boolean expressions, but more often you'll glue multiple expressions together to form complex sequences that "expand over time".

To make elements stick together on the same clock, use 'fusion' ( in PSL or 'zero clock delay' (##0) in SVA.

To introduce a one cycle break between elements, use 'concatenation' (;) in PSL or 'one cycle delay' (##1) in SVA.

You can specify longer delays using a range of values (##[ m:n ]) in SVA.

PSL uses the "consecutive repetition operator" (<sequence>[*m to n]) to specify a "value range" delay. If there is no sequence to repeat, "True" is assumed to be the repeated parameter.

Now that we've mentioned repetition, let's look at this more formally.

If the same condition should remain for more than one cycle, then we can use the "Continuous Repetition Operator" instead of using concatenation or one cycle delay to repeat the condition.

This operator looks the same in PSL and SVA: Sequence [* Number_or_Range ] Sequence [* Number_or_Range].

The simple form with a number indicates that the sequence should be repeated (kept) a given number of times: A[ *7].

The range version indicates that the sequence should hold for any number of cycles within the natural range (to specify an infinite upper bound, use "inf" in PSL or "$" in SVA): B[*1 to inf] B[*1:$]

Let's illustrate this with an example:

image 3

Here we see an example of a repeat, as well as an equivalent sequence without the repeat, and show the same sequence for PSL and SVA.

Clock Sequence/Reset and Properties

All property languages use discrete time, which means that a clock or sampling method must be specified.

If a clock is not specified, the fastest available tool default is applied, which in the case of a simulator may be a clock with a period equal to the simulation resolution.

If most properties use a clock method, you can specify a 'default clock'.

To specify a clock event, use "@<clock condition>" at the end of the sequence in PSL or at the beginning in SVA.

For clock conditions, use the preferred clock detector in your native HDL, such as the " rising_edge " function in VHDL or " negedge " in Verilog.

We also need to be able to handle resets, because sometimes you might be in the middle of a property evaluation, and a reset occurs, which causes an assertion failure or other unwanted behavior.

Fortunately, both PSL and SVA provide mechanisms to forgo attribute evaluation without adverse effects.

PSL allows adding an "async_abort" or "sync_abort" operator and a reset condition at the end of a property.

always (({(A);(B)}) async_abort C='1′) @rising_edge(CLK);

Add the phrase "disable iff (condition)" to the beginning of the attribute.

@(posedge CLK) disable iff (C) A ##1 B;

To summarize clock and reset:

There is no default reset in the properties, but you can have a default clock (sampling event).

The textual order in which reset and clock are applied to attributes in SVA is a mirror image of the order in PSL.

Figure 4

In summary

We introduced assertions and found that PSL and SVA properties are similar and resemble design requirements.

We developed the basic terminology and ideas of assertions and discussed sequences, properties, assertions, and coverage and how they form design properties. We also learned how to define properties and how it follows from the principles of temporal logic. Finally, we started building some actual assertions to understand what we have introduced and discussed.

If you liked this introduction, you can look forward to the second part which will cover the use of entailment in assertions and its importance in assertions and its use in simulations.