Assertion on Sva

SystemVerilog
1

I want to write a assertion to check whether the variable b occurs after 50 clock cycles of last occurance of variable a .

Here variable a is Valid and is randomised n of times.
and variable b idles ideal.

so we need to write assertion to check if after last occurance of valid and count 50 edge of clk and then check ideal is high , so assertion passes.

it fails if ideal is low at 50 clockedge .

so hindrance is checking for last time the variable a which is valid is high as it can go high n of times.

2

In reply to bhj78:

so hindrance is checking for last time the variable a which is valid is high as it can go high n of time

Are you saying that for every occurrence of “a” then variable b occurs after 50 clock cycles?
Or, are you saying that if I have something like:


a[*3] ##1 !a then b after the last b? 
Pehaps something like: $rose(a) ##1 !a[->1] |-> ##50 b;

Clarify your requirements
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

Hi Ben ,

I mean to say

Are you saying that for every occurrence of “a” then variable b occurs after 50 clock cycles?
No, we are only concerned about the last occurrence of “a”.I mean after last occurrence of “a”

Or, are you saying that if I have something like:
a[*3] ##1 !a then b after the last b? Not this
Pehaps something like: $rose(a) ##1 !a[->1] |-> ##50 b;

but something like

a[*3] ##1 !a then b after the last a? this but here a is getting repeated n number of times at any interval as it is randomised so
Pehaps something like: $rose(a) ##1 !a[->1] |-> ##50 b;// donot know this will catch the last occurance of a

4

In reply to bhj78:

$rose(a) ##1 !a[->1]
Catches the last occurrence of a before another rose of a.
No assertion will predict another repeats of a.
You may need some support logic or other info to limit what you are searching for. Again, you have to define what “Last” means.
Ben

5

In reply to bhj78:

In reply to ben@SystemVerilog.us:
Hi Ben ,
I mean to say
Are you saying that for every occurrence of “a” then variable b occurs after 50 clock cycles?
No, we are only concerned about the last occurrence of “a”.I mean after last occurrence of “a”
Or, are you saying that if I have something like:
a[*3] ##1 !a then b after the last b? Not this
Pehaps something like: $rose(a) ##1 !a[->1] |-> ##50 b;
but something like
a[*3] ##1 !a then b after the last a? this but here a is getting repeated n number of times at any interval as it is randomised so
Pehaps something like: $rose(a) ##1 !a[->1] |-> ##50 b;// donot know this will catch the last occurance of a


  a will be asserted within 50 cycles. if a is not asserted within 50 cycles , then b should be asserted. Should we consider that a will be the last occurrence? 
 always@(posedge clk) begin 
   if(a) count <= 0 ;
   else  count <= count + 1 ;
  end 
  
 assert property(@ posedge clk    count >= 50 |-> b) 
 
 is there case there in signal a can be asserted after 50 clock cycles?
6

In reply to kddholak:

yes there can be case where a can be asserted after 50 clock edge

7

In reply to bhj78:

In reply to kddholak:
yes there can be case where a can be asserted after 50 clock edge

How would design know its last a, and b should be asserted after 50 clock cycles ? here its not predictable behaviour.
if the design can predict the last a , and asserts b after 50 clock cycles. there should be some deterministic behavior