Learning Properties, Assertions and Covers for Hardware Design

How do you learn new hardware design topics? I just got trained online about property-based verification for hardware designers using a free online class at Aldec. The material was created by Jerry Kaczynski, a Research Engineer at Aldec.

Assertions
An assertion is an abstract representation of device behavior, useful in design specification, verification and implementation.

• SoC designers use assertions
• The IEEE has defined standards: IPSL, SystemVerilog, VHDL
• They are simple, based on the design specification
• Create safety for simulation
• Can be live documentation

You can place assertions directly into RTL code, hidden in special comments like:

–psl property p1 is…, or //psl property p2=…

With SystemVerilog you can add assertions directly in the Verilog code. Eventually in VHDL 2008 you can place PSL assertions directly in the VHDL code.

Most logic synthesis tools ignore assertions for now, although some libraries of property checkers allow synthesis.

Assertion Based Verification (ABV) involves: Sequences -> Properties -> Assertions/Covers. An Assert on a property verifies that bad things do not happen, while a Cover on a property verifies that good things happen.

Properties
Formal properties use the concept of temporal logic, which is boolean logic along with time. These time relationships use operators like:

• Next
• Finally
• Globally
• Until

As an example if we wanted to describe, “activation of REQ must be followed by activation of ACK”, it looks like:

• globally (REQ implies (finally ACK) )

Temporal Logic
Temporal logic extends the familiar concept of boolean logic to include time (i.e. next, finally, globally, until, release, all, exists).

Computational Tree Logic
An example from a 5-state machine is provided, then Computational Tree Logic (CTL) is used to ask some questions about the design:

In case 1, the Expression of AF S4 means, “Can we Always Find a path to state S4?”. Well, that’s false both p1 and p3 don’t require state S4.

Properties are used in verification for:

• Liveness (e.g. something good eventually happens)
• Safety (something bad does not happen)

A verification tool would use properties to:

• Assume that certain properties must hold all the time
• Assert that certain properties hold, alarm when they fail
• Check if all desired properties were covered

Building Sequences and Properties
Two standard languages are introduced: Property Specification Language (PSL), SystemVerilog Assertion subset (SVA). An example sequence using boolean:

• Elements stick together at the same clock

  • A:B (using fusion in PSL)
  • A##B (using zero cycle delay in SVA)
• One cycle break between elements

  • A;B;C (using concatenation in PSL)
  • A ##1 B ##1 C (using one cycle delay in SVA)

An example using repetition notation:

Creating Asserts and Covers
The concept of Implication is introduced, then applied to the design property, “ACK should be activated 1 to 3 cycles after REQ, provided that RESET is not active”:

An improvement is made to the assertion to take into account the edge of RESET:

Asserts raise alarm when the asserted property fails, while Covers can print or increment when the behavior was detected.

Verification Directives
Assert, Assume and Cover are reviewed, then Action Blocks are shown with usage tips:

Some of the verification directives are simulator specific, so you have a learning curve with each new simulator. The Aldec simulators use a color-coded waveform viewer to show results of Assertions:

Summary
You can learn to use Properties, Assertion and Coverage to improve the design, verification and implementation of your next SoC project. Free, online training is a good starting point which can then be followed up with instructor-led classes, and book reading.