SystemVerilog Assertions (SVA) is a language for precisely specifying the DUT behavior ( functionality or property ) but do not constitute a golden model.
SVA is describing DUT functionality ( property ) that is to be there and it is given directive to verification to
- verify ( assert ( property ) verification directive )
- assume ( assume ( property ) verification directive )
- measure coverage ( cover ( property ) verification directive )
the functionality described.
Assertion checking is a simple addition to a simulation-based verification methodology, adding additional monitors of DUT functionality.
e.g. You can use assertions to monitor the interface of a module: assertions will quickly identify when the protocols or sequences of the interface signals are incorrect.
The DUT functionality represented by an assertion can be
- combinational (boolean) or
- temporal (extended over time).
- Default $error severity task
By default, when an assertion fails, the simulator calls the $error severity task, which displays an error message. No action is taken by default when an assertion passes.
All possibilities of a SVA failure severity tasks are:
— $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.
SVA described here are represented in a testbench as a custom property.
There are two kinds of assertions: concurrent and immediate:
- Immediate assertions tests an expression when the statement is executed in the procedural code.
- Concurrent assertions are based on clock and can describe Boolean behaviors or patterns of behavior that span over time.
From design specification to SVA based verification
e.g. A simple synchronous request - acknowledge protocol design (DUT)
Excerpt from the DUT specification
Output signal ack has value 0 while POR ( input signal reset_n=0). Input signal req can be raised at any time and must stay asserted until output signal ack is asserted Once both req and ack are asserted in the next clock cycle both req and ack must be de-asserted.
How SVA is extracted from the specification:
- DUT has three inputs ( clock, reset_n and req) and one output (ack)
- reset_n is asynchronous, active low signal
- Test vector generation assumptions ( SVA Implementation HINT, use :assume ) about input signal req that must be respected during verification ( in relation to DUT output signal ack)
- one cycle after ack, req must be de-asserted
property pr2;
@(posedge clk) ack |=> !req;
endproperty
assume_ack2:assume property (pr2);
- hold req asserted until and one clock cycle after ack is asserted
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty
assume_ack3:assume property (pr3);
- Verify following DUT functionality (SVA Implementation HINT, use :assert )of DUT the output signal ack
- while reset_n=0 or req=0, ack must be held: 0
property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
assert_req1:assert property (pa1)
else $display("\n ack asserted while req is still de-asserted");
- once reset_n=1 and req=1, ack must become and stay 1, during one clock cycle and after the clock cycle go back to 0 again.
property pa2;
@(posedge clk) ack |=> !ack;
endproperty
assert_req2:assert property (pa2)
else $display("\n ack is extended over more than one cycle");
SVA vs. Verilog HDL
e.g. A detail of DUT functionality to verify:
signal if request ( req ) change from 0 to 1, within next 3 rising edge clocks ( clk ), signal acknowledge ( ack ) should change from 0 to 1 too.
Verilog HDL
begin
repeat (1) @(posedge clk);
fork: pos_pos
begin
@(posedge ack)
$display("Assertion Success",$time);
disable pos_pos;
end
begin
repeat (2) @(posedge clk);
$display("Assertion Failure",$time);
disable pos_pos;
end
join
end // always
- SVA equivalent to previous HDL
assert property (
@(posedge clk) $rose(req)|-> ##[1:3] $rose(ack)
)
else $display(“Assertion Failure",$time) ;
SVA Immediate Assertions
assert(expression) action_block
An immediate assertion tests an expression when the statement is executed in the procedural code. If the expression is interpreted as true, the assertion passes. If the expression is interpreted as false, the assertion fails.
The expression is non-temporal and is interpreted the same way as an expression in the condition
of a procedural if statement. Also the expression is not defined under a sequence or propery.
SVA Immediate Assertions are good for combinational checks
e.g. On positive edge clk, every time state is in REQ , check there is either req1or req2. If this in not truth assertion fail, otherwise pass.
time t;
always @(posedge clk)
if (state == REQ)
assert (req1 || req2)
else begin
t = $time;
#5 $error("assert failed at time %0t",t);
end
Since the fail statement, like the pass statement, is any legal SystemVerilog procedural statement, it can also be used to signal a failure to another part of the testbench.
e.g > assert (myfunc(a,b)) count1 = count + 1; else ->event1;
e.g > assert (y == 0) else flag = 1;
e.g >
always @(read_n || address) begin
case (bank)
"RAM_BANK_0" : mem_delay = 5;
"ROM_BANK_0" : mem_delay = 10;
"RAM_BANK_1" : mem_delay = 15;
default :
begin
// Here, an assertion is used inside a case statement.
// It checks that the correct names of memory bank variables are used.
//
assert(0); else $error("Unexpected bank setting. %s\n",bank);
mem_delay = 0; /* Default */
end
endcase
end
SVA Concurrent Assertions
Unlike immediate assertions, the evaluation model is based on a clock such that a concurrent assertion is evaluated only at the occurrence of a clock tick.
The clock expression that controls evaluation of a sequence can be more complex than just a single signal name.
e.g; Expressions such as (clk && gating_signal) and (clk iff gating_signal) can be used to represent a gated clock
The simplest form of concurrent assertion checks a combinational logic at every clock event.
e.g. at every rising edge of the clk both of request signals can not be high at the same time
assert property (
( @ posedge clk )
! ( request1 && request2 )
) else $error( “ ERROR: Both requests active at the same time”)
SVA Language Layers
Boolean expressions
• Evaluated at a single clocking event (combinational).- Verilog operators supported with Verilog semantics
Sequences
DUT functionality ( or property ) can be described in sequences or may involve checking of one or more sequences beginning at various times.e.g. > Sequence : a ##1 b ##c, describes this DUT functionality:
- after signal a transitions from 0 to 1, signal b MUST transition 0 to 1 on next clock cycle and finally after b becomes 1 signal c MUST transition to 0 t 1 in the next clock cycle .
e.g. > Sequence : b ##[1:4] c, describes this DUT functionality:
- after signal b transitions from 0 to 1, after 1 or 2 or 3 or 4 clock cycles signal c MUST transition 0 to 1 as well.
##n
Specifies the number of clock cycles that occur between sequence expressions. The number of clock cycles can be 0, to specify no delay.Leading Delay
“##n S” specifies a delay of n clock events until the beginning of the match of S
- n must be a non-negative integer, compile-time
constant
- “##0 S” is equivalent to “S”
- “##n S” is equivalent to “1’b1 ##n S”, n > 0
- ##1 a // means 1’b1 ##1 a
- ##2 a // means 1’b1 ##1 1’b1 ##1 a
e.g > a ##2 b // means a ##1 1’b1 ##1 b
e.g. > The following example defines a property, P1, which checks that if a is true, and b is true two clock cycles later, then c must be true one clock cycle after that. The concurrent assertion, A1, causes this property to be checked during simulation or formal analysis.
property P1;
@(negedge clk) (a ##2 b) |=> (c);
endproperty
A1: assert property (P1);
e.g> This example defines a sequence, S1, that takes two arguments. S1 specifies that after the first argument occurs, the second argument must occur from zero to two clock cycles later. The sequence S2 instantiates S1 and passes the arguments b and a to S1.
sequence S1(AA, BB);
(AA ##[0:2] BB);
endsequence
sequence S2;
S1(b,a);
endsequence
##[start:end]
Specifies a range of clock cycles. Specifies a delay range of at leaststart and at most end clock events
e.g. “req” that changes 0 to 1 on positive edge of the clock, will be followed with “ack” change from 0 to 1, 1 to 3 positive edge clock later
sequence x ;
req ##[1:3] ack ;
endsequence
req ##[1:3] ack is same as:
req |-> ##[1] ack or
req |-> ##[2] ack or
req |-> ##[3] ack
e.g. ##[0:3]a // means (a) or (1’b1 ##1 a) or (1’b1 ##1 1’b1 ##1 a) or
(1’b1 ##1 1’b1 ##1 1’b1 ##1 a)
- Sequences can be composed of other sequences.
e.g>
sequence s;
a ##1 b ##1 c;
endsequence
sequence rule;
@(posedge sysclk)
trans ##1 start_trans ##1 s ##1 end_trans;
endsequence
Sequence rule in the preceding example is equivalent to:
sequence rule;
@(posedge sysclk)
trans ##1 start_trans ##1 a ##1 b ##1 c ##1 end_trans ;
endsequence
- Although sequences can be composed of other sequences, cyclic dependency of sequences is not allowed
e.g. Example of illegal cyclical dependency of two sequences: sequence s1 depends on sequence s2 and further s2 depend on s1
sequence s1;
@(posedge sysclk) (x ##1 s2);
endsequence
sequence s2;
@(posedge sysclk) (y ##1 s1);
endsequence
Concatenation sequences
Sequences can be composed by concatenation.The concatenation specifies a delay, using ##, from the end of the first sequence until the beginning of the second sequence.
Overlapped concatination
If in a sequence composed by concatination, specifified delay between two sequencies with overlapped concatination ##0, this means that second sequnce can start eventhough the first one did not finished yet.e.g. (a ##1 b ##1 c) ##0 (d ##1 e ##1 f) // overlapped concatenation
Is equal to
a ##1 b ##1 c&&d ##1 e ##1 f
Consecutive Repetition
<boolean expression> [*count]
b[*n] matches over n consecutive clock events, b Boolean expression
b[*0] matches over . . . zero clock events!
e.g > a[*1:3] is equivalent to
a or (a ##1 a) or (a ##1 a ##1 a)
e.g. when ready transitioned from 0 to 1,it stays 1 during 3 consecutive clock cycles
sequence ready_3 ;
ready ##1 ready ##1 ready :
endsequence
OR
sequence ready_3 ;
ready[ * 3] :
endsequence
e.g> “ack cannot be active for k consecutive cycles,” where k is a parameter
assert property ( not ack[*k ] ) ;
e.g. >
( clk ##1 !clk )[*3]
is equivalent to
( ( clk ##1 !clk ) ##1 ( clk ##1 !clk ) ##1 ( clk ##1 !clk ) )
which is equivalent to
( clk ##1 !clk ##1 clk ##1 !clk ##1 clk ##1 !clk )
You can also use [*] for [0:$], and [+] for [1:$].
delay and repetition in the same sequence
e.g> 1’b1 ##3 (a [*3]) // means 1’b1 ##1 1’b1 ##1 1’b1 ##1 a ##1 a ##1 ae.g> (1’b1 ##2 a) [*3] // means (1’b1 ##2 a) ##1 (1’b1 ##2 a) ##1
// (1’b1 ##2 a), which in turn means 1’b1 ##1 1’b1 ##1
// a ##1 1’b1 ##1 1’b1 ##1 a ##1 1’b1 ##1 1’b1 ##1 a
e.g> (a ##2 b) [*5]
This is the same as:
(a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)
consecutive repetition operator [*min:max]
A repetition with a range of min minimum and max maximum number of iterationse.g> (a ##2 b)[*1:5]
is equivalent to
(a ##2 b)
or (a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)
e.g>
(a[*0:3] ##1 b ##1 c)
is equivalent to
(b ##1 c)
or (a ##1 b ##1 c)
or (a ##1 a ##1 b ##1 c)
or (a ##1 a ##1 a ##1 b ##1 c)
e.g>
Once risen, xfer must remain high up to and including the
cycle of the next activation of done
|-> (Overlapped implication) and ##0 are used to allow done to rise concurrently with xfer
e.g>
• The following are equivalent:
§ S |-> (T |-> U)
§ (S ##0 T) |-> U
assert property (
$rose(xfer) |-> xfer [*1:$] ##0 done
);
Non-consecutive repetition ( [= )
This operator applies to a Boolean. The resulting sequence matches any trace in whichthe operand occurs for a specified number or range of cycles, which might or might not
be consecutive.
e.g. > a[=3] matches the traces (a, a, a), (a, b, b, a, b, a), and (b, a, b, b, a, b, a, b, b, b)
Go to repetition operator[-> …
This operator applies to a Boolean. The resulting sequence matches any trace in whichthe operand occurs for a specified number or range of cycles, which might or might not be consecutive, provided that the last occurrence is in the last cycle in the tracee.g. > a[->3] matches the traces (a, a, a), (a, b, b, a, b, a), and (b, a, b, b, a, b, a)
e.g If there is a valid start signal ( on posetive edge of the clock) , 2 clocks latter, signal “a” will repeat 3 times ( continuously or intermittently ) before there is a valid “stop” signal
assert property ( clk)
@(posedge clk) $rose(start) |->
##2 (a[->3] ) ##1 stop ;
endproperty
);.
• “!b[*0:$] ##1 b” matches at the nearest concurrent or future occurrence of boolean b
- SVA provides goto operator “b[->1]” for this idiom
• “(!b[*0:$] ##1 b)[*n]” is a common idiom for the nth occurrence of b
- SVA provides goto operator “b[->n]” for this idiom
Goto Operator
b[ -> n ] : Go to n-th occurance of
Unbounded consecutive repetition
e.g. if “req” rises, then as long as “wait” is held high
consecutively, “ack” must not be asserted
property wait_no_ack;
($rose(req) ##0 wait[*1:$]|-> !ack) ;
endproperty: e.g> req is high up to, but not necessarily including, the next cycle
that ack is high
sequence req_until_ack_2;
req [*0:$] ##1 ack;
endsequenceSame As:
sequence req_until_ack_2;
ack or
req[*1] ##1 ack or
req[*2] ##1 ack or
...endsequence
- Using very large repeat values, such as ack[*20000000], uses a large amount of memory, but unbounded repeat values, such as ack[*], do not.
SVA Sequence Operators
SVA Operator: and
The requirement for the match of the and operation is that both the sequences must match.
Specifies that two sequence expressions must begin in the same clock cycle, but they do not need to end during the same cycle.
When one of the operand sequences matches, it waits for the other to match. The end time of the composite sequence is the end time of the operand sequence that completes last.
e.g> (a ##2 b) and (c ##2 d ##2 e)
Properties
Properties are built up out of sequence.
The result of property evaluation is either true or false.
There are seven kinds of property:
1) sequence,
2) negation
e.g> For each evaluation attempt of the property, there is an evaluation attempt of
not property_expr
3) Disjunction
property_expr1 or property_expr2
4) Conjunction
property_expr1 and property_expr2
5) , if...else
if (expression_or_dist) property_expr1 else property_expr2
6) implication,
sequence_expr |-> property_expr ( overlapped implication )
or the form
sequence_expr |=> property_expr ( non-overlapped implication )
7) and instantiation
If the statement appears in an always block, the property is always monitored. If the statement appears in an initial block, then the monitoring is performed only on the first clock tick.
e.g>
property rule;
a ##1 b ##1 c;
endproperty
always @(posedge clk) begin
<statements>
assert property (rule);
end
In general it is a good idea to define the clocks in property definitions and keep the sequences independent of the clocks, to reuse sequences.
e.g; clocking example in relation to sequences and properties
sequence x ;
a ##2 b ;
endsequence
property y ;
@(posedge clk ) x ;
endproperty
assert property (y) ;
“disable iff (exp)”
- specifies that property evaluation should abort and return true any time
“exp” evaluates to true. When “exp” is a signal, it is checked asynchronously.
- “disable iff (exp)” can be placed only at the top level of an assert/cover property statement.
- Nested disable iff directives are not allowed.
e.g > aborting checks on reset
|=> (Non-overlapped implication)
sequence_expr |=> property_expris equivalent to:
sequence_expr ##1 1’b1 |-> property_expr
e.g>
• The following are equivalent:
§ S |=> (T |=> U)
§ (S ##1 T) |=> U
Don’t confuse “a ##1 b” ( continuously checked ) with “a |=> b” ( only checked when a is true, with the exception when used in initial block .
“|=>” is essentially the same as “|-> ##1”. The latter can be
generalized to “|-> ##n”
e.g. if “ack” change from 0 to 1 it will stay 1 only one clock cycle.In other words “ack ”can not be active two consecutive cycles.
assert property ( ack |=> !ack ) ; // if ack next clock cycle !ack
OR
assert property ( ack |-> ##1 !ack ) ; // if ack next clock cycle !ack
OR
assert property ( not ( ack ##1 ack ) ;
OR
assert property ( not ( ack [*2] ) ;
SVA Untyped ( arguments declared without a data type ) Formal Arguments
Not recommendede. g. > sequence S2 (CC, DD);
(a ##1 CC) or (b ##1 DD);
endsequence
S1_assertion: assert property
(@(negedge clk) (S1(b,c)) |=> S2((e||f), g));
SVA Typed ( arguments declared with a data type ) Formal Arguments
Recommeded
e.g > sequence S1 (bit AA, bit BB);
(a ##1 AA ##1 BB);
endsequence
e.g. > In the following example, Property P5 shows one argument, AA, that is untyped, and one argument that is of type bit, b.
property P5 (AA, bit BB);
@(negedge clk)
(BB ##1 c) |=> (AA ##[1:2] (d||AA));
endproperty
e.g. > You can pass a signal that is used as an event argument (clk), but not the event (@clk). For example, you can use
property exampl1(clk,x,y);
@(clk) x |=> y;
endproperty
but you cannot use
property exampl1(@clk,x,y);
@(clk) x |=> y;
endproperty
- When you instantiate a sequence or property, the argument list can be either:
1) name-associated or
2) positional.
e.g.> named_association: assert property P5 (.AA(my_AA), .BB(my_BB));
e.g.> sequence BusReq (min=0, max=0);
REQ ##[min:max] ACK;
endsequence
Default clocking: (Recommended)
A default clocking block:
- specifies the clock or event that controls the evaluation of sequences or properties within the block. Or
- attaches a clocking event to every assume/assert/cover property statement in the module that does not have its clock specified otherwise.
assertions in clocking blocks are not permitted by the IEEE 1800 standard
e.g. > default clocking master_clk @(posedge clk);
property p4; (a |=> ##2 b); endproperty
endclocking : master_clk
assert property (p4);
e.g. > default clocking master_clk @(posedge clk);
endclocking
sequence x ;
req ##1 ack ;
endsequence
assert property (x) ;
assert property ( req ##1 ack && req ##1 ack );
e.g>
clocking pos_clk @(posedge clk);
...
endclocking : pos_clk
default clocking pos_clk;
As an alternative to specifying a default clock, you can place assertions in an always or initial block
An inferred clock takes precedence over a default clock.
e.g> // @(posedge clk) applies to all assertions in the block.
always @(posedge clk) begin
A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
A2i: assert property ( (a[*3]) |=> ~c );
A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end
An initial block might or might not have an inferred clock. It is executed once.
// @(posedge clk) applies to all assertions in the block.
initial @(posedge clk) begin
A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
A2i: assert property ( (a[*3]) |=> ~c );
A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end
A local clock targeted at limited number of properties
e.g>clocking boo @( posedge clk)
property bleh ;
req |=> ack ;
endproperty
endclocking
a_bieh: assert property (boo.bleh) ;
Clocking options
The clock for a property can be specified in several ways
- Clock inferred from always block
Eg> always @(posedge clk) begin
A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
A2i: assert property ( (a[*3]) |=> ~c );
A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end
eg> always @(posedge clk)
begin
a1: assert property($past(ack) |-> !ack);
c1: cover property(req ##1 ack);
end- Explicit clock in assert/cover property statement:
eg>
a1: assert property(
@(posedge clk) $past(ack) |-> !ack
);
e.g>
a1: assert property(
@(posedge clk) $past(ack) |-> !ack
);c1: cover property(
@(posedge clk) req ##1 ack
);e.g>
sequence s;
@(posedge clk) a ##1 b;
endsequence
property p;
a |-> s;
endproperty
assert property (p);
:
o Explicitly specified in the property:
property p;
@(posedge clk) a ##1 b;
endproperty
assert property (p);
o Explicitly specified in the concurrent assertion:
assert property (@(posedge clk) a ##1 b);
o Inferred from a procedural block:
property p;
a ##1 b;
endproperty
always @(posedge clk) assert property (p);
SVA Multiple Clocks
Multiply-clocked sequences are built by concatenating singly-clocked subsequences using the single-delayconcatenation operator ##1
e.g. > assert property (@(posedge clk1) (a ##1 b) |=> @(posedge clk2) (c ##1 d));
Multiple-clock sequences must be built by concatenating single-clocked sub-sequences using the single-delay concatenation operator, ##1, or the |=> implication operator.
The delay is understood to be from the endpoint of the first sequence that occurs at the tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins.
For a multi-clocked assertion, the clocks are explicitly specified. No default clock or inferred clock is used. Inaddition, multi-clocked properties are not allowed to be defined within a clocking block.
A multi-clocked property assert statement must not be embedded in procedural code where a clock is inferred.
For example, following forms are not allowed.
always @(clk) assert property (mult_clock_prop);// illegal
initial @(clk) assert property (mult_clock_prop);// illegal
multiply-clocked properties
The boolean property operators (not, and, or) can be used freely to combine singly- and multiply-clocked
Properties
e.g> (@(posedge clk0) sig0) and (@(posedge clk1) sig1)
is a multiply-clocked property, but it is not a multiply-clocked sequence.
This property evaluates to true at a point if and only if the two sequences
@(posedge clk0) sig0
and
@(posedge clk1) sig1
both have matches beginning at the point.
e.g> property using clock flow and if...else
property mult_p8;
@(posedge clk) a ##1 b |->
if (c)
(1 |=> @(posedge clk1) d)
else
e ##1 @(posedge clk2) f ;
endproperty
Here, a, b, c, and e are clocked at posedge clk.
e.g>
sequence s;
//sequence composed of two named subsequences
@(posedge s_clk) e ##1 s1 ##1 s2 ##1 f;
endsequence
sequence s1;
@(posedge clk1) a ##1 b; // single clock sequence
Endsequence
sequence s2;
@(posedge clk2) c ##1 d; // single clock sequence
endsequence
SVA Local Variable Usage
The local variables declared in one sequence are not visible in the sequence where it gets instantiated
As shown in the following example, when valid_in is true, the x variable is assigned the value of data_in. If data_out is equal to x + 1 five cycles later, the property is true. Otherwise, the property is false. When valid_in is false, this property evaluates vacuously (idle, empty: devoid of serious occupation) to true.
e.g. > property pipeline;
int x;
@(posedge clk) disable iff (reset)
(valid_in, x = data_in) |=> ##5 (data_out == (x+1));
endproperty
The following example shows the use of a packed struct as a local variable:
e.g. > // Pipeline data check
typedef struct packed signed {reg[7:0] x, y;} data_struct;
property ex1;
data_struct ldata;
@(posedge clk)
(valid_in, ldata.x=data_in) |-> ##5 (data_out == ldata.x)
endproperty
e.g.
- When “req” change from 0 to 1, max_delay[3:0] is valid.
- max_delay[3:0] is assumed to be nonzero when it is valid.
- if “req” rises and remain high, then “ack” must be asserted no later then max_delay-th cycle after the “req”
property variable_ack_response_time;
reg[3:0] l_md ;
( $rose(req), l_md = max_delay )
|=> ( req && !ack, l_md = l_md -1)[*1:$]
|-> ( l_md > 0 ) ;
endproperty
Coverage
· Functional coverage
offers an insight on how the verification goals set by a test plan are being met, and can be performed on user-defined coverage points, specified using SystemVerilog assertions, or covergroup statementsFunctional coverage can be:
- Control-Oriented Using SVA Statements
- Data-Oriented Using SystemVerilog Covergroup
coverage metrics:
1) Line coverage
Counts executions of each line in the specification file.
2) cover property statement coverage
“cover property (p)” should be used only when “p” is a sequential property
3) covergroup coverage
Tracks a user-specified set of variable values and reports combinations of values that are not covered.
