Solution of Assertion with variable ## delay

  •  Assertion is the life savior of verification and design engineers . With the help of assertions we could verify more and precisely in very less time.
  •  There are many tricks for writing property of assertion , this topic of the blog will describe one of the tricks of writing assertion.

EXAMPLE

  • There is one input signal ‘a‘ and one output signal ‘b‘.
  •  whatever the value of a is given to b after 10 clock cycle , we need to write property to check it.

It’s quite easy…


property delay_check();              // take all signals as defined in the code 
@(posedge clk)
   disable iff (! rst)                         //  Disable if reset
    a |-> ##10 b;                            
endproperty

===or====

`define DELAY 10

property delay_check();              // take all signals as defined in the code
@(posedge clk)
disable iff (! rst)                            //  Disable if reset
a |-> ##`DELAY b;
endproperty


  • As of now we can use only constant (either fixed number or `define ) after ## to specify number of clocks.
  • If we want to use variable like integer after ## , we could not directly write

int delay;
property delay_check();
…….
a |-> delay b;
….
endproperty

It will give a compile time error that you can write only constants 


  •  We could not write directly variable but using repetition operator we could achieve same goal , Here is the logic

int delay;
property delay_check();
int d;                                                   // local variable which store value of delay
bit prev_a;                                         // local variable which store input value

@(posedge clk)
disable iff (!rst)
((a == 0 || a == 1), prev_a = a, d=delay+1’b1 ) |-> ((d != 0 && d > 0) , d=d-1’b1)[*1:$] ##1 (d == 0) ##0 (b == prev_a);

endproperty


  • Bold part in above expression is the logic
  1. First we store value of delay in local d
  2. When posedge of  clk event  triggered  our property , Input value is stored in prev_a
  3. than we take delay signal and decrement it one by one untill it reaches to zero
  4. After that we simply check output value which has to be prev_a or else assertion fails
  5. Here we took help of repetition operator to repeat whole expression ((d != 0 && d > 0) , d=d-1’b1) in code..until d reaches to zero.
Here I also shared link of  code which will run on Questa , VCS , EDA playground. For better view of Waveforms go with Questa and VCS

=> LINK : http://www.edaplayground.com/x/WgB

Go on play with it and comment if you have any query..

2 responses

  1. Can u explain in some more detail:
    Suppose delay is 4
    (5>0,d=4)##1(4>0,d=3)##1(3>0,d=2)##1(2>0,d=1)##1(1>0,d=0)##1(d==0)
    so it sums up to 5 delays but not 4 .
    Where did i go wrong ?

    Like

    1. Here, following will be the sequence:
      1st posedge: check 5>0 and assign d=4
      2nd posedge: check 4>0 and assign d=3
      3rd posedge: check 3>0 and assign d=2
      4th posedge: check 2>0 and assign d=1
      5th posedge: check 1>0 and assign d=0
      6th posedge: check d=0.
      So, it will delay by 5 clock edges and then check on the next edge ‘d’.

      Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: