Tuesday, 14 June 2011

How to use variable delay in property?

I want to compare input bit with output bit using property but there is some delay between input and output. Let's say delay between input and output is 2 clock ticks.
So we can write SV property as below :
-----------------------------------------------------------------------
property bit_check(data_in,data_out);
bit x ;
(`true,x=data_in) |-> ##2 (data_out == x);
endproperty
-----------------------------------------------------------------------
But in my case the delay between input and output is not fix from beginning. I can get this information during the run time. So I should write property like following way :
-----------------------------------------------------------------------
property bit_check(data_in,data_out,delay);
bit x ;
(`true,x=data_in) |-> ##(delay) (data_out == x);
endproperty
-----------------------------------------------------------------------
When I use property like above the tool gives error as variable delay does not allow in property. It should be constant and the value should be predefined otherwise tool generates compilation error.
So to handle variable delay, I have added one more sequence between input and output instead of ##(delay). I wrote property like below and it works for me.
-----------------------------------------------------------------------
property bit_check(data_in,data_out,delay);
bit x ;
int cnt ;
(`true,x=data_in,cnt=0) |-> ((cnt < delay),cnt++)[*0:$] ##1 (cnt == delay) |-> (data_out == x);
endproperty

No comments:

Post a Comment