Lecture Overview Introduction to SystemVerilog Assertions (SVA)

Introduction to SystemVerilog Assertions (SVA)

Lecture Overview

Introduction to

SystemVerilog

Assertions (SVA)

In this lecture, you will. . .

Harry D. Foster

Chief Scientist Verification

?

Learn the structure of the SVA language

?

Learn how to construct sequence

?

Learn how to construct properties

IC Verification Solutions Division

?

Apply SVA on real examples

February 2020

?

Exercises

?

Summary

2

2

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

SystemVerilog Assertions

LINEAR FORMALISM

?

SVA is based on linear temporal logic (LTL) built over

sublanguages of regular expressions.

?

Most engineers will find SVA sufficient to express most

common assertions required for hardware design.

Brief Review of LTL and Introduction of Regular Expressions

? Mentor Graphics Corporation

4

4

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

1

HF, UT Austin, Feb 2019

? Mentor Graphics Corporation

Introduction to SystemVerilog Assertions (SVA)

What We can Express in LTL

What We can Express in LTL

?

? All Boolean logic propositions - p

F p ¨C sometimes (i.e., eventually) p holds.

¡°eventually process 2 will enter the critical section¡±

¡°Process 2 is in the critical section¡±

Fp

p

? X p ¨C p holds in the next state.

¡°Process 2 will be in the critical section in the next state¡±

Xp

?

G p ¨C always (i.e., globally) p holds.

¡°process 1 and 2 are always mutually exclusive¡±

p

Gp

5

5

? Mentor Graphics Corporation

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

6

6

What We can Express in LTL

?

?

p

p

p

p

p

p

p

p

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

p

p

? Mentor Graphics Corporation

?

Weak operators ¨C X, G, W

Used to express safety properties,

i.e. ¡°something bad never happens¡±

?

Strong operators ¨C F, U

Used to express liveness properties,

i.e. ¡°something good eventually happens¡±

q

[p W q] ¨C ¡°p holds from now until q holds¡± (weak)

pWq

p

HF, UT Austin, Feb 2020

and p holds from now until q holds¡± (strong)

p

p

What We can Express in LTL

[p U q] ¨C ¡°q holds now or sometime in the future

pUq

p

p

p

Safety properties put no obligation on the future, liveness properties do!

7

7

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

8

8

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

2

HF, UT Austin, Feb 2019

? Mentor Graphics Corporation

Introduction to SystemVerilog Assertions (SVA)

What We can Express in LTL

?

What We can Express in LTL

LTL formulas can be combined using the ?, ¡Ä, ¡Å, ¡ú

logic connectors (negation, conjunction, disjunction, implication)

?

For example¡­.

LTL formulas can be combined using the ?, ¡Ä, ¡Å, ¡ú

logic connectors (negation, conjunction, disjunction, implication)

For example¡­.

G ( request ¡ú F grant )

p

p

Temporal operators can be combined too¡­

grant

request

p

G ( request ¡ú F grant )

p

p

p

FG p

p

9

9

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

10

10

What We Cannot Express in LTL

?

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

p

p

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

Regular Expressions

?

Counting example:

Regular expressions describe sets of finite words

w=a1,a2,¡­,an .

¡°p is asserted in every even cycle¡±

¡ª a1,a2,¡­ are letters in an alphabet.

All the following traces satisfy this property

!p,p,!p,p,¡­

p,p, p,p¡­.

p,p,!p,p,p,p¡­

?

Regular expressions can express counting modulo n.

?

The * operator ¨C enables counting modulo n.

¡ª (ab)* - a regular expression describing the set of words:

?

11

11

No LTL formula can express this property

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

12

12

¨C

¦Å - (the empty word)

¨C

ab

¨C

abab

¨C

ababab¡­..

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

3

HF, UT Austin, Feb 2019

? Mentor Graphics Corporation

Introduction to SystemVerilog Assertions (SVA)

Regular Expressions

?

What Regular Expressions Cannot Express

For reactive systems a letter in the alphabet is a Boolean

expression

? The

?

The set of computations satisfying ¡°p is asserted in every even

behavior, ¡°eventually p holds forever¡±

cannot be expressed by a regular expression

cycle¡± is described by the SVA regular expression

(1`b1 ## p)[*]

? It

?

can be expressed in LTL as : F G p

A regular expression by itself is not a property

¡ª Later: building properties from regular expressions in SVA

13

13

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

14

14

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

Linear Formalisms

?

LTL and regular expressions are linear formalisms

¨C Linear formalisms can be used to express mainly properties that are

intended to hold on all computations (i.e., executions of a design

model).

¨C Most properties required for the specification of digital designs can

SVA LANGUAGE STRUCTURE

be expressed using linear formalism

?

What cannot express in linear formalisms:

¡°There exists a computation in which eventually p holds forever¡±

¨C

15

15

LTL implicitly quantifies universally over paths

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

4

HF, UT Austin, Feb 2019

Introduction to SystemVerilog Assertions (SVA)

SVA Language Structure

Assertion

Units

SVA Language Structure

assert property (@(posedge clk) disable iff (~rst_n)

!(grant0 & grant1));

? Checker packaging

Directives

(assert, cover)

? assert, assume, cover

Properties

Sequences

(Sequential Expressions)

Boolean Expressions

? Specification of behavior;

desired or undesired

clk

Assertion

Units

Directives

(assert, cover)

? How Boolean events

are related over time

rst_n

Properties

Sequences

(Sequential Expressions)

? True or false

!(grant0 & grant1)

error

Boolean Expressions

Note: rst_n is an active low reset in this example

17

17

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

18

18

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

SVA Language Structure

?

SVA provides a mechanism to asynchronously

disable a property during a reset using the SVA

disable iff clause

MAPPING SVA INTO LTL

assert property (@(posedge clk) disable iff (~rst_n)

!(grant0 & grant1));

Note: rst_n is an active low reset in this example

19

19

H Foster, EE 382M, Verification of Digital Systems, Spring 2018

? Mentor Graphics Corporation

? Mentor Graphics Corporation

HF, UT Austin, Feb 2020

? Mentor Graphics Corporation

5

HF, UT Austin, Feb 2019

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download