ASSERTIONS

IN
SYSTEM VERILOG
SUBSCRIBE TO “VLSI TO YOU”
Assertions

 Assertions are used to check design rules or specifications and generate

warnings or errors in case of assertion failures. An assertion also provides
function coverage that makes sure a certain design specification is
covered in the verification. The methodology that uses assertions is
commonly known as “Assertion Based Verification” (ABV). Assertions can be
written in the design as well as the verification environment.
 Types of Assertions
1. Immediate assertions
2. Concurrent assertions
Advantages of using Assertions

1. Checks design specifications and reports errors or warnings in case of

failure.
2. It improves debugging time. For example, a bug due to an illegal state
transition can propagate to the output. Writing an assertion helps out to
improve debugging time.
3. Can be re-used across verification testbench or design.
4. Can be parameterized
5. Can be turned on/off based on the requirement.
Advantages of System Verilog Assertion
(SVA)

▪ System Verilog merges benefits from different assertion languages into one,
thus giving the best from all languages.
▪ Due to native support of assertions in SV, assertions can be added to the
design and testbench directly without needing to add special interface.
▪ SVA is easy to learn and implement.
▪ Same assertions can be re-used in both functional and formal assertions.
▪ System Verilog supports two types of assertions: immediate
assertions and concurrent assertions.
IMMEDIATE ASSERTIONS
An assertion that checks a condition at the current simulation time is called
immediate assertions.

CONCURRENT ASSERTIONS.

An assertion that checks the sequence of events spread over multiple clock
cycles is called a concurrent assertion
Immediate Assertions
An assertion that checks a condition at the current simulation time is called
immediate assertions. They are executed like procedural statements like the if-
else statements.

Syntax: <label>: assert (expression) <pass_statement> else <fail_statement>

1. If an expression evaluates true then pass_statement is executed, else the

fail_statement is executed and said to be assertion failure.
2. Both pass_statement and fail_statement in the above syntax are optional.

Since the assertion is a statement that something must be true, the failure of an
assertion shall have a severity associated with it. By default, the severity of an
assertion failure is an error.
Assertion severity levels

• Other severity levels can be specified by including one of the following

severity system tasks in the fail statement:
• $fatal is a run-time fatal.
• $error is a run-time error.
• $warning is a run-time warning, which can be suppressed in a tool-
specific manner.
• $info indicates that the assertion failure carries no specific severity.
• If an assertion fails and no else clause is specified, the tool shall, by
default call $error.
module asertion_ex;

bit clk,a,b; Output:

//clock generation ncsim: *E,ASRTST (./testbench.sv,23): (time 15 NS) Assertion

asertion_ex.__assert_1 has failed
always #5 clk = ~clk; ncsim: *E,ASRTST (./testbench.sv,23): (time 25 NS) Assertion
//generating 'a' asertion_ex.__assert_1 has failed
ncsim: *E,ASRTST (./testbench.sv,23): (time 35 NS) Assertion
initial begin asertion_ex.__assert_1 has failed Simulation complete via
$finish(1) at time 55 NS + 0
a=1; b=1;

#15 b=0;

#10 b=1; a=0;

#20 a=1;

#10; $finish;

end

//Immediate assertion

always @(posedge clk) assert (a && b);

endmodule
Concurrent Assertion
 An assertion that checks the sequence of events spread over multiple
clock cycles is called a concurrent assertion. They execute in parallel with
other always blocks concurrently, hence it is known as a concurrent
assertion.
1. Unlike immediate assertion, the concurrent assertion is evaluated only at
clock tick. Thus, it is a clock-based evaluation model and an expression
used in the concurrent assertion is always tied to a clock definition.
2. The variables used in the assertions are sampled in the preponed region of
the simulation time slot but it is evaluated at the observe region and
execute pass/fail statements in the reactive region.
3. A concurrent assertion can be declared in an always or initial block and
that can be placed in an interface, program, or module block.
4. An assert keyword is used to check the property.
5. The Keyword differentiates the immediate assertion from the concurrent
assertion is “property.”

