SVA to check clock toggling for a fixed number of cycles

SystemVerilog
, , , ,
1

Hi,

I’m trying to write assertions for sclk to be stable and toggling for 4 clock cycles before ack goes high and stable and toggling 8 clock cycles after ack goes low. ack goes high after req is asserted, so that’s the 4 clock cycles delay for ack before it’s asserted.


property sclk_ack_req;
     @(posedge ref_clk) $rose(req) |-> sclk[*4] ##1 $rose(ack) ##3 $fell(ack) ##1 sclk[*8];
   endproperty

Please help me with this one, thanks.

2

In reply to foxtrot:


// sclk to be stable and toggling for 4 clock cycles 
// Q: What is the definition of "stable"? 
//    steady in value for 4 ref_clk cycles or 
//    toggling for 4 sck cycles?   You mention both

// before ack goes high and stable and toggling 8 clock cycles after ack goes low. 
// ack goes high after req is asserted, so that's the 4 clock cycles delay for ack before it's asserted. 
// Q: Very poor defintion of the requirements.  
//    Now you are talking about sclk to be a clock used as delay. 
//    GIGO.  I don't understand your requirements. 

property sclk_ack_req;
     @(posedge ref_clk) $rose(req) |-> sclk[*4] ##1 $rose(ack) ##3 $fell(ack) ##1 sclk[*8];
   endproperty
// Above property says: 
   // At the rose(req) you have sclk==1 for 4 consecutive ref_clk clock cyccles.
   // This is then followed by a rose(ack)and 3 ref_clk later ack fell. 
   // This is then followed by sclk==1 for 8 consecutive ref_clk clock cyccles.

   // Note that $rose(ack) ##3 $fell(ack) does not cover the case of this sequence 
  //  $rose(ack) ##1 ack==0 ##1 ack==1 ##1 ack==0
   // 0   1  x 1 0 
   // to avoid this, you need 
   // $rose(ack) ##0 ack[*3] ##1 $fell(ack)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

sclk must be stable and toggling before ACK asserts (min 4 SCLKs)
 sclk must be stable and toggling after ACK de-asserts (min 8 SCLKs)
 sclk must be stable and toggling when both the REQ and ACK are asserted

Here you go, this is what I need to do.

Thanks

4

In reply to ben@SystemVerilog.us:

In reply to foxtrot:


// sclk to be stable and toggling for 4 clock cycles 
// Q: What is the definition of "stable"? 
//    steady in value for 4 ref_clk cycles or 
//    toggling for 4 sck cycles?   You mention both
// before ack goes high and stable and toggling 8 clock cycles after ack goes low. 
// ack goes high after req is asserted, so that's the 4 clock cycles delay for ack before it's asserted. 
// Q: Very poor defintion of the requirements.  
//    Now you are talking about sclk to be a clock used as delay. 
//    GIGO.  I don't understand your requirements. 
property sclk_ack_req;
@(posedge ref_clk) $rose(req) |-> sclk[*4] ##1 $rose(ack) ##3 $fell(ack) ##1 sclk[*8];
endproperty
// Above property says: 
// At the rose(req) you have sclk==1 for 4 consecutive ref_clk clock cyccles.
// This is then followed by a rose(ack)and 3 ref_clk later ack fell. 
// This is then followed by sclk==1 for 8 consecutive ref_clk clock cyccles.
// Note that $rose(ack) ##3 $fell(ack) does not cover the case of this sequence 
//  $rose(ack) ##1 ack==0 ##1 ack==1 ##1 ack==0
// 0   1  x 1 0 
// to avoid this, you need 
// $rose(ack) ##0 ack[*3] ##1 $fell(ack)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Let’s consider your comment, I don’t want to check for sclk==1 for 4 clock cycles, but I want to check whether it’s toggling for 4 clock cycles. I’m unable to do that toggling part, this is where I need your help.

5

In reply to foxtrot:
You have not described the relationship between ref_clk and sclk
How are they derived? Something like:


always_ff @(posedge sclk) begin
   ref_clk <= !ref_sclk;     
end
// That relationship determines how you proceeed.  You may need multiclocking. 
// ref_clk   ^  |  ^  |  ^  |  ^  |  ^  |  ^  |
// sclk      1     0     1     0     1
// req       0     1     x
// for the *4 repeat, perhaps something like this? 
property sclk_ack_req;
    bit v; 
    @(posedge ref_clk) 
       $rose(req) |-> @(ref_clk) (1, v=ref_clk) 
                     ##0 (sclk==v ##1 sclk==!v)[*4] 
    ##1 @(posedge ref_clk) $rose(ack) ##3 $fell(ack) ##1 sclk[*8];
endproperty

GBGO, be more specific in your definition of requirements
Ben