System Verilog

ASSERTIONS

ROHIT KHANNA
 Assertions and Coverage

 Assertions
These are checks which used to verify that your design meets
the given requirements.
Example: grant should be high two clock cycles after request

 Coverage
These are used to judge what percentage of your test plan or
functionality has been verified.
They are used to judge quality of stimulus.
They help us in finding what part of code remains untested.

System Verilog Assertions

 Assertions

Design Rule : Grant should be asserted 2 clock cycles after request

Clock

Request

Assertion Passed
Grant

Assertion Failed
Grant

System Verilog Assertions

 Assertions

 Types of Assertions
Immediate Assertions.
Concurrent Assertions.

System Verilog Assertions

 Immediate Assertions

 These are used to check condition at current time.

 These checks are Non Temporal i.e. checks are not performed
across time or clock cycles.

 These are used inside procedural blocks (initial/always and

tasks/functions).

 Assertion fails if expression evaluates to 0, X or Z.

[Label] : assert (expression) [pass _statement];

[else fail_statement;]

System Verilog Assertions

 Example

Design Rule : State Machine should go to REQ state only if req1 or

req2 is high.

clk

req1

req2

state IDLE REQ IDLE REQ IDLE REQ

System Verilog Assertions

 Example

always @ (posedge clk)

if (state==REQ) //if current state is REQ
assert ( req1 || req2) //Check whether req1 or
//req2 is high
$info(“Correct State”);
else
$error(“Incorrect State”);

System Verilog Assertions

 Assertions Severity

 $info indicates that the assertion failure carries no specific

severity. Useful for printing some messages.

 $warning indicates runtime warning. Can be used to indicate non

severe errors.

 $error indicates runtime error. Can be used to indicate protocol

errors.

 $fatal indicates fatal error that would stop simulation.

System Verilog Assertions

 Examples

always @ (posedge clk)

assert(func(a, b)) ->myevent; else error=error + 1;
//Trigger myevent if function returns 1 else increase error count.

always @ (negedge clk)

assert (y==0) error_flag=0; else error_flag=1;
//y should not be 1 at negedge of clk

always @ (state)
assert(state==$onehot) else $fatal;
//In a one-hot encoded state machine all states should be one-hot

System Verilog Assertions

 Concurrent Assertions

 These assertions test for a sequence of events spread over

multiple clock cycles i.e. they are Temporal in nature.

 property keyword is used to define concurrent assertions.

 property is used to define a design specification that needs to be

verified

 They are called concurrent because they occur in parallel with

other design blocks.

[Label] : assert property (property_name) [pass_statement];

[else fail_statement;]
System Verilog Assertions
 Assertions

Design Rule : Grant should be high 2 clock cycles after request,

followed by low request and then grant in consecutive cycles.

Clk

Req

Assertion Passed
Gnt

Gnt Assertion Passed

System Verilog Assertions

 Example

property req_gnt;
@ (posedge clk) req ##2 gnt ##1 !req ##1 !gnt;
endproperty
assert property(req_gnt) else (“req_gnt property violated”);

 ## followed by a number is used to indicate no. of clock

cycles.

 If gnt is not high 2 clock cycles after req goes high, violation
will be reported.

 If req and gnt come at proper time but req is not low in next
clock cycle, that will also lead to violations.
System Verilog Assertions
 Assertion Region

Preponed Active Values are sampled in