Syntax: <label>: assert property (<property_name(signals)>) <pass_statement>

else <fail_statement>;
 <label>: assert property (<property_name(signals)>) <pass_statement> else
<fail_statement>;

Example: assert property (@(posedge clk) (req1 || req2));

or
If it is a complex property then it can be defined separately and used as the
assert statement. Then
assert property (prop_req);
property prop_req; Property usage
@(posedge clk) disable iff (!reset_n)
1.The property captures design
req1 |=> req2 ##2 req3; specifications and checks for design
behavior.
endproperty
2.It is also used for coverage to measure
that property is covered.
 The steps involved in the creation of an SVA checker,

The functionality is represented by the combination of multiple logical

events. These events could be simple Boolean expressions.

Boolean expression events that evaluate over a period of time involving

single/multiple clock cycles. SVA provides a keyword to represent these
events called “sequence.” Syntax: sequence name_of_sequence;
……
endsequence
Number of sequences can be combined logically or sequentially to
create more complex sequences. SVA provides a keyword to
represent these complex sequential behaviors called “property”.
Syntax: property name_of_property;
test expression or complex sequence expressions
endproperty

The property is the one that is verified during a simulation. It has to be asserted
to take effect during a simulation. SVA provides a keyword called “assert” to
check the property.

Syntax: assertion_ name: assert_property( property_name );

 SVA Sequence(assertion Sequence)
sequence seq_1; In this example the sequence seq_1 checks that the signal “a” is high on
@(posedge clk) a==1; every positive edge of the clock. If the signal “a” is not high on any
positive clock edge, the assertion will fail.
endsequence

A sequence with a logical relationship

sequence seq_2; In this sequence, seq_2 checks that on every positive edge of the
@(posedge clk) a || b; clock, either signal “a” or signal “b” is high. If both the signals are low,
endsequence the assertion will fail.

Sequences with timing relationship

In SVA, clock cycle delays are represented by a “##” sign. For
sequence seq; example, ##2 means 2 clock cycles.
@(posedge clk) a ##2 b;
In this the sequence checks for the signal “a” being high on a given
endsequence
positive edge of the clock. If the signal “a” is not high, then the
sequence fails. If signal “a” is high on any given positive edge of the
clock, the signal “b” should be high 2 clock cycles after that. If signal
“b” is not asserted after 2 clock cycles, the assertion fails.
Clock delays

1. ## : represents cycle delay

2. ##n – represents “n” clock cycles

3. ##0 – represents same clock cycle

4. ## [min:max] represents a range of clock cycles. Where min and max must
be 0 or greater than 0.

##0 -> means that there should be no delay and expression on LHS and RHS
should hold true at same time.
##1 -> means that the expression present on RHS should be true after one
clock cycle of LHS.
##[2:4] valid -> assert statement will fail if valid is not set to 1 within 2 to 4
clock cycles after input_data becomes 1.
 Repetition operators

sequence seq; if the signal “a” is high on given posedge of the

@(posedge clk) req1 ##1 req2[*3]; clock, the signal “b” should be high for 3 consecutive
endsequence clock cycles.

req1 ##1 req2[*3] is same as req1 ##1 req2 ##1 req2

##1 req2.

sequence seq;
@(posedge clk) req1 ##1 req2[*2:4]; In this example, if req1 is true then after 1 clock cycle,
endsequence req2 must be true for a minimum of 2 and a maximum
of 4 consecutive clock cycles.

sequence seq; In this example, once req1 holds true after one clock
@(posedge clk) req1 ##1 req2[=4]; cycle req2 must be true for 4 clock cycles but it is not
endsequence mandatory to be consecutive clock cycles.
sequence seq;
@(posedge clk) req1 ##1 req2[=2:4];
endsequence

once req1 holds true after one clock cycle, req2 must
be true for a minimum of 2 and a maximum of 4 clock
cycles but it is not mandatory to be consecutive
clock cycles.
 Clock defined in the sequence definition

