Assertion for dynamic variable timing checks

SystemVerilog
,
1

Hello,

I am trying to check a variable timing which is calculated at the beginning of each slice.

I used the below code, but it does not check every time the initial_tun_v_en falls. I am not sure why.

int delay;
assign delay = 17 + ( v_a_prog_chei_time * ( slice_no - 2 ));
property p_prog_time_check;
        int v;
    @( posedge  control_clk )
    disable iff (( inj_en_b == 1'b1 ) | ( PROG == 1'b0 ))
    ( $fell( hvsw_preset_en ), v=delay+1'b1) |-> first_match((v>0, v=v-1'b1)[*0:$] ##1 v==0 ##0 $fell( initial_tun_v_en ));
endproperty

Can anyone help?

Thank you,
-Vikram

2

In reply to casper:
Try for the consequent

 first_match((1, v=v-1'b1)[*1:$] ##0 v==0 ##0 $fell( initial_tun_v_en ));

With that, you basically keep on decremeting “v” until v==0, and then check for the fell. You know that since delay is a positive number, v==0 will eventually occur. ***** A word of caution ****** (a[*0] ##1 b) is same as (b) Thus, in (v>0, v=v-1'b1)[*0:] ##1 v==0, you have the equivalency for the 1st term of
((v>0, v=v-1’b1)[*0] ##1 v==0) // SAME AS (v==0), with v not decremented since
the sequence-matched-item is not exercised.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
3

Hello Ben,

I tried it. Now it seems to be checking. But i am facing failures for anything other than the initial start of the assertion after a disable. After more debugging, it does not seem to be able to calculate the delay which keeps changing with slice_no. Hence these errors. I am not sure how to approach this problem.

Thank you,
-Vikram

4

In reply to casper:

it does not seem to be able to calculate the delay, which keeps changing with slice_no. Hence these errors.

[Ben] You need to clarify your requirements. Based on your assertion below, your requirements seem to be as follow (ignoring the disable for now):

  1. upon a fell of hvsw_preset_en, capture the value of “delay”, which is based on the current slice number. Ignoring the equation for the value of delay for now)
  2. Following the number of cycles defined by the captured (i.e., saved) “delay”, signal initial_tun_v_en is expected to fall.

If that is not your requirements, you need to clarify what to expect at which cycle; and that is your responsibility. Remember GIBO!!! Don’t blame SVA :)


int delay;
assign delay = 17 + ( v_a_prog_chei_time * ( slice_no - 2 ));
property p_prog_time_check;
 int v;
 @( posedge control_clk )
 disable iff (( inj_en_b == 1'b1 ) | ( PROG == 1'b0 ))
  ($fell(hvsw_preset_en ), v=delay+1'b1) |-> 
  first_match((1, v=v-1'b1)[*1:$] ##0 v==0 ##0 $fell( initial_tun_v_en ));
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
5

In reply to ben@SystemVerilog.us:

Hello Ben,

Thanks for the reply. Yes I agree i should have been clearer with spec. I tried to execute the SVA as per your reply. But the SVA does not seem to trigger ( no pass or fails). Is there a good way to debug this?

Thanks,
-Vikram

6

In reply to casper:

In reply to ben@SystemVerilog.us: I tried to execute the SVA as per your reply. But the SVA does not seem to trigger ( no pass or fails). Is there a good way to debug this?

Tools provide debug features. If not disabled, the assertion should trigger at every successful attempt. You could add some $display.


property p_prog_time_check;
 int v;
 @( posedge control_clk )
 disable iff (( inj_en_b == 1'b1 ) | ( PROG == 1'b0 ))
  ($fell(hvsw_preset_en ), v=delay+1'b1, $display("attempted @t %t", $time) ) |-> 
  first_match((1, v=v-1'b1, $display("@t %t", $time)[*1:$] ##0 v==0 ##0 $fell( initial_tun_v_en ));
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

7

In reply to ben@SystemVerilog.us:

Thank you so much Ben. You taught me a lot with this few post. I used $changed to reduce the large memory usage as complained by the tool.

My final assertion looks like this

property p_prog_time_check;
    int v;
     @( posedge control_clk )
    disable iff (( inj_en_b == 1'b1 ) | ( hvsw_preset_en == 1'b1 ) | ( PROG == 1'b0 ))
    ($changed(dio_normal) , v=delay+1'b1) |->
    first_match((1, v=v-1'b1)[*0:$] ##0 v==0 ##0 $changed( dio_normal ));
endproperty