Request - Acknowledge related Assertion

SystemVerilog
,
3

In reply to ben@SystemVerilog.us:

Hi Ben ,

Using goto ( → 1 ) instead of Non-Consecutive ( = 1 ) for both ack N $rose( req ) gives the desired results .

However I am still confused between the working of the two .


 @( posedge clk )  a  |=> b[ =2] ##1 c ;  //  (EQ1)

 @( posedge clk )  a  |=> b[ ->2] ##1 c ; //  (EQ2)

My understanding is that for (EQ2) , ’ c ’ should be high exactly 1 clock after
’ b ’ is sampled true twice consecutively / non - consecutively

For (EQ1) ’ c ’ could be high anytime 1 clock after ’ b ’ is sampled true twice consecutively / non - consecutively

So essentially the qualifying event( ##1 c ) differentiates the two .

If I write property as ::


    property  req_ack ;
 
  `ifdef GO_TO

    @( posedge clk )  $rose( req )  |=>  ack [ ->1 ] ; 
 
 `else

    @( posedge clk )  $rose( req )  |=>  ack [ = 1 ] ; 

 `endif

  endproperty

  initial  forever  #10 clk = ! clk ;

  c_property : cover   property ( req_ack )  $display(" TIME : %0t  PASS " , $time ) ;

  initial  begin

    // [1]  ' req '  is  True  on  1st  posedge  N  then  ' req ' is  de - asserted  just  before  Next  posedge .
    //
    //      ' ack '  is  asserted  at  TIME : 49  !!

       #9 ;  req = 1 ;    //  TIME:9

      #20 ;  req = 0 ;    //  TIME:29

      #20 ;  ack = 1 ;    //  TIME:49

      #5 ; 
      $finish(); 
 end

In both cases ( with or without +define+GO_TO ) the assertion passes at TIME : 50 .
My understanding is that since there is no qualifying event after ’ ack ’ they give same results .

Since there is no qualifying event in the original question I posted how do they result in different output ? .

!ack[*0:$] being an empty sequence , which says ‘!ack’ needs to be true on 0 clock tick . Doesn’t it mean that ’ ack ’ need not be false on any clock tick ?


LRM  says  ::

Goto repetition :: "The overall repetition sequence matches at the last iterative match of the operand."

Nonconsecutive repetition  ::  "The overall repetition sequence matches at or after the last iterative match of the operand, but before any later match of the operand"

This too however is confusing to me especially “at or after the last iterative match of the operand, but before any later match of the operand”