variable delay in assertions in System Verilog

Question

I am a newbie learning System Verilog assertions and found a code online from verificationguide.com for variable delays in assertions. But I am unable to understand a few things. Can someone elaborate on these following given descriptions?

// Copy variable value to the local variable.
(1,delay=v_delay)

How does this data gets copied?

// Decrements the value of the local variable and checks for the value of ‘delay’ equals ‘0’.
(1,delay=delay-1) [*0:$] ##0 delay <= 0

What does *0 mean? I know $ is for infinite checking till the end of the simulation. And why is ##0 needed as it just means 0 delay, if I am not wrong?

// waits for value of ‘delay’ equals to ‘0’
first_match((1,delay=delay-1) [*0:$] ##0 delay <=0)

How does the first_match function works and whats the syntax of it?

Please find the code below:

//-------------------------------------------------------------------------
//                      www.verificationguide.com
//-------------------------------------------------------------------------
module asertion_variable_delay;
  bit clk,a,b;
  int cfg_delay;

  always #5 clk = ~clk; //clock generation

  //generating 'a'
  initial begin 
    cfg_delay = 4;
        a=1; b = 0;
    #15 a=0; b = 1;
    #10 a=1; 
    #10 a=0; b = 1;
    #10 a=1; b = 0;
    #10;
    $finish;
  end

  //delay sequence
  sequence delay_seq(v_delay);
    int delay;
    (1,delay=v_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);
  endsequence

  //calling assert property
  a_1: assert property(@(posedge clk) a |-> delay_seq(cfg_delay) |-> b);

  //wave dump
  //initial begin 
  //  $dumpfile("dump.vcd"); $dumpvars;
  //end
endmodule

rag123 rag123 · Accepted Answer · 2020-06-14T21:14:40

1) The sequence delay_seq has a variable cfg_delay which is passed from the property. That is actually assigned to v_delay, which is in turn assigned to the local variable delay.

2) *0 is called an empty match. For example a[*0:$] |-> b means a [*0] or a [*1] or a [*2] .. a [$]

3) For example ($rose(b) ## [3:4] b) has two possible matches and ($rose(b) ## [3:$] b) can have infinite number of matches. To avoid unexpected behaviors because of multiple matches or cause an assertion to never succeed because all threads of antecedent must be tested for property to succeed. The first_match operator matches only the first of possibly multiple matches for an evaluation attempt and causes all the subsequent matches to be discarded.

variable delay in assertions in System Verilog

1 Answers