SYSTEMVERILOG

ASSERTIONS FOR
FORMAL VERIFICATION
Dmitry Korchemny, Intel Corp.

HVC2013, November 4, 2013, Haifa

November 4, 2013

Most of the examples used in

this tutorial are borrowed from

our SVA book

HVC2013

November 4, 2013

HVC2013

Agenda
Introduction
Formal verification model. LTL properties
Assertion statements
Sequences and properties
Clocks and resets
Assertion system functions
Metalanguage and checkers
Local variables
Recursive properties
Efficiency and methodology tips
Future directions and challenges

November 4, 2013

HVC2013

INTRODUCTION

November 4, 2013

HVC2013

Hardware Verification Task

SPEC
(Spec
language)

DUT
(RTL)

Does DUT meet the spec?

Simulation
Does DUT meet the spec for given input stimuli?
Formal Verification (FV)
Does DUT meet the spec for any legal input stimuli?

November 4, 2013

HVC2013

SystemVerilog Assertions (SVA)

SystemVerilog (proliferation of Verilog) is a unified

hardware design, specification, and verification language

RTL/gate/transistor level
Assertions (SVA)
Testbench (SVTB)
API

SVA is a formal specification language

Native part of SystemVerilog [SV12]
Good for simulation and formal verification

November 4, 2013

HVC2013

SVA Standardization History

2003
Basic assertion features defined
2005
Improved assertion semantics
2009
Major changes in the language: deferred assertions, LTL support,
checkers
2012
Improved checker usability, final assertions, enhancements in bitvector system functions and in assertion control
Part of SystemVerilog standardization (IEEE 1800)

November 4, 2013

HVC2013

SVA vs. PSL

Formal semantics of SVA is (almost) consistent with the

formal semantics of PSL [PSL10]

Meta-language layers are quite different (e.g., checkers
vs. vunits)
SVA has well-defined simulation semantics; tightly
integrated with other parts of SystemVerilog

November 4, 2013

HVC2013

FORMAL VERIFICATION
MODEL. LTL PROPERTIES

November 4, 2013

HVC2013

10

Linear Time Model. Global Clock

We assume that the time is linear:
There is one global clock (AKA system clock or reference clock)
which always ticks (never stops)
All signal changes are synchronized with the ticks of the global
clock
Global clock introduces the notion of discrete time in the system
0, 1, 2,
Each number corresponds to a tick of the global clock

[Pnu77]

November 4, 2013

HVC2013

11

Global Clock in SystemVerilog

In simulation the natural notion of global clock are simulation

ticks. But such definition makes global clock very expensive

In SystemVerilog there is a special construct for global
clocking definition
May be declared
anywhere in the
design

Default clocking
defines the
default clock for
assertions

module m(input logic clk, );

global clocking @(posedge clk); endclocking

default clocking @$global_clock; endclocking

endmodule : m

global clocking is used in simulation, but usually ignored in FV and emulation

In practice most assertions are written relative to some specific clock,
not relative to the global clock. Will be discussed later

$global_clock
is explicit
designation of
global clock

November 4, 2013

HVC2013

12

Formal Verification Model

Kripke structure:
= , , , 
 Finite set of states
  Set of initial states
 Set of Boolean variables (labels)

:  2 Labeling function mapping each state to the set of
variables that are true in this state
   (Left total) transition relation
Shows to which states it is possible to transition from given state

[Kr63]

November 4, 2013

HVC2013

13

Formal Verification Model. Example

module m(input logic i, clk, output o);
wire a = !i;
global clocking @(posedge clk); endclocking
always @($global_clock) o <= a;
endmodule : m

 = , 
 = ,  ,  , , 
=


November 4, 2013

HVC2013

Symbolic Representation
Each  variable is represented as a pair:
Current value (its value at the current time moment): 
Next value (its value at the next time moment): 
Each set and relation is represented by its characteristic

function

E.g.,  =  

In SystemVerilog there is a notation of next value:

$future_gclk(x)
E.g.,  corresponds to i ^ $future_gclk(o)

Other future sampled value functions:

$rising_gclk(x)
!x & $future_gclk(x) (for bit variables)
$falling_gclk(x)
x & !$future_gclk(x) (for bit variables)
$steady_gclk(x)
x === $future_gclk(x)
$changing-gclk(x)
x !== $future_gclk(x)

14

November 4, 2013

15

HVC2013

Linear Time Model

Linear time FV model defines a number of legal infinite

traces
Specification language describes the properties of these
traces module m(input logic clk, i, output logic o);
global clocking @(posedge clk); endclocking
default clocking @$global_clock; endclocking
always @(posedge clk) o <= !i;
assert property (i |=> !o);
endmodule : m
Feasible
traces
Infeasible
trace

November 4, 2013

HVC2013

16

Linear Time Language (LTL) Properties

Properties are temporal statements that can be true or

false
Properties have a starting point (t), but no end point

Boolean property: e
0

e
2

Nexttime property: nexttime p

0

p
t+1

In SVA there exists also a strong version: s_nexttime

Discussed later

