How to check a signal to be one for 'n' clocks in SVA

SystemVerilog
, ,
1

I want to check a signal to be high for n clocks where n can be configurable local variable

2

I want to check a signal to be high for n clocks where n can be configurable local variable


module m; 
  bit clk, a, b; 
  int g=5; 
  property p_g; 
   int v; 
   ($rose(a), v=g) |-> (1'b1, v=v-1'b1)[*1:$] ##0 v==1'b0;
  endproperty
  ap_g: assert property(@ (posedge clk) p_g);

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

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books
3

In reply to ben@SystemVerilog.us:

Hi Ben,

I think above property does not check whether Signal a reamins high for all 5 clocks so can we write this as

(rose(a), v=g) |-> (a==1'b1, v=v-1'b1)[*1:] ##0 v==1’b0 ##0 a==1’b1;

Thanks & Regards
Raku

4

In reply to raku:

You’re correct, my mistake.
Thanks for the update
Ben

5

In reply to ben@SystemVerilog.us:

(a==1’b1, v=v-1’b1) this will work as an and ? what is purpose of ##0’s . We can not do it using $stable?

Chandru

6

In reply to Chandrashekhar Goudar:

(a==1’b1, v=v-1’b1) this will work as an and ? what is purpose of ##0’s .

(a==1'b1, v=v-1'b1)[*1:$] ##0 v==1'b0 ##0 a==1'b1;

You’re correct, you could have written this as:

(a==1'b1, v=v-1'b1)[*1:$] ##0 v==1'b0 && a==1'b1;

the Boolean_expression && Boolean_expression has a different connotation than the Boolean_expression ##0 Boolean_expression; the && operator has a combinational logic inference, whereas the ##0 has sequential inference (e.g., occurring after). Thus, in this case, I wanted to express that at the end of the count (when v==0) I want to then test that a==1’b1. The point here is that from an intent or emphasis point of view, there is a difference.

We can not do it using $stable?

Cannot use $stable because the range is not static, it is dynamic, per the requirement:

check a signal to be high for n clocks where n can be configurable local variable

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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
7

In reply to ben@SystemVerilog.us:

Thank you Ben and raku for your inputs

8

In reply to raku:

Hi Raku,

I see that this code is perfectly working fine for ‘x’ cycles but aren’t we taking care of falling edge of ‘a’ ??
I do not think ‘a’ will be high for exactly ‘x’ cycles, how are we checking whether ‘a’ is falling to 0 after ‘x’ cycles i.e after our local counter ‘v’ goes to zero ??

Thanks in advance!