SVA : question on using throught vs [*n]

SystemVerilog
, ,
1

I came across this assertion in a book where the requirement was : When burst mode (bmode) is asserted oe and dack must be found asserted after 2 clocks ; oe and dack must remain asserted for minimum of 4 clocks after both are found asserted and the bmode must remain deasserted while the oe and dack is high

Question : I want to learn how do I modify the same without using the throught operator


//Solution explained using throught 
sequence data transfer;
##2 ((dack ==1) && (oe==1))[*4]; //After 2 cycles the oe and dack are high for 4 cycles continuous
endsequence

sequence checkbmode;
(!bmode) throught data_transfer; //Making sure that bmode is not high while oe and dack are high
endsequence

property pbrule1;
@(posedge clk) $fell(bmode) |-> checkbmode;
endproperty



property pbrule1;
@(posedge clk) $fell(bmode) |-> ##2 ((dack ==1) && (oe==1))[*4] && (!bmode)[*4];  //Does this look correct ?
endproperty

So if bmode goes low the fell gets triggered say cycle 0 in cycle 1 it goes high and goes back low in cycle 2 the property still passes ?

2

In reply to CPU_Verif:
The solution explained in the book is incorrect because it does not meet the following requirement:
“Making sure that bmode is not high while oe and dack are high”
What it does instead is:
“Making sure that bmode is not high for 2 cycles and then when oe and dack are high”
Below are my untested changes

 
//Solution explained using throught 
sequence data transfer; // 6 cycles in length 
 ##2 ((dack ==1) && (oe==1))[*4]; 
//After 2 cycles the oe and dack are high for 4 cycles continuous
endsequence
 
sequence checkbmode;
(!bmode) throughout data_transfer; 
//Making sure that bmode is not high for 2 cycles and then  when oe and dack are high
endsequence
 
//Making sure that bmode is not high for 2 cycles and then  when oe and dack are high
@(posedge clk) $fell(bmode) |-> checkbmode;
endproperty

//Making sure that bmode is not high only when oe and dack are high
// In other words, (dack==1 && oe==1 && !bmode)[*4]; 
property pbrule1a; // simplified to 
    @(posedge clk) $fell(bmode) |-> ##2 (dack==1 && oe==1 && !bmode)[*4];   
endproperty

property pbrule1b;
@(posedge clk) $fell(bmode) |-> ##2 
 (dack ==1 && oe==1[*4] intersect !bmode[*4]);   
endproperty

//Making sure that bmode is not high for 2 cycles and then  when oe and dack are high
endsequence
property pbrule1c;
    @(posedge clk) $fell(bmode) |-> (##2 dack==1 && oe==1[*4]) intersect !bmode[*6]; // 6 cycles total 
endproperty

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:

Thanks Ben for your help. I agree with intersect solution
//Making sure that bmode is not high for 2 cycles and then when oe and dack are high
endsequence
property pbrule1c;
@(posedge clk) $fell(bmode) |-> (##2 dack==1 && oe==1[*4]) intersect !bmode[*6]; // 6 cycles total
endproperty
Seq 1 intersect seq 2 => two sequences start at the same time and end at the same time. satisfies my condition here .

May I please know if we can write the same without using intersect , that is using [*] only

4

In reply to CPU_Verif:


 $fell(bmode) |-> (##2 dack==1 && oe==1[*4]) intersect !bmode[*6]; 
// same as 
 $fell(bmode) |-> !bmode[*2] ##0 (dack==1 && oe==1 && !bmode) [*4];
5

In reply to ben@SystemVerilog.us:

Thank you Ben