November 4, 2013

17

HVC2013

LTL Properties (cont.)

Always property: always p
p
0

Eventually property: s_eventually p

p
0

November 4, 2013

18

HVC2013

Compound Properties
True from next moment: nexttime always p
p

True from some moment: s_eventually always p

p

Infinitely often: always s_eventually p

p
t

November 4, 2013

Boolean Connectives
Negation: not p
Conjunction: p and q
Disjunction: p or q
Implication: p implies q
Equivalence: p iff q
Condition: if (e) p else q
Case

HVC2013

19

November 4, 2013

HVC2013

20

Counterexample
Counterexample trace witnessing a property failure
In general case infinite
May be finite
Meaning that any infinite extension of this finite trace is a
counterexample

November 4, 2013

21

HVC2013

Safety and Liveness

[AS87, KV01]

Safety properties
All their counterexample are finite
E.g., always e

!e
t

Liveness properties
All their counterexamples are infinite
E.g., s_eventually e
!e

!e

!e

!e

!e

!e

!e

!e

Hybrid properties also exist

Sometimes also called liveness

!e

!e

!e

November 4, 2013

22

HVC2013

LTL Properties. Until

Non-overlapping until
p until q if q does not happen, p holds forever
p s_until q q must eventually happen
p
0

Safety

(General)
liveness

Overlapping until
p until_with q if q does not happen, p holds forever
p s_until_with q q must eventually happen
p
0

p
p and q

Safety

(General)
liveness

November 4, 2013

HVC2013

23

Bounded Versions
Property

Semantics

[s_]nexttime [m] p

[s_]nexttime [s_]nexttime p

[s_]eventually [m:n] p

[s_]nexttime [m] p or or [s_]nexttime [n] p

s_eventually [m:$] p

s_nexttime [m] s_eventually p

[s_]always [m:n] p

[s_]nexttime [m] p and and [s_]nexttime [m] p

always [m:$] p

nexttime [m] always p

November 4, 2013

HVC2013

24

ASSERTION STATEMENTS

November 4, 2013

HVC2013

25

Assertion Kinds
Assertions

Clocked

Concurrent

Unclocked

Immediate

Deferred
2009

Final
2012

November 4, 2013

HVC2013

26

(Concurrent) Assertion Statements

Assertions
Insure design correctness
assert property (p);
Assumptions
Model design environment
assume property (p);
Cover statements
To monitor coverage evaluation
cover property (p);
Restrictions
To specify formal verification constraint
restrict property (p);

November 4, 2013

27

HVC2013

Assertion Placement
Inside initial procedure execute only once
Outside of initial procedure execute continuously
Once

initial
assert property(p);
Expresses pure
semantics, but
rarely used

initial assert property(rst);

assert property(p);
Implicit always

p is always true
assert property(ok);

rst is high at time 0

Every clock
tick
always p is true at time 0
ok is always high

November 4, 2013

HVC2013

Assertions
Specify requirements from DUT
FV
Mathematically proves assertion correctness
DV
Checks assertion correctness for given simulation trace

initial assert property (p);

Passes iff p is true at time 0 on all feasible traces

Fails iff p is false at time 0 on some feasible trace

28

November 4, 2013

HVC2013

29

Assumptions
Specify requirements from environment
FV
Restricts the set of feasible traces in the model
DV
Checks assertion correctness for given simulation trace
assume property (in == !inv_in)
else $error(Inputs in and inv_in are expected to be inverse);

From FV point of view, the DUT acts as an assumption

Contradictory assumptions (with each other or with the

model) cause all assertions to pass

This is called an empty model

November 4, 2013

HVC2013

Restrictions
Specify condition for which FV has been performed
FV
Restricts the model
Same as assumption

DV
Completely ignored

restrict property (opcode == OP_ADD);

30

November 4, 2013

HVC2013

31

Cover
Specify scenario you wish to observe
FV
Mathematically prove that the property holds on some feasible
trace
DV
Capture scenario in simulation trace
cover property (read[*2]);

From FV point of view

initial cover property (p);

initial assert property (not p);

passes

fails

November 4, 2013

HVC2013

Formal View on Assertions and

Assumptions
Set of assumptions
initial assume property (q_1);

initial assume property (q_m);
and assertions
initial assert property (p_1);

initial assert property (p_n);
is equivalent to the following single assertion
initial
assert property (q_1 and and q_m
implies p_1 and p_n);

32

November 4, 2013

HVC2013

33

Sampling
Signal values are sampled at the beginning of simulation

tick

Time Step
sample here
sig

clock

November 4, 2013

HVC2013

SEQUENCES AND
PROPERTIES

34

November 4, 2013

HVC2013

35

Sequence
Informal definition
Sequence is a rule defining a series of values in time
A sequence does not have a truth value, it has one initial

point and zero or more match points

When a sequence is applied to a specific trace, it defines

zero or more finite fragments on this trace starting at the

sequence initial point and ending in its match points
Essentially, sequence is a regular expression

November 4, 2013

HVC2013

36