Preponed Region
Sample Data
before entering Inactive
current time slot
(#1step) NBA

From Current Time Slot Observed Evaluated in Observed Region

True / False statements

To Next Time Slot Re-Active
executed in Re-Active Region
$strobe, $monitor,
Re-Inactive
PLI Calls

Postponed Re-NBA

System Verilog Assertions

 Properties and Sequences

 Assertions can directly include a property.

assert property (@ (posedge clk) a ##1 b);

 Assertions can be split into assertion and property declared

separately
property myproperty;
@ (posedge clk) a ##1 b ##1 c;
endproperty
assert property (myproperty);

System Verilog Assertions

 Properties and Sequences

 A property can be disabled conditionally

property disable_property;
@ (posedge clk) disable iff (reset)
a ##1 b ##1 c;
endproperty

 property block contains definition of sequence of events.

 Complex properties can be structured using multiple sequence

blocks.

System Verilog Assertions

 Properties and Sequences

sequence s1; sequence s2;

a ##1 b ##1 c; a ##1 c;
endsequence endsequence

property p1;
@ (posedge clk) disable iff (reset) assert property(p1);
s1 ##1 s2;
endsequence

System Verilog Assertions

 Sequences

 Sequence is series of true/false expression spread over one

or more clock cycles.

 It acts like basic building block for creating complex property

specifications.

 Sampling edge can be specified inside a sequence. If not

defined, it is inferred from property block or assert block.

sequence s1;
@(posedge clk) a ##1 !b ##1 c ##0 !d;
endsequence

System Verilog Assertions

 Linear Sequences

 Linear sequence is finite list of System Verilog Boolean

expression in a linear order of increasing time.

 A sequence is set to match if all these conditions are true:

o The first boolean expression evaluates to true at the first
sampling edge.
o The second boolean expression evaluates to true after the
delay from first expression.
o and so forth, up to and including the last boolean
expression evaluating to true at the last sampling edge.

 Sequence is evaluated on every sampling edge.

System Verilog Assertions

 Example

module test; program assert_test;

bit clk; initial begin
logic a=0, b=0, c=0; #4 a=1;
#10 a=0; b=1;
always #5 clk=~clk; #10 b=0; c=1;
property abc; #10 c=0;
@ (posedge clk) a ##1 b ##1 c; #10 a=1;
endproperty #20 b=1;
assert property(abc)” #10 c=1;
$info(“Sequence Occurred”); #10;
//program block end
endmodule endprogram

System Verilog Assertions

 Example

clk

Error Reported Evaluation in progress Sequence Occurred

System Verilog Assertions
 Declaring Sequences

 A sequence can be declared inside:

o Module
o Interface
o Program
o Clocking block
o Package

 Syntax:
sequence sequence_name [ (arguments) ];
boolean_expression;
endsequence [ : sequence_name]
System Verilog Assertions
 Sequence Arguments

 Sequences can have optional Formal Arguments.

 Actual arguments can be passed during instantiation.

sequence s1 (data, en)

( !a && (data==2’b11)) ##1 (b==en)
endsequence

 Clock need not be specified in a sequence.

 In this case clock will be inferred from the property or assert

statement where this sequence is instantiated.

System Verilog Assertions

 Implication Operator

 Evaluation of a sequence can be pre-conditioned with an

implication operator.

 Antecedent – LHS of implication operator

 Consequent – RHS of implication operator

 Consequent will be evaluated only if Antecedent is true.

 There are two types of implication operators:

o Overlapping (Antecedent |-> Consequent )
o Non-Overlapping (Antecedent |=> Consequent )

System Verilog Assertions

 Overlapping Implication Operator

 If antecedent is true then Consequent evaluation starts

immediately.
 If antecedent is false then consequent is not evaluated and
sequence evaluation is considered as true this is called vacuous
pass.

 $assertvacuousoff [ (levels[ , list]) ] can be used to disable

vacuous pass.

property p1;
@ (posedge clk) en |-> (req ##2 ack);
endproperty

System Verilog Assertions

 Example

module test; program assert_test;

bit clk; initial begin
logic en=0, req=0, gnt=0; #4 en=1; req=1;
#10 en=0; req=0;
always #5 clk=~clk; #10 gnt=1;
property abc; #10 gnt=0;
@ (posedge clk) en |-> req ##2 gnt; #20 en=1;
endproperty #10 en=0; req=1;
assert property(abc) #10 req=0; gnt=1;
$info(“Sequence Occurred”); #10;
//program block end
endmodule endprogram

System Verilog Assertions

 Example

clk

en

req

gnt

Error Reported Sequence Occurred Vacuous Pass

Evaluation in progress
System Verilog Assertions
 Example

module test; program assert_test;

bit clk; initial begin
logic en=0, req=0, gnt=0; #4 en=1; req=1;
#10 en=0; req=0;
always #5 clk=~clk; #10 gnt=1;
property abc; #10 gnt=0;
@ (posedge clk) en ##0 req ##2 gnt; #20 en=1;
endproperty #10 en=0; req=1;
assert property(abc) #10 req=0; gnt=1;
$info(“Sequence Occurred”); #10;
//program block end
endmodule endprogram

System Verilog Assertions

 Example

clk

en

req

gnt

Error Reported Evaluation in progress Sequence Occurred

System Verilog Assertions
 Non-Overlapping Implication Operator

 If antecedent is true then Consequent evaluation starts in

next clock cycle.

 If antecedent is false then consequent is not evaluated and

sequence evaluation is considered as true this is called
vacuous pass.

property p1;
@ (posedge clk) en |=> (req ##2 ack);
endproperty

System Verilog Assertions

 Example

module test; program assert_test;

bit clk; initial begin
logic en=0, req=0, gnt=0; #4 en=1; req=1;
#10 en=0; req=0;
always #5 clk=~clk; #10 gnt=1;
property abc; #10 gnt=0;
@ (posedge clk) en |=> req ##1 gnt; #20 en=1;
endproperty #10 en=0; req=1;
assert property(abc) #10 req=0; gnt=1;
$info(“Sequence Occurred”); #10;
//program block end
endmodule endprogram

System Verilog Assertions

 Example

clk

en

req

gnt

Error Reported Evaluation in progress Sequence Occurred

System Verilog Assertions
 Example

module test; program assert_test;

bit clk; initial begin
logic en=0, req=0, gnt=0; #4 en=1; req=1;
#10 en=0; req=0;
always #5 clk=~clk; #10 gnt=1;
property abc; #10 gnt=0;
@ (posedge clk) en ##1 req ##1 gnt; #20 en=1;
endproperty #10 en=0; req=1;
assert property(abc) #10 req=0; gnt=1;
$info(“Sequence Occurred”); #10;
//program block end
endmodule endprogram

System Verilog Assertions

 Example

clk

en

req

gnt

Error Reported Evaluation in progress Sequence Occurred

System Verilog Assertions
 Sequence Operators

 ## n represents n clock cycle delay (or number of sampling

edges).

 ## 0 means same clock cycle (overlapping signals).

 ## [min: max] specifies a range of clock cycles

o min and max must be >=0.
sequence s1;
@ (posedge clk) a ## [1:3] b;
endsequence
Equivalent to: (a ##1 b) || (a ##2 b) || (a ##3 b)
System Verilog Assertions
 Example

clk

a
Assertion Passed
b
Assertion Passed
b
Assertion Passed
b
Assertion Failed
b

System Verilog Assertions

 Sequence Operators

 $ is used to specify infinite number of clock cycles (till end of

simulation).
sequence s2;
@ (posedge clk) a ## [2:$] b;
endsequence

b must be high after 2 or more clock cycle after a is asserted.

System Verilog Assertions

 Sequence Operators

 Sequence of events can be repeated for a count using [*n].

sequence s3;
@ (posedge clk) a ##1 b [*2];
endsequence

Equivalent to : a ##1 b ##1 b

b must be true for two consecutively clock cycles after a goes high
a (##1 b ##1 c) [*2];

Equivalent to : a ##1 b ##1 c ##1 b ##1 c

System Verilog Assertions
 Sequence Operators

 Sequence of events can be repeated for a range of count

using [*m : n].
o n should be more than 0 and cannot be $
sequence s4;
@ (posedge clk) a ##1 b [*2:5];
endsequence
Equivalent to : b must be true for minimum 2
(a ##1 b ##1 b ) || and maximum 5 consecutive
(a ##1 b ##1 b ##1 b) || clock cycles after a is asserted
(a ##1 b ##1 b ##1 b ##1 b) ||
(a ##1 b ##1 b ##1 b ##1 b ##1 b) ||
System Verilog Assertions
 Sequence Operators

 [=m] operator can be used if an event repetition of m non-

consecutive cycles are to be detected.
o m should be more than 0 and cannot be $

sequence s5;
@ (posedge clk) a ##1 b [=2];
endsequence

b must be true for 2 clock cycles, that may not be consecutive.

System Verilog Assertions

 Example

clk

b
Assertion Passed

b
Assertion Passed

System Verilog Assertions

 Sequence Operators

 [=m : n] operator is used if an event repetition of m (minimum)

to n (maximum) non-consecutive cycles are to be detected.

sequence s6;
@ (posedge clk) a ##1 b [=2: 3];
endsequence

b must be true for minimum of 2 and maximum of 3 clock cycles,

that may not be consecutive.

Equivalent to : (a ##1 b [=2] ) || (a ##1 b [=3] )

System Verilog Assertions

 AND Operator

 Use and operator if two sequences needs to match.

seq1 and seq2

 Following should be true for resultant sequence to matches:

o seq1 and seq2 should start from same point.
o Resultant sequence matches when both seq1 and seq2
matches.
o The end point of seq1 and seq2 can be different.
o The end time of resulting sequence will be end time of last
sequence.

System Verilog Assertions

 Example

(a ##2 b) and (c ##1 d ##2 e)

clk
a
b
seq1detected
Resultant Sequence Detected
c

d
e
seq detection started Seq2 detected
System Verilog Assertions
 Example

(a and b)

clk

Seq1 Detected Seq2 Detected Resultant Sequence Detected

System Verilog Assertions

 Example

(a ##[2:4] b) and (c ##1 d ##2 e)

clk
a
b

d
e

System Verilog Assertions

 Intersect Operator

seq1 intersect seq2

 Following should be true for resultant sequence to matches:

o seq1 and seq2 should start from same point.
o Resultant sequence matches when both seq1 and seq2
matches.
o The end point of seq1 and seq2 should be same.

System Verilog Assertions

 Example

(a ##[2:4] b) intersect (c ##1 d ##2 e)

clk
a
b
seq detection started
c

d
e
Seq1 Detected Seq2 Detected Resultant Sequence Detected
System Verilog Assertions
 OR Operator

 Use or operator when at least one of the sequences needs to

match.

seq1 or seq2

 Following should be true for resultant sequence to matches:

o seq1 and seq2 should start from same point.
o Resultant sequence matches when either seq1 or seq2
matches.
o The end point of seq1 and seq2 can be different.
o The end time of resulting sequence will be end time of last
sequence.
System Verilog Assertions
 Example

(a ##2 b) or (c ##1 d ##2 e)

clk
a
b
seq1detected
Resultant Sequence Detected
c

d
e
seq detection started Seq2 detected
System Verilog Assertions
 Example

(a or b)

clk

Seq1 Detected Seq2 Detected Resultant Sequence Detected

System Verilog Assertions

 Example

(a ##[2:4] b) or (c ##1 d ##2 e)

clk
a
b
seq detection started
c

d
e
Seq1 Detected Seq2 Detected Resultant Sequence Detected
System Verilog Assertions
 First_match Operator

 first_match operator matches only first of possible multiple

matches for evaluation of sequence.

a ##[2:5] b first_match(a ##[2:5] b)

Equivalent to: Sequence will match only one of the

(a ##2 b) || following options, whichever occurs first
(a ##2 b)
(a ##3 b) ||
(a ##3 b)
(a ##4 b) || (a ##4 b)
(a ##5 b) (a ##5 b)

System Verilog Assertions

 Example

first_match(a ##[2:4] b)

clk

seq detection started Resultant sequence detected

System Verilog Assertions

 throughout Operator

 Useful for testing a condition that an expression has to be true

throughout the sequence.

expr1 throughout seq1

 Left of throughout cannot be a sequence.

(!c) throughout a ##3 b

System Verilog Assertions

 Example

(!c) throughout a ##3 b

clk

Detection Started Assertion Passed Assertion Failed

System Verilog Assertions
 within Operator

 Useful for testing a condition where a sequence is overlapping

in part length of another sequence.

seq1 within seq2

 seq1 should happen between start and completion of seq2.

sequence seq1; sequence seq2;

@(posedge clk) a ##2 b; @(posedge clk) c ##1 !d ##2 e;
end sequence end sequence
property p1;
@(posedge clk) seq1 within seq2;
endproperty
System Verilog Assertions
 not Operator

 not operator is used to check that a particular sequence should

not occur.
sequence abc;
a ##1 b##1 c;
endsequence

property nomatch;
@(posedge clk) start -> not (abc);
endproperty

System Verilog Assertions

 not Operator

 Example c ##1 d should not occur after a ##1 b.

property incorrect;
@ (posedge clk) not (a ##1 b -> c ##1 d);
endproperty

 Will report even if a ##1 b does not occur because of

vacuous pass.

property correct;
@ (posedge clk) not(a ##1 b ##0 c ##1 d);
endproperty
System Verilog Assertions
 If-else Expression

 It is possible to select property expression based on some

condition using if-else expression.

property test;
@(posedge clk) (req1 || req2) ->
if(req1)
##1 ack1;
else
##1 ack2;
endproperty

System Verilog Assertions

 Local Variables

 Local variables can be declared and used inside property and

sequence.

 These are dynamically created inside sequence instance and

removed when end of sequence occurs.

 Each instance of sequence has its own set of variables.

 A local variable is assigned a value using a comma separated

list along with other expressions.

System Verilog Assertions

 Example

sequence s1;
int i;
(data_valid, (i = tag_in))
##7 (tag_out == i);
endsequence

Local variable i is assigned a value of tag_in when data_valid is

high. This value is then checked with the value of tag_out 7 clock
ticks later.

System Verilog Assertions

 Sample Value Functions

 Special System Functions are available for accessing sampling

values of an expression.
o Functions to access current sampled value.
o Functions to access sampled value in the past.
o Functions to detect changes in sample values.

 Can also be used in procedural code in addition to assertions.

System Verilog Assertions

 $rose, $fell

 $rose(expression [, clocking event)

o Returns true if least significant bit changes to 1 with respect
to value(0, X, Z) at previous clock else false.

 $fell(expression [, clocking event)

o Returns true if least significant bit changes to 0 with respect
to value(1, X, Z) at previous clock else false.

 Clocking event is optional usually derived from clocking event

of assertion block or procedural block.

System Verilog Assertions

 $rose vs @(posedge)

 @ (posedge signal) returns 1 when signal changes from (0, X,

Z) to 1 or (0 to X) or (0 to Z).

 $rose(signal) is evaluated to true when signal changes from

(0, X, Z) to 1 across two clocking event.

property p1; property p2;

@(posedge clk) a ##2 b; @(posedge clk) a ##2 $rose(b);
endproperty endproperty

System Verilog Assertions

 $rose

property p1; property p2;

@(posedge clk) a ##2 b; @(posedge clk) a ##2 $rose(b);
endproperty endproperty

p1 asserted p2 asserted

System Verilog Assertions

 $stable, $past

 $stable(expression [, clocking event)

o Returns true if value of expression did not change from its
sampled value in previous clock else false.

 $past(expression [, no of cycles] [, gating expression]

[,clocking event])
o Used to access sampled value of an expression any number
of clock cycles in past.
o no of cycles defaults to 1.
o gating expression for clocking event.
o clocking event inferred from assertion or procedural block
if not specified.

System Verilog Assertions

 System Functions and Tasks

 Following System Functions and Tasks are available that can

be used in assertions and procedural blocks:
o $onehot (expression) : Returns true if only one bit of the
expression is high.

o $onehot0 (expression) : Returns true if at most one bit of

the expression is high.

o $isunknown (expression) : Returns true if any bit of the

expression is X or Z.
o $countones (expression) : Returns number of one’s in the
expression.

System Verilog Assertions

 $asserton, $assertoff, $assertkill

 disable iff can be locally disable assertions.

 $asserton, $assertoff and $assertkill are used to control
assertions of a module or list of instance.
 $asserton, resume execution of assertions, enabled by
default.
 $assertoff, temporarily turns off execution of assertions.
 $assertkill, kills all currently executing assertions.

$asserton(level[, list of modules or instances)

System Verilog Assertions

 Properties

 A property defines behavior of a design

 A property can be used for verification as an
assumption, a checker, or a coverage specification.
 assert to specify the property as a checker to ensure
that the property holds for the design
 assume to specify the property as an assumption for
the environment
 cover to monitor the property evaluation for coverage

System Verilog Assertions

 Declaring Properties

 A property can be declared in a module,

interface, clocking block, package or any
compilation unit
 Properties can have formal arguments like
sequence declarations

System Verilog Assertions

 Types of Properties

 Seven Types of Properties

 1) sequence
 2) negation
 3) disjunction
 4) conjunction
 5) if..else
 6) implication
 7) instantiation
System Verilog Assertions
 Sequence

 A property that is a sequence evaluates to true if and

only if there is a non-empty match of the sequence
 As soon as a match of sequence_expr is determined, the
evaluation of the property is considered to be true

System Verilog Assertions

 Negation

 A property is a negation if it has the form

 not property_expr

 if property_expr evaluates to true, then not

property_expr evaluates to false, and
 If property_expr evaluates to false, then not
property_expr evaluates to true

System Verilog Assertions

 Disjunction (OR)

 A property is a disjunction if it has the form

 property_expr1 or property_expr2
 The property evaluates to true if and only if at
least one of property_expr1 and
property_expr2 evaluates to true.

System Verilog Assertions

 Conjunction (AND)

 A property is a conjunction if it has the form

 property_expr1 and property_expr2
 The property evaluates to true if and only if both
property_expr1 and property_expr2 evaluate to true.

System Verilog Assertions

 If...else
1) if (expression) property_expr1
 Evaluates to true if expression evaluates false
 Evaluates to true if expression evaluates true and
property_expr1 also evaluates true
 Others – evaluate to False
2) if (expression) property_expr1 else property_expr2
 Evaluates to true if expression evaluates true and
property_expr1 also evaluates true
 Evaluates to true if expression evaluates false and
property_expr2 evaluates true
 Others evaliate False

System Verilog Assertions

 Implication

 A property is an implication if it has either the form

 sequence_expr |-> property_expr (overlapping)
 or the form
 sequence_expr |=> property_expr (non-
overlapping)

System Verilog Assertions

 Instantiation

 An instance of a named property can be used

as another property_expr or property_spec.

System Verilog Assertions

 Recursive Properties

 A named property is recursive if its declaration involves

an instantiation of itself.
Specifies that signal “p” must hold
at every cycle . Note that “and”
will return true if both operands
return true

 This assert will make sure that after reset is de-

asserted the signal bootStrap holds to “1”. Any time it
goes low , the assertion fires

System Verilog Assertions

 Recursive Properties

 What if we change above non-overlapping operator

to overlapping operator?
 Gets stuck in an infinite loop recursion in same cycle
resulting in a run-time error
 So needs to be careful in using recursive properties

System Verilog Assertions

 Usage/Example

 Spec: interrupt must hold untill interrupt ack is

received
 Passing case Failing
Case

Note:
1) The “and” between intr and the recursive call will make sure that if intr
goes low before intrAck - the property/assertion fails
2) The “or” makes sure that property passes when intrAck goes high
System Verilog Assertions
 Restrictions on Recursive Properties

 Operator “not” cannot be used in recursive

property instances.

System Verilog Assertions

 Restrictions on Recursive
Properties

 The operator “disable iff” cannot be used in

the declaration of a recursive property

 Rewrite as follows as legal_3 is not recursive

System Verilog Assertions

 Restrictions on Recursive Properties

 If p is a recursive property, then, in the declaration of

p, every instance of p must occur after a positive
advance in time.

Note: The overlapping

operator will make this
recursion stuck in an infinite
loop

System Verilog Assertions

 Mutual recursion

 Recursive properties can be mutually recursive

 This is valid as there is time advancement (non-

overlapping implication) and there is an antecedent

System Verilog Assertions

 Labelling Assertions

 Always Label meaningfully

 Optional but highly useful for debug
 Label gets printed during failure and also shows up in
waveform
 Without label – assertions from a module that are instantiated
multiple times will be a nightmare to debug
 Multiple unnamed assertion failures are also hard

 E.g. An assertion for a D-Flip flop

ERROR_q_did_not_follow_d:
assert property (@(posedge clk) disable iff (!rst_n) (q==$past(d)));
System Verilog Assertions