Assertion to check number of clock pulses

SystemVerilog
1

Is it possible to write SV assertion for something like this wrt a clk
when cs_n is low then sck toggles 16 times before cs_n goes high

How do we count the number of sck clock pluses?

2

In reply to gv_bing:
Your requirements were not very clear. I interpreted them to be:
Following a fall of cs_n, cs_n remains at zero for 16 cycles, and then rises to a logical one. cs_n is a synchronous signal clocked at the posedge of sck.


ap_cs_n: assert property(  
        @(posedge sck)  $fell(cs_n) |=> !cs_n[*16] ##0 $rose(cs_n));

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

No. Let me put it differently
there are two clocks – clk and sck

  1. cs_n is a synchronous signal clocked at the posedge of clk
  2. cs_n goes low
  3. count sck for 16 cycles
  4. cs_n goes high

note that when cs_n is high sck is always 0

4

In reply to ben@SystemVerilog.us:

In reply to gv_bing:
Your requirements were not very clear. I interpreted them to be:
Following a fall of cs_n, cs_n remains at zero for 16 cycles, and then rises to a logical one. cs_n is a synchronous signal clocked at the posedge of sck.


ap_cs_n: assert property(  
@(posedge sck)  $fell(cs_n) |=> !cs_n[*16] ##0 $rose(cs_n));

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:

For training, consulting, services: contact http://cvcblr.com/home.html =>
Hi Ben, when I click download profile, file not found (404 error) occurs. What should I do? Thanks~

5

In reply to gv_bing:


/* there are two clocks -- clk and sck
1. cs_n is a synchronous signal clocked at the posedge of clk
2. cs_n goes low
3. count sck for 16 cycles, cs_n stays low <--- ADDED this 
4. cs_n goes high*/
     ap_cs_n: assert property(  
        @(posedge clk)  $fell(cs_n) |-> 
            @(posedge sck) !cs_n[*16] ##0 @(posedge clk) $rose(cs_n));
// note that when cs_n is high sck is always 0 
    ap_cs_nHI: assert property(  
              @(posedge clk)  cs_n |-> sck==1'b0);

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:
6

In reply to gv_bing:

Simpler with modeling code - untested below.


  // 1. cs_n is a synchronous signal clocked at the posedge of clk

  always @(posedge clk)
    if (!cs_n) sclk_count <= 0;

  // 2. cs_n goes low
  // 3. count sck for 16 cycles
  always @(posedge sclk) // assume 16 posedge
   sclk_count++; // lazy, use <= + 1

  // 4.  cs_n goes high
  a_chk_sclk_16 : assert property
    ( @(posegde clk) $rose (cs_n) |-> sclk_count == 16 );

  // Am sure you will need to tweak the NBA/BA/count by 1-2 to get it right

Good Luck
Srini
www.verifworks.com

7

In reply to Srini @ CVCblr.com:
Your figures show that clk is a master clock and sck is a derived divde-by-two clock and is not a separate async clock. If that is the case, then the following should work
See diagrams below.


 ap_cs_n: assert property(  
        @(posedge clk)  $fell(cs_n) |-> 
            (##2 sck && !cs_n ##2 !sck && !cs_n)[*16] ##2 $rose(cs_n));

Google Photos

Google Photos

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:
8

In reply to ben@SystemVerilog.us:

Thank you Ben and Srini, seems the tool is not supporting this kind of complex assertion and choking after 3 cycles. There might a bug in the tool.

9

With 2 clocks

 
ap2_cs_n: assert property(  
        @(posedge clk)  $fell(cs_n) |-> 
            ##0 @(sck)!cs_n)[*32] ##0 @(posedge clk) !cs_n[*2] ##1 $rose(cs_n));
// untested. Follow the timing

// updated
ap2_cs_n: assert property(  
        @(posedge clk)  $fell(cs_n) |-> 
            ##0 @(sck)!cs_n)[*32] ##1 @(posedge clk) !cs_n[*2] ##1 $rose(cs_n));
// ##1 instead of ##0 because posedge sck is at same cycle as posedge of clk

I prefer the previous reply.
The previous reply should easily be handled by any tool, as it is straightforward.
Ben

10

In reply to gv_bing:

My previous code snippet should be supported by most/all tools, see below:



  // 4.  cs_n goes high
  a_chk_sclk_16 : assert property
    ( @(posegde clk) $rose (cs_n) |-> sclk_count == 16 );

Are you saying the above isn’t supported?

Srini

11

In reply to Srini @ CVCblr.com:

Thank you Srini.

Agree, this is easier and cleaner, this works too.

12

In reply to ben@SystemVerilog.us:

Thank you Ben. I’m not sure how the tool is expanding the inner block, but the following is working.

property p1;
@(posedge clk)
$fell(a) |=> (##1 b && !a ##2 !b && !a)[*16] ##2 $rose(a);
endproperty

13

In reply to gv_bing:
Because the sequence (##1 b && !a ##2 !b && !a) is braced with parentheses, the repeat applies to the whole sequence. Thus,


(##1 b && !a ##2 !b && !a)[*16] 
// is same as 
sequence q_ab; 
  ##1 b && !a ##2 !b && !a;
endsequence  

q_ab[*16]

Ben SystemVerilog.us