Example
Read is followed by write in one or two clock ticks
read ##[1:2] write
Let starting point of this sequence be t = 2

No match
Single match at 3

Single match at 4
2

Two matches (at 3 and 4)

2

November 4, 2013

HVC2013

37

Boolean Sequence
Boolean expression e defines the simplest sequence a

Boolean sequence
This sequence has a match at its initial point if e is true
Otherwise, it does not have any satisfaction points at all

November 4, 2013

HVC2013

38

Sequence Concatenation
Sequence concatenation: r ##1 s
There is a match of sequence r ##1 s if there is a match of
sequence r and there is a match of sequence s starting from the
clock tick immediately following the match of r
In other words, a finite trace matches r ##1 s iff it can be split into two

adjacent fragments, the first one matching r, and the second one
matching s.

November 4, 2013

HVC2013

39

Sequence Fusion
Sequence fusion r ##0 s is an overlapping concatenation
The fusion of sequences r and s, is matched iff for some match of
sequence r there is a match of sequence s starting from the clock
tick where the match of r happened

November 4, 2013

HVC2013

40

Zero Repetition (Empty Sequence)

s[*0]
sequence admitting only an empty match
Matches on any trace but the trace fragment is empty (does not contain

clock ticks)

November 4, 2013

HVC2013

41

Sequence Disjunction
Sequence disjunction r or s is a sequence which has a

match whenever either r or s (or both) have a match

November 4, 2013

HVC2013

Consecutive Repetition
Repetition
r[*0] is an empty sequence
If n > 0 (const.)
r[*n]
r[*n-1] ##1 r

Finite repetition range

r[*n:n]
r[*n]

r[*m:n]
r[*m:n-1] or r[*n] m

<n

42

November 4, 2013

HVC2013

43

Infinite Repetition Range

Infinite range: repeat s n or more times
Formal definition
Sequence s[*1:$] matches trace fragment i : j if it is possible to
divide this trace fragment into one or more consecutive fragments
so that each such fragment matches s
s[*0:$]
s[*0] or s[*1:$]
s[*n:$]
s[*0:n-1] or s[*1:$], n > 1
Shortcuts (SVA 2009)
s[*]
s[*0:$] Zero or more times
s[+]
s[*1:$] One or more times
s[*n:$] does not mean that sequence s is repeated infinitely many
times, but that it is repeated n or more (finite) number of times

November 4, 2013

HVC2013

44

Sequence Concatenation and Delay

r ##0 s is a sequence fusion
r ##1 s is a sequence concatenation
r ##n s, where n > 1 is defined recursively
r ##n s
r ##1 1[*n-1] ##1 s

##n s
1[*n] ##1 s

November 4, 2013

HVC2013

45

