System Verilog
assertions
Presenting by
Kanakala saikumar
Topics to be discussed
• Operators
• Binding properties
• Cyclic dependency
• Assertions examples
Operators used in
concurrent assertions
Implication operator
• How assertion will be if we don’t use an implication operator?
• Property pr1;
@ (posedge clk) req ##2 gnt;
Endproperty
Before implication
But why?
After implication operator using
Property pr1;
@(posedge clk) req |-> ##2 gnt;
Endproperty
But why?
Vacuous pass ( cover does not allow an action
block if property fails)
Clock delay operator ##m
• Sequence s1;
a ##2 b;
endsequence
Property ab;
@(posedge clk) z -> s1;
endproperty
• What happens with ##0 cycle delay will it have same effect?
• Sequence s1;
a ##0 b;
endsequence
Property ab;
@(posedge clk) z -> s1;
endproperty
##0 acts as Overlapping delay here
a ##1 b ##1 c // first sequence seq1
d ##1 e ##1 f // second sequence seq2
(a ##1 b ##1 c) ##0 (d ##1 e ##1 f) // overlapped concatenation
The delay ##1 indicates that the beginning of the sequence that follows is one clock tick later than
the current clock tick.
The delay ##0 indicates that the beginning of the sequence that follows is at the same clock tick as
the current clock tick
When used as a concatenation between two sequences :
The delay ##1 indicates that the beginning of the second sequence is one clock tick later than the end
of the first sequence.
The delay ##0 indicates that the beginning of the second sequence is at the same clock tick as the
end of the first sequence.
a ##1 b ##1 c&&d ##1 e ##1 f (this also concatenation)
Clock delay range ##[m:n]
As opposed to fixed number of clocks it is used to check the expression or
signal with in a range.
Sequence s1;
a ##[1:3] b;
endsequence
Property ab;
@(posedge clk) z -> s1;
endproperty
m can be 0 ( no delay) The property will match the very first
n can be 0 or $(maximum) time b is true.
##[0:0] same as ##0.
Clock delay range operator multiple threads
• Property rdyprotocol;
@(posedge clk) rdy |-> ##[1:5] rdyAck
endproperty
The range operator can cause multiple
Threads to complete at the same time.
$rose, local variables are used for
Efficient Simulation performance.
This is how multiple threads are look like
##[*] is used as an equivalent representation of##[0:$].
##[+] is used as an equivalent representation of ##[1:$].
Sequence s1;
a ## [0:$] b;
Endsequence
Property pr1;
@(posedge clk) z |-> s1;
Endproperty
$can be very useful when in a complex sequence you do
not really know when a certain signal/sequence will
follow another sequence but you do need to make sure it
does occur
[*m] consecutive repetition operator
• Sequence sc1;
a ##1 [b *2];
endsequence
Property ab;
@(posedge clk) z |=> sc1;
Endproperty
Wave form for consecutive repetition
Any observations we will update here:
Practical usage of consecutive repetition
• In AHB we having HREADYOUT signal to insert wait states
• When HREADY is low wait states are introduced
• After HREADY is low we should not change the HTRANS type until
HREADY is low or till HREADY high
Here we can check through consecutive repetition operator how this
functionality is happening.
Lets write the assertion for this condition in the next slide….
AHB EXAMPLE
Property Ahbcon (clk, sig, numclk);
@(posedge clk) $fell(HREADY) |-> $stable (sig[*numclk]);
endproperty
Ahb_con: assert property (Ahbcon (Hclk, HTRANS , 3))
$info(………………..);
else
$error(-----------------------);
Cov_prop: cover property (Ahbcon(Hclk, HTRANS , 3));
Exercise: property cons_on_antecedent;
@(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty
[*m : n] consecutive repetition
range
• First point to be observed in both [*m] and [*m : n] are
• If [*m] sequence ends on last match of m value.
• If[*m : n] sequence ends on first match of m value.( but why?)
Sequence sc1; this sequence a ##1 b[*2:5] is equivalent to
a ##1 b[*2:5]; a ##1 b ##1 b ||
endsequence a ##1 b ##1 b##1 b ||
Property ab; a ##1 b ##1 b##1 b##1 b ||
@(posedge clk) z |-> sc1; a ##1 b ##1 b##1 b##1 b##1 b
endproperty
Important note: the property first waits and look for the two
consecutive high on “b” if it finds the sequence the property ends and
pass the assertion.
Here comes the question why do we need max range? then
When this max range checks?
If there is any qualifying event then this max range check happens
Lets see how do this works….
Sequence sc1; this sequence a ##1 b[*2:5] is equivalent to
a ##1 b[*2:5] ##1 c; a ##1 b ##1 b ##1 c ||
endsequence a ##1 b ##1 b##1 b ##1 c||
Property ab; a ##1 b ##1 b##1 b##1 b ##1 c ||
@(posedge clk) z |-> sc1; a ##1 b ##1 b##1 b##1 b##1 b ##1 c
endproperty
Application for Consecutive repetition range
operator [*m:n]
• Specification: In AXI we have 5 independent channels here for the
write data channel we have WVALID,WREADY,WLAST.
Here 2 scenarios included : one for handshaking and other writing valid
data WDATA till WLAST asserted.
Try writing some assertions for above conditions
Request handshaking
Property reqhs;
@(posedge clk) $rose(AWVALID) |-> AWVALID [*1:2] ##0 AWREADY ;
endproperty
Assert property(reqhs) $display(-----------------) else $display(-----------------);
Property wdhs;
@(posedge clk) $rose(WVALID) |-> WVALID[*1:2] ##0 WREADY;
endproperty
Assert property(wdhs) $display(-----------------) else $display(-----------------);
Property wd;
@(posedge clk) $rose(WREADY) |-> WDATA[*1:$] ##0 WLAST;
endproperty
Assert property(wd) $display(-----------------) else $display(-----------------);
[=m] non-consecutive
repetition operator
• Read acknowledgements
Property p1;
@(posedge clk) req |=> gnt[=2];
endproperty
The above waveform is for below property please examine carefully
Property p1;
@(posedge clk) req |=> gnt[=2] ##1 c ;
endproperty
[=m:n] non-consecutive range
operator
Property p1;
@(posedge clk) req |=> gnt[=2:5] ##1 c ;
endproperty
Application for non-consecutive
repetition operator
• Specification : if nonburst (nburst) read of length 8 is asserted that the
RACK must be asserted 8 times and readdone(rddone) must be
asserted anytime after last read and there are nomore RACK between
lastread and readdone(rddone).
• Property Rdackcheck(int length);
@(posedge clk) nburst |=> RDACK[=length] ##1 rddone;
endproperty
A never fail case example(avoid
this)
• Property abc;
@(posedge clk) a|=> b[=0:$] ##1 c;
Endproperty
Assert property(abc) $display(-----------------) else
$display(-----------------------);
note: careful usage of minimum and maximum
Ranges.
[->m] Go To non – consecutive
repetition operator
• This exactly similar to [=m] operator
• Then what makes the difference between these two i.e qualifying event
Property abc;
@(posedge clk) req |=> gnt[=2];
endproperty
Property abc;
@(posedge clk) req |=> gnt[->2];
endproperty
Property abc;
@(posedge clk) req |=> gnt[=2] ##1 c;
endproperty
Property abc;
@(posedge clk) req |=> gnt[->2] ##1 c;
endproperty
Example code
• module con_rep;
• bit clk,req,gnt,c;
• property conrep;
• @(posedge clk) $rose(req) |=> gnt[->2] ##1 c;
• endproperty
• crep:assert property (conrep) else $display($time,,,"\t\t %m FAIL");
• c_req:cover property (conrep) $display($time,,,"\t\t %m PASS")
• initial begin
• clk=0;
• req=0;
• #5 req=1;
• #3 req=0;
• #15 gnt=1;
• req=1;
• #15 gnt=0;
• #20 gnt=1;
• #10 gnt=0;
• #4 c=1;
• end
• always #5 clk=~clk;
initial begin
• $monitor($time,"\t clk=%0d,req=%0d,gnt=%0d",clk,req,gnt);
• end
• initial begin
• #100;
• $finish;
• end
• endmodule
PART1
The End