sequence seq;
a ##2 b;
endsequence
sequence seq;
property p; @(posedge clk) a ##2 b;
@(posedge clk) seq; endsequence

endproperty
a_1 : assert property(p);

Clock defined in the property definition

 Implication Operator
sequence seq; In this particular sequence If we want the sequence
@(posedge clk) a ##2 b; to be checked only after “a” is high, this can be
endsequence achieved by using the implication operator.

 There are 2 types of implication:

• Overlapped implication
• Non-overlapped implication
 The implication is similar to an if-then structure. The left-hand side of the
implication is called the “antecedent” and the right-hand side is called the
“consequent.” The antecedent is the gating condition. If the antecedent
succeeds, then the consequent is evaluated.
 The implication construct can be used only with property definitions. It
cannot be used in sequences.
 Overlapped implication

• The overlapped implication is denoted by the symbol |->.

property p; • If there is a match on the antecedent, then the
@(posedge clk) a |-> b; consequent expression is evaluated in the same clock
endproperty cycle.
a: assert property(p); • Below property checks that, if signal “a” is high on a given
positive clock edge, then signal “b” should also be high on
the same clock edge.

Non-overlapped implication

• The non-overlapped implication is denoted by the symbol

property p; |=>.
@(posedge clk) a |=> b; • If there is a match on the antecedent, then the
endproperty consequent expression is evaluated in the next clock cycle.
a: assert property(p); • Below property checks that, if signal “a” is high on a given
positive clock edge, then signal “b” should be high on the
next clock edge.
The implication with a fixed delay on the consequent
Below property checks that, if signal “a” is high on a given positive clock edge,
then signal “b” should be high after 2 clock cycles.

property p; @(posedge clk)

sequence seq;
a |-> ##2 b; @(posedge clk) a ##2
endproperty b; endsequence
a: assert property(p);
The implication with a sequence as an antecedent
 Below property checks that, if the sequence seq_1 is true on a given
positive edge of the clock, then start checking the seq_2 (“d” should be
low, 2 clock cycles after seq_1 is true).

sequence seq_1;
(a && b) ##1 c;
endsequence

sequence seq_2;
##2 !d;
endsequence

property p;
@(posedge clk) seq_1 |-> seq_2;
endproperty
a: assert property(p);
 Timing windows in SVA Checkers
property p;
@(posedge clk) a |-> ##[1:4] b;
endproperty if signal “a” is high on a given positive clock edge, then within
a: assert property(p); 1 to 4 clock cycles, the signal “b” should be high.

property p;
Overlapping timing window @(posedge clk) a |-> ##[0:4] b;
if signal “a” is high on a given positive clock edge, then endproperty
signal “b” should be high in the same clock cycle or a: assert property(p);
within 4 clock cycles.

property p; Indefinite timing window

@(posedge clk) a |-> ##[1:$] b; if signal “a” is high on a given positive clock
endproperty edge, then signal “b” will be high eventually
a: assert property(p); starting from the next clock cycle.
 Repetition operators

property p; if the signal “a” is high on given posedge of the

@(posedge clk) a |-> ##1 b ##1 b ##1 b; clock, the signal “b” should be high for 3 consecutive
endproperty clock cycles.
a: assert property(p);
@(posedge clk) a |-> ##1 b[*3]; //can also be
written in this way

The go-to repetition operator property p;

if the signal “a” is high on given posedge of the clock, the @(posedge clk) a |-> ##1 b[->3] ##1 c;
signal “b” should be high for 3 clock cycles followed by “c” endproperty
should be high after ”b” is high for the third time. a: assert property(p);
 Forbidding a property
 A separate property definition is not needed to assert a sequence. the
expression to be checked can be called from the assert statement directly
as shown below.

sequence seq;
@(posedge clk) a ##2 b;
endsequence The sequence checks that if signal “a” is high on a
given positive edge of the clock, then after 2 clock
property p; cycles, signal “b” shall not be high. The keyword “not” is
not seq; used to specify that the property should never be true.

endproperty
a_1: assert property(p);