Delay Ranges
r ##[0:0] s
r ##0 s
r ##[m:n] s
(r ##1 1[*m-1:n-1] ##1 s), where n m > 0
r ##[0:n] s
(r ##0 s) or (r ##[1:n] s), where n > 0
r ##[m:$] s
(r ##1 1[*m-1:$] ##1 s), where m > 0
r ##[0:$] s
(r ##0 s) or (r ##[1:$] s), where n > 0
##[m:n] s
1 ##[m:n] s, where n m 0
##[m:$] s
1 ##[m:$] s, where m 0
Shortcuts (SVA 2009)
##[*]
##[*0:$]
##[+]
##[*1:$]

November 4, 2013

HVC2013

Other Sequence Operators

Go to repetition: e[->n], e[->m:n]
e is a Boolean
Non-consecutive repetition: e[=n], e[=m:n]
e is a Boolean
Intersection: r intersect s
Conjunction: r and s
Containment: r within s
Throughout: e throughout s
First match: first_match(r)
Sequence methods
r.triggered
r.matched

46

November 4, 2013

HVC2013

47

Sequential Property
Strong sequential property
strong(s) is true in clock tick i iff sequence s with initial point i has
a match
Sequence s should not admit an empty match
Weak sequential property
weak(s) is true in clock tick i iff there is no finite trace fragment i : j
witnessing inability of sequence s with the initial point i to have a
match.
Sequence s should not admit an empty match
In assertions, assumptions and restrictions weak may be

omitted
In cover statements strong may be omitted

November 4, 2013

HVC2013

Sequential Properties. Examples

initial assert property (rst[*2]);
Same as initial assert property (weak(rst[*2]));
For global clock it is also the same as initial assert property

(strong(rst[*2]));

initial assert property (rst[*]);

Admits empty match

initial assert property (rst[*] ##1 ready);

Same as initial assert property (rst until ready);
initial assert property (strong(rst[*] ##1 ready));
Same as initial assert property (rst s_until ready);
initial assert property (##[*] ready);
Tautology
initial assert property (strong(##[*] ready));
Same as initial assert property (s_eventually ready);

48

November 4, 2013

HVC2013

49

Suffix Implication
A suffix implication is a property built from a sequence (s)

and a property (p)

s antecedent triggering condition
p consequent checked when triggering condition holds
Suffix implication is true when its consequent is true upon each

completion of its antecedent

Overlapping implication: s |-> p

consequent is checked starting from the moment of every
nonempty match of the antecedent
Nonoverlapping implication: s |=> p
consequent is checked starting from the next clock tick of every
match of the antecedent
For singly-clocked properties
s |=>p
s ##1 1 |-> p

November 4, 2013

HVC2013

Examples
Request must be granted
1. assert property (req |-> s_eventually gnt);
2. assert property (req |=> s_eventually gnt);
Both assertions allow sending one grant to multiple requests
Request must be granted in 3 cycles
1. assert property (req |-> ##3 gnt); or
2. assert property (req |=> ##2 gnt);
Request must be active until grant is asserted
1. assert property(req |-> req until grant);
2. assert property(req |-> req until_with grant);
3. assert property(req |-> req s_until grant);
4. assert property(req |-> req s_until_with grant);
Two consecutive alerts must be followed by reset
assert property (alert[*2] |=> reset);

50

November 4, 2013

HVC2013

51

Vacuity
What do we check in previous assertions if requests

cannot be produced by the model?

Assertion holds vacuously if it is redundant
E.g., the previous assertions may be rewritten in this case as

assert property (not req);

FV tools provide vacuity check

The cost is rather high

[Ar03]

November 4, 2013

HVC2013

52

Suffix Conjunction
A suffix conjunction is a property built from a sequence (s)

and a property (p)

s antecedent triggering condition
p consequent checked when triggering condition holds
Suffix conjunction is true when its consequent is true upon at least

one completion of its antecedent

Overlapping conjunction: s #-# p

Nonoverlapping conjunction: s #=# p
Example:
Reset is initially high and when it becomes low it remains low
forever
Passes if rst is
initial assert property (rst[+] ##1 !rst |=> always !rst);

always high

initial assert property (rst[+] ##1 !rst #=# always !rst);

Fails if rst is
always high

November 4, 2013

CLOCKS

HVC2013

53

November 4, 2013

HVC2013

54

Clocks
Assertion clock should be explicitly written or inferred from

the default clocking

assert property (@clk p);
assert property (@(posedge clk) p);
default clocking @(posedge clk); endclocking

assert property (p);

November 4, 2013

HVC2013

55

Clock Rewriting
Unless clock is not inferred as a system clock (=global

clock) by an FV tool, the corresponding property is

rewritten
Examples
assert property (@(posedge clk) e);
assert property ($rising_gclk(clk) |-> e);
assert property (@(posedge clk) req |=> gnt);
assert property (($rising_gclk(clk) & req ##1 $rising_glck(clk)|-> gnt);

November 4, 2013

HVC2013

56

Clock Fairness
Clock is fair if it ticks infinitely many times
Without any preliminary knowledge clock fairness is not

guaranteed
Clock may stop ticking at some moment

Global clock is fair by its definition

November 4, 2013

HVC2013

Clock Fairness (cont.)

Clock defines a subtrace
Only moments corresponding to clock ticks are retained

When clock is fair the subtrace is infinite

Formal semantics does not change
When clock is not fair the subtrace is finite
Need to define property semantics on finite trace

57

November 4, 2013

HVC2013

58

Weak and Strong Properties

Weak operators do not require clock to tick
Strong operators require clock to tick enough times
Example
nexttime weak version
s_nexttime strong version
initial assert property (@clk nexttime p);
initial assert property (@clk s_nexttime p);

Passes iff either p is

true at time 1 or clk
ticks less than two
times

Passes iff clk ticks at

least two times and p is
true at time 1

November 4, 2013

HVC2013

59

Weak and Strong Properties. Negation

Negation inverts weakness
E.g., not, antecedent in implies
Example
not always p
s_eventually not p

November 4, 2013

HVC2013

60

Mixing Weak and Strong Properties

Mixing weak and strong properties in most cases in non-

intuitive and should be avoided

Also for performance reasons

Example
s_nexttime always p
Clock should tick at least twice and p should true at each clock tick

starting from time t + 1

In some cases mixing is meaningful
s_eventually always p fairness
always s_eventually p

November 4, 2013

HVC2013

Multiply Clocked Properties

SVA supports multiply clocked properties
assert property(@(posedge clk1) a |=> @(posedge clk2) b);

61

November 4, 2013

RESETS

HVC2013

62

November 4, 2013

HVC2013

63

Resets and Aborts

Reset and abort operators operators to stop property

evaluation when some condition is met

Simplify writing assertions in presence of hardware resets

disable iff main reset of an assertion

Aborts
Asynchronous
accept_on
reject_on

Synchronous
sync_accept_on
sync_reject_on

November 4, 2013

HVC2013

64

Aborts
Asynchronous aborts
Ignore the actual clock
Checked at each time step

Synchronous aborts
Checked at clock ticks only
Informal semantics
accept_on (cond) p, sync_accept_on (cond) p
True if there is no evidence of the failure of p before the abort condition

has become true

reject_on (cond) p, sync_reject_on (cond) p
False if there is no evidence of the success of p before the abort

condition has become true

November 4, 2013

HVC2013

Asynchronous Aborts. Example

assert property(@(posedge clk)
accept_on (retry) a |=> reject_on(bad) b[*2]);

65

November 4, 2013

HVC2013

66

Synchronous Aborts. Example

assert property(@(posedge clk)
sync_accept_on (retry) a |=> sync_reject_on(bad) b[*2]);

November 4, 2013

HVC2013

67

One More example

reject_on(rst) 1[*3]
Property 1[*3] can never fail
Therefore, reject_on(rst) 1[*3] fails iff rst becomes high any time
during first three clock cycles
sync_reject_on(rst) 1[*3] is equivalent to !rst[*3]

November 4, 2013

HVC2013

68

Disable Clause
Syntax
disable iff (expression)
Specifies top-level assertion reset
At most one in the entire assertion
In FV may be regarded as accept_on in assertions and

assumptions, and as reject_on in cover statements

Formally introduces a notion of disabled evaluation

Evaluation is disabled if the assertion evaluation has been aborted
because the disable condition became true
Disable condition is checked continuously, and it is not

sampled

This definition introduces inconsistency between simulation and FV

November 4, 2013

HVC2013

69

Disable Clause (cont.)

default disable iff may be used to specify the default

disable condition
module m (input logic reset, rst, req, gnt, clk, );
default disable iff reset;
a1: assert property (@(posedge clk) req |=> gnt);
a2: cover property (@(posedge clk) req ##1 gnt);
a3: assert property (@(posedge clk) disable iff (1b0) a |=> b);
a4: assert property (@(posedge clk) disable iff (rst) a |=> b);
endmodule : m

November 4, 2013

HVC2013

ASSERTION SYSTEM
FUNCTIONS

70

November 4, 2013

71

HVC2013

Bit-Vector System Functions

Name

Description

$onehot0

Check that at most one bit in a vector is high

$onehot

Check that exactly one bit in a vector is high

$countones

Count number of bits in a vector with value high

$countbits

Count number of bits having specific value

$isunknown

Check whether a vector has a bit with value x or z

November 4, 2013

HVC2013

Sampled Value Functions

Name

Description

$sampled

Return sampled value of expression

$past

Return past value of expression

$rose

Check whether expression value rose

$fell

Check whether expression value fell

$changed

Check whether expression value changed

$stable

Check whether expression value remained stable

72

November 4, 2013

Past Sampled Values

$past(e, n, en, @clk)
e expression
n 1 constant expression
specifying the number of
clock ticks (delay)
en gating expression for
the clocking event
clk clocking event

HVC2013

73

November 4, 2013

HVC2013

74

Values Before Initial Clock Tick

What happens if for a given time-step there are not

enough previous clock ticks?

$past(e) returns an initial value of e

The initial value of e is that as computed using the initial

values stated in the declaration of the variables involved

in e
If a static variable has no explicit initialization, the default value of

the corresponding type is used, even if the variable is assigned a

value in an initial procedure
FV tools may ignore variable initialization everywhere, except in
checker constructs. Also, many FV tools consider all variables to be of
two-state value type, and therefore they assume that $past(e) is 0 in
clock tick 0 for any e

November 4, 2013

HVC2013

75

Other Sampled Value Functions

$rose(e, @clk)

$past(LSB(e),,,@clk)!== 1 && $sampled(LSB(e))=== 1

$fell(e, @clk)

$past(LSB(e),,,@clk)!== 0 && $sampled(LSB(e))=== 0

$changed(e, @clk)

$past(e,,,@clk)!== $sampled(e)
$stable(e, @clk)

$past(e,,,@clk)=== $sampled(e)

November 4, 2013

HVC2013

76

Global Clocking Sampled Value Functions

May be used only if global clock has is defined
Past
$past_gclk(e)
$past(e, 1, 1, @$global_clock)
$rose_gclk(e)
$rose(e, @$global_clock)
$fell_gclk(e)
$fell(e, @$global_clock)
$changed_gclk(e)
$changed(e, @$global_clock)
$stable_gclk(e)
$stable(e, @$global_clock)
Future
$future_gclk(e) Sampled value of e in the next tick of the global clock
$rising_gclk(e)
$sampled(LSB(e))!== 1 && $future_gclk(LSB(e)) === 1
$falling_gclk(e)
$sampled(LSB(e))!== 0 && $future_gclk(LSB(e)) === 0
$changing_gclk(e)
$sampled(e) !== $future_gclk(e)
$steady_gclk(e)
$sampled(e) === $future_gclk(e)
Cannot be nested or used in reset conditions

November 4, 2013

HVC2013

METALANGUAGE

77

November 4, 2013

HVC2013

78

Let Declaration
let identifier [(port, port, )] = expression;

Compile-time macro for integral expressions

Follow normal scoping rules
Formal arguments may be typed or untyped
Formal arguments can have default actual arguments
May be included in a package
May easily be processed by tools for linting and statistical
reporting

Typical usage
Templates for Boolean assertions
Instrumental code
Does not introduce new variables
Visible to debuggers

November 4, 2013

HVC2013

Let Example
module m (input logic clk, rst, );
logic mod1, mod2;
logic req1, req2;
logic rsp;
let req = mod1 & req1 | mod2 & req2;
let gnt = $changed(rsp);

a: assert property (@(posedge clk) disable iff (rst) req |=> gnt);
endmodule : check

79

November 4, 2013

HVC2013

80

Sequence and Property Declaration

module m(input logic clk, rst, );
logic my_req;
logic gnt;
sequence two_reqs(req);
req[*2];
endsequence
property delayed_grant(int n);
nexttime [n] gnt;
endproperty

req_granted: assert property (@(posedge clk) disable iff (rst)

two_reqs(my_req) |-> delayed_grant(2);
endmodule

November 4, 2013

CHECKERS

HVC2013

81

November 4, 2013

HVC2013

Checkers
Checkers are SystemVerilog containers to package

verification code
Both assertions and modeling

Checker is a kind of hybrid of module, property and

assertion
May contain (almost) the same constructs as a module
Is instantiated as a property (in place)
Placed as an assertion
Acts as an assertion with complex internal implementation

82

November 4, 2013

83

HVC2013

Example. Sequential Protocol

Whenever start is high, dataIn is valid.
Whenever complete is high, dataOut is valid.
If start is high, then the value of dataIn at that time must equal the value of dataOut at the next strictly

subsequent cycle in which complete is high

If start is high, then start must be low in the next cycle and remain low until after the next strictly

subsequent cycle in which complete is high

complete may not be high unless start was high in a preceding cycle and complete was not high in any of

the intervening cycles

start

complete

dataIn

dataOut

November 4, 2013

HVC2013

84

Sequential Protocol Verification Checker

checker seq_protocol (start, complete, dataIn, dataOut, event clk);
default clocking @clk; endclocking
var type(dataIn) data;
property match (first, last);
always_ff @clk

first |=> !first until_with last; endproperty

if (start) data <= dataIn;

a_data_check: assert property (complete |-> dataOut == data);

a_no_start: assert property (match(start, complete));
a_no_complete: assert property (match(complete, start));
initial
a_initial_no_complete: assert property (!complete throughout start[->1]);
endchecker : seq_protocol

November 4, 2013

HVC2013

85

Checker Binding
module top;
logic clock, snda, sndb, sndc, rcva, rcvb, rcvc;
...
trans ta (clock, snda, rcva);
trans tb (clock, sndb, rcvb);
trans #(2) tc (clock, sndc, rcvc);
endmodule : top
checker eventually_granted (req, gnt, );

endchecker : eventually_granted
checker request_granted (req, gnt, n, );

endchecker : request_granted

module trans #(DEL=1) (input logic clock, in, output logic out);
if (DEL == 1) begin : b
always @(posedge clock) out <= in;
end
else begin : b
logic [DEL - 2: 0] tmp;
always @(posedge clock) begin
tmp[0] <= in;
for (int i = 1; i < DEL - 1; i++) tmp[i] <= tmp[i-1];
out <= tmp[DEL - 2];
end
end
endmodule : trans

bind trans eventually_granted check_in2out(in, out, posedge clock);

bind trans: ta, tb request_granted delay1(in, out,, posedge clock);
bind trans: tc request_granted delay2(in, out, 2, posedge clock);

November 4, 2013

HVC2013

86

Free Variables
Checker may have free variables
Behave non-deterministically (like free or constrained inputs)
FV: consider all possible values imposed by assumptions and

assignments
Simulation: their values are randomized
Free variable values are never sampled

Limitations
Continuous and blocking assignments to free variables are illegal
rand bit r;
bit [2:0] x;

assign x = r ? 3d3 : 3d5;

rand bit a;
always_ff @clk a <= !a;

November 4, 2013

HVC2013

Rigid Variables
Rigid variables = constant free variables

checker data_consistency (start, complete, dataIn, dataOut,

event clk, untyped rst);
default clocking @clk; endclocking
default disable iff rst;
rand const type(dataIn) data;

Rigid
variable

a1: assert property (start && data == dataIn ##1 complete[->1]

|-> dataOut == data);
endchecker : data_consistency

87

November 6, 2013

Intel Confidential

88

Modular Assertion Modeling

checker check_fsm(logic [1:0] state, event clk);
logic [1:0] astate = IDLE; // Abstract state
model_fsm c1(state, clk, astate);
check_assertions c2(state, astate, clk);
endchecker
checker model_fsm(input event clk, output logic [1:0] astate = IDLE);
always @clk
case (astate)
IDLE: astate <= ;

default: astate <= ERR;

endcase
endchecker
checker check_ assertions(state, astate, event clk);
default clocking @clk; endclocking
a1: assert property (astate == IDLE <-> state inside {IDLE1, IDLE2});
//
endchecker

November 6, 2013

Intel Confidential

89

Implementing Formal Verification

Environment With Checkers

In simulation module
input signals are
randomized remaining
mutually exclusive

checker env(event clk, output logic out1, out2);

rand bit a, b;
m: assume property (@clk $onehot0({a, b}));
assign out1 = a;
assign out2 = b;
endchecker : env

module m(input logic in1, in2, clock, output );

endmodule : m
module top();
logic clock, n1, n2;

m m1(n1, n2, clock, );

evn env1(clock, n1, n2);
endmodule : top

November 4, 2013

HVC2013

LOCAL VARIABLES

90

November 4, 2013

HVC2013

91

Informal Definition
Local variable is a variable associated with an evaluation attempt
Local variables are not sampled

checker data_consistency (start, complete, dataIn, dataOut,

event clk, untyped rst);
default clocking @clk; endclocking
default disable iff rst;
Local
property p_data_check;
variable
var type(dataIn) data;
(start, data = dataIn) ##1 complete[->1] |-> dataOut == data;
endproperty : p_data_check
Match
item
a1: assert property (p_data_check);
endchecker : data_consistency

November 4, 2013

HVC2013

92

Example
Check that the value of dataIn when start is high

coincides with the value of dataOut read in n clock ticks

If n = const
assert property (start |-> ##n dataOut == $past(dataIn, n) );

If n is not const
property data_check;
var type(n) ctr;
(start, ctr = n - 1) ##1 (ctr > 0, ctr--)[*] ##1 (ctr == 0)
|-> dataOut = dataIn;
endproperty : data_check
assert property (data_check);

November 4, 2013

HVC2013

93

Local vs. Rigid Variables

Local variables are broader than rigid variables
They are mutable
Local variables are more intuitive
Local variables are supported in simulation, rigid variables

are not
Rigid variables are FV friendly their implementation is
straightforward
Efficient implementation of local variables in FV is challenging

November 4, 2013

HVC2013

94

RECURSIVE PROPERTIES

November 4, 2013

HVC2013

95

Recursive Properties
Properties may be recursive
property prop_always (p) ;
p and nexttime prop_always (p);
endproperty
initial assert property (@(posedge clk) prop_always (ok));
property prop_weak_until (p, q);
q or (p and nexttime prop_weak_until (p, q));
endproperty
initial assert property (@(posedge clk) prop_weak_until (req, gnt));

November 4, 2013

HVC2013

EFFICIENCY AND
METHODOLOGY TIPS

96

November 4, 2013

HVC2013

97

Assertion Compilation for FV

Assertions are usually compiled into finite automata [Var96]
Typical for FV and emulation
Sometimes done for simulation as well
Safety assertions are compiled into (conventional) finite

automata on finite words

Liveness and hybrid assertions are compiled into finite
automata on infinite words (e.g., Bchi automata):
Finite automata on finite words + fairness conditions

Complexity of automaton reflects well FV efficiency

Another factor is the number of state variables in the model

November 4, 2013

HVC2013

98

Automaton-Based Compilation. Example

true
a

always a ##1 b |=> c

always a[*3] ##1 b |=> c
always a[+] ##1 b |=> c

!c

true
a

true
a

!c

!c

November 4, 2013

HVC2013

99

Avoid Large and Distant Time Windows

assert property (start ##1 !complete[0:1000] ##1 complete |=> done);

assert property (start ##1 complete[->1] |=> done);

assert property (start ##1 !complete[*] ##1 complete |=> done);

Also applies to bounded property operators and $past

November 4, 2013

HVC2013

100

Avoid Using Liveness Assertions Unless

Really Needed
Request must be active until grant is asserted



assert property(req |-> req s_until grant);

assert property(req |-> req until grant);

Clock is fair



Do you really want

to check that grant
is eventually
received?

Strong operators
have clumsier
syntax to prevent
inadvertent
usage

assert property (s_eventually clk);

assert property (req |-> ##[1:1000] gnt);

assert property (req |-> s_eventually gnt);

Liveness assertion
is usually better
than a safety
assertion with a
large time window

November 4, 2013

101

HVC2013

Avoid Mixing Weak and Strong Properties

s_nexttime always p

nexttime s_eventually p

nexttime always p

s_nexttime s_eventually p

Sometimes this is unavoidable

always s_eventually p

November 4, 2013

HVC2013

102

Past vs. Future

Future value functions are cheap in FV
Recall that each variable is represented as a pair (v, v')
Past value functions are more expensive
They introduce new flip-flops (=variables)
Need to optimize the usage of $past
logic check;
logic [31:0] a, b, c;



assert property (##1 check |-> $past(c) == $past(a) + $past(b));

assert property (##1 check |-> $past(c == a + b));

November 4, 2013

103

HVC2013

Intersection Family
Sequence operators from intersection family (intersect, and, within)

are expensive
These operators are not inefficient by themselves, but allow to concisely

code complex sequences

Use only where appropriate

Each transaction should contain two read requests and three write requests
Common case

assert property (start |-> read[=2] intersect write[=3] intersect complete[->1]);

If known that all reads come after writes

assert property (start |-> write[=3] ##1 read[=2] intersect complete[->1]);

Top-level conjunction in a sequence promoted to property is not

expensive

assert property (en |-> r and s);

assert property (en |-> (r and s) ##1 a);

This is rather
efficient

November 4, 2013

HVC2013

104

Assertion Clock
Assertions governed by a global clock are more efficient

in FV than assertions governed by an arbitrary clock

true
a

true

!c

!@clk
a & @clk

always a ##1 b |=> c

!@clk
b & @clk

!c & @clk

@clk always a ##1 b |=> c

FV tools may automatically infer the global clock from a singly clocked design

November 4, 2013

HVC2013

105

Local vs. Free and Rigid Variables

Implementing free and rigid variables is straightforward in

FV
Implementing local variables is tricky
Important advantage of local variables
Allow checking assertions in simulation

Both are usually expensive

Efficiency is strongly dependent on FV tool
May need to experiment

November 4, 2013

HVC2013

106

Assignments vs. Assumptions

Assignments are usually more efficient than assumptions
They add directionality to the search
Compare
assign x = !y;
vs.
assume property (x != y);

November 4, 2013

HVC2013

107

Overlapping vs. Nonoverlapping

Transactions
Nonoverlapping transactions may be modeled

deterministically
Overlapping transactions usually require nondeterministic
modeling
E.g., local or rigid variables

Compare:
Sequential protocol vs.

property p_data_check;
var type(dataIn) data;
(start, data = dataIn) ##1 complete[->1] |->
dataOut == data;
endproperty : p_data_check

If it is known that transactions cannot overlap, model them as nonoverlapping

November 4, 2013

HVC2013

108

Be More Specific
Being more specific usually pays off. Check only what you

really need
Dont check for eventuality unless this is essential
If events are ordered in a sequence specify this order explicitly
If you know that transactions do not overlap model this fact

explicitly

Nulla regula sine exceptione

Liveness assertions are usually more efficient than safety
assertions with large/distant time windows
Being more specific comes at a price of generality
However, generality does not help if performance problems prevent us

from getting result

November 4, 2013

HVC2013

109

Efficiency: Simulation vs. FV

Simulation and FV efficiency requirements may be

inconsistent
Especially when assertion simulation has a transaction-based

implementation

E.g.
Infinite ranges and repetitions are efficient in FV, but not in
simulation
Sequence intersection is efficient in simulation, but not in FV
Liveness does not cost in simulation
Future value functions are more efficient than past value functions
in FV. The situation with simulation is opposite
Local variables are rather efficient in simulation, but not in FV

November 4, 2013

HVC2013

110

FUTURE DIRECTIONS AND

CHALLENGES

November 4, 2013

HVC2013

111

Convergence Between SVA and SVTB

Coverage features are divided between SVA and SVTB
Assertion coverage belongs to SVA
Covergroups belong to SVTB
Currently there is no organic connection between the two
Syntax and semantics are absolutely different
One can consider temporal coverage specification by

integrating sequences and covergroups

November 4, 2013

HVC2013

112

Standard Packages
SVA provides basic assertion capabilities and some

sugaring
There are many useful properties and functions that could be

reused, but are not a basic part of the language

It makes sense to standardize them by creating standard property
packages
PSL has some of such common properties embedded into the

language, e.g., never, before, next_event, etc.

November 4, 2013

HVC2013

113

Assertion Libraries
Using SVA checker mechanism it is possible to create a

powerful and flexible standard assertion library with

concise library assertion invocation
Kind of next generation OVL

November 4, 2013

HVC2013

114

AMS Assertions
AMS = Analog and Mixed Signals
The intention is to merge SystemVerilog and Verilog-AMS
This includes development of AMS assertions and including them
into SVA
The initial step was done in SV2012: real type support in SVA
No continuous time support yet

November 4, 2013

HVC2013

TLM Assertions
SVA covers RTL assertions
TLM assertions are different
Unclocked or approximately clocked
SVA is too low level for TLM
Need to extend SVA to cover TLM needs

115

November 4, 2013

HVC2013

116

Checkers for UVM

UVM Universal Verification Methodology
Widely used in verification
Includes verification level monitors to check design

correctness
Part of TB
Uses completely different mechanism, does not explore the

strength of assertions
Implemented as class methods

Challenge
Checkers currently cannot be instantiated in classes
Need to enhance them to allow their usage in UVM

November 4, 2013

HVC2013

BIBLIOGRAPHY

117

November 4, 2013

HVC2013

118

[Ar03] - R.Armoni et al., Enhanced Vacuity Detection in Linear

Temporal Logic, 2003

[AS87] - B. Alpern, F.B. Schneider, Recognizing safety and
liveness, 1987
[Kr63] - S. Kripke. Semantical Considerations on Modal Logic,
1963
[KV01] - O. Kupferman, M.Y. Vardi, Model checking of safety
properties, 2001
[Pnu77] - A. Pnueli. The temporal logic of programs, 1977
[PSL10] - IEEE Standard for Property Specification language
(PSL), 2010
[SV12] - IEEE Standard for SystemVerilog, 2012
[Var96] - M. Vardi. An Automata-Theoretic Approach
to Linear Temporal Logic, 1996