SVA Non-consecutive Repetition @(posedge clk) a |=> b[=2] ##1 c at which cases assertion will pass

SystemVerilog
, ,
1

Hi All,

I have a doubt in below assertion execution

property p_1
@(posedge clk) a |=> b[=2] ##1 c ;
endproperty : p_1

So If suppose my sampled values are like this assertion will pass

run -all
#0 clk=1, a=0, b=0, c=0
#5 clk=1, a=1, b=0, c=0 // a got asserted (antecedent got triggered)
#10 clk=1, a=0, b=0, c=0
#15 clk=1, a=0, b=1, c=0 // 1st b=1
#20 clk=1, a=0, b=0, c=0
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=0
#35 clk=1, a=0, b=0, c=1 // Property Passed

and If my sampled values are like below will my assertion pass ?

run -all
#0 clk=1, a=0, b=0, c=0
#5 clk=1, a=1, b=0, c=0 // a got asserted (antecedent got triggered)
#10 clk=1, a=0, b=0, c=0
#15 clk=1, a=0, b=1, c=0 // 1st b=1
#20 clk=1, a=0, b=0, c=0
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=0
#35 clk=1, a=0, b=1, c=1 // Property Passed or Fail ?

So at #35 time unit b and c are 1 and also b is 1 for 3 times
but as per our property b=1 appeared 2 times and after 1 clock cycle delay c=1 is happening. So , here will our simulation consider b also ?

Thanks You

2

In reply to SUNODH:


b[=2] // is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]

a |=> b[=2] ##1 c ; // is eauivalent to 
a |=> !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 c; 
// #35 clk=1, a=0, b=1, c=1 // Property Passed or Fail ?
// Because of !b[*0:$] ##1 c; 
// property is false at time 35 because b==1
// It requires NO b before a c
// Assertion would fail 
//
// If you had 
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=1
// If would pass because 
 b ##1 !b[*0:$] ##1 c
// get reduced to 
b ##1 c // b==1 at 25, c==1 at 30

On your testbench, use nonblocking assignments (the <= ) instead of the blocking assignment.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:
If you make a mistake you admit it.

 
a |=> b[=2] ##1 c ; // is eauivalent to 
a |=> !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 c; 
// #35 clk=1, a=0, b=1, c=1 // Property Passed or Fail ?
// Because of !b[*0:$] ##1 c; 
// equivalent to 
!b[*0] ##1 c or !b[*1] ##1 c or... 
// also
!b[*0] ##1 c // is equivalent to 
C // b can be 1 or 0
// property is true at time 35 because b==1

My apologies

4

In reply to ben@SystemVerilog.us:

Just for the record, at time 35 b was 0 before there, thus you do not get the condition
!b[*0] ##1 c but rather the condition of b[*0] ##1 c .
Thus my original response is correct for time 35. As I stated before,
a second b followed by c is a pass.
a 2nd b followed by b==0 then a b==1, c==1 is a fail.

// If you had 
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=1
// If would pass because 
 b ##1 !b[*0:$] ##1 c
// get reduced to 
b ##1 c // b==1 at 25, c==1 at 3