Difference in output using ##[0:$] $rose( b ) V/S $rose( b )[->1]

SystemVerilog
,
1

For the following code


always #5 clk = !clk;
 property a_to_b_rise;
    realtime a_rose;
  @(posedge clk) disable iff (!rst_n)
    ($rose(a), a_rose = $realtime) |-> $rose(b)[->1] ##0 ( ($realtime - a_rose) > 2ns ); 
 endproperty  

  ap1:assert property( a_to_b_rise ) $display("T:%2t Pass",$time);    
                                else $display("T:%2t Fails",$time);    
  initial begin
     #4 ; a = 1; b = 1;
    #20 ; $finish();
  end

The check works as per expectation i.e failure at T:5 .

However when I change the consequent to


property a_to_b_rise;
    realtime a_rose;
  @(posedge clk) disable iff (!rst_n)
    ($rose(a), a_rose = $realtime) |-> ##[0:$] $rose(b) ##0 ( ($realtime - a_rose) > 2ns ); 
endproperty

There is no failure at T:5 . Why is it so ?

2

In reply to Have_A_Doubt:


##[0:$] expr ##0 w //  is equivalent to 
##0   expr ##0 w or 
##1   expr ##0 w or 
##2   expr##0 w or 
..
##n   expr ##0 w 
/* if(expr==1) and w==0 then  you keep on looking for another possibility in later cycles. 
The consequent can never be a NO-MATCH because if no-match, then try for next cycle, maybe there will be  match. 
expr[->1] ##0 w // is equivalent to 
!expr[*0:$] ##0 expr  // Thus
// if (expr==1) in any cycle, then w must be true in the same cycle 
// Once expr==1 there cannot be cannot repeat cycle where expr==0
// the goto is like the 1st occurrence of the expression.

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:

Thanks Ben,
So essentially the consequent is expanded to :


##0 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
##1 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
##2 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
..............................................  or 
##N $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or

At time:5 since expression:( ($realtime - a_rose) > 2ns ) isn’t true , it keeps on checking the other remaining sequences.As a result no failure at time:5

I then changed property to:


property a_to_b_rise;
    realtime a_rose;
  @(posedge clk) disable iff (!rst_n)
    ($rose(a), a_rose = $realtime) |-> first_match( ##[0:$] $rose(b) ) ##0 ( ($realtime - a_rose) > 2ns ); 
 endproperty

This works as per intention

4

In reply to Have_A_Doubt:


($rose(a), a_rose = $realtime) |-> first_match( ##[0:$] $rose(b) ) ##0 ( ($realtime - a_rose) > 2ns ); // OK 
// Better coding 
($rose(a), a_rose = $realtime) |-> ##[0:$] $rose(b)[->1]  ##0 ( ($realtime - a_rose) > 2ns );
5

In reply to ben@SystemVerilog.us:

Ben ,

($rose(a), a_rose = realtime) |-> first_match( ##[0:] $rose(b) ) ##0 ( ($realtime - a_rose) > 2ns ); // OK
// Better coding
($rose(a), a_rose = realtime) |-> ##[0:] $rose(b)[->1] ##0 ( ($realtime - a_rose) > 2ns );

I am not clear why is clock delay ##[0:$] required for $rose(b) ?

Using it we don’t observe the failure at time:5 due to infinite ‘or’ sequence.
##[0:$] essentially will wait (till end of simulation) till sequence is true else it doesn’t throw an error.

Shouldn’t the following be sufficient ? :


 ($rose(a), a_rose = $realtime) |-> $rose(b)[->1]  ##0 ( ($realtime - a_rose) > 2ns );
6

In reply to Have_A_Doubt:

It was a copy/paste error on my part, apologies.
Yes, this is what you want |-> $rose(b)[->1] ##0 ( ($realtime - a_rose) > 2ns );