Achieving Dynamic delays in SVA using subroutine

Hi ,
I was trying alternative to Dynamic delay : sq_1 |-> ##d1 sq2 using subroutine call ( so that I can use SV procedural constructs ) : edalink

However I observe the o/p differs across simulators . Two tools throw assertion failure at T:5 whereas
3rd tool throws compilation error : xmvlog: *E,SFLNOS (testbench.sv,34|50): Delays or wait statements in match item task calls are not supported.

[Q1] Is the code legal ? i.e Can the task block ?
[Q2] If the code is legal then why does the assertion fail at T:5 ? I expected ‘b’ to be evaluated only after task completes at T:45

In reply to MICRO_91:
[Q1] Is the code legal ? i.e Can the task block ?
[Ben]The code is legal in that it will compile and should simulate.
We do not address tools in this forum. Note that not every feature of SV is
necessarily supported by vendors.
[Q2] If the code is legal then why does the assertion fail at T:5 ? I expected ‘b’ to be evaluated only after task completes at T:45
[Ben] Tasks do NOT block; it’s more like fire and forget.
Thus, @( posedge clk ) a |-> ( 1, dynamic_delay2( val ) ) ##0 b ;
is functionally (but not per 1800) equivalent in this case to :
@( posedge clk ) a |-> (1 ##0 b) and (1, dynamic_delay2( val ));
I use the “and” to demonstrate the concept that the task call has nothing to do
with the (1 ##0 b). The task fires and does its thing until completion.
If you want to use the task approach, then complete the consequent within the task,
as shown in the code below.
Dynamic Delay(2) - EDA Playground // code
EPWave Waveform Viewer // wave

task automatic dynamic_delay2( int cnt );  
    $display("Task called at T:%0t with i/p arg == %0d",$time,cnt);
    if( cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
      am_b: assert(b) pass=pass+1; else  fail=fail+1;
       $display("Task completes at T:%0t",$time);
     end   
  endtask
  
    property prop;       
      @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ); //  ##0 b ;
    endproperty
  
  assert property ( prop ) pass=pass+8; // $display("T:%0t Assertion PASS" , $time);
    
                     else  fail=fail+8; // $display("T:%0t Assertion FAILS" , $time);

See my paper Understanding the SVA Engine Using the Fork-Join Model

Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.

BTW, your original code, slightly modified to show the assertion results in the waveform is available at:
Dynamic Delay(1) - EDA Playground // code
EPWave Waveform Viewer // wave


// Original code with BAD use of tasks 
task dynamic_delay2( int cnt );  
    $display("Task called at T:%0t with i/p arg == %0d",$time,cnt);
    if( cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
       $display("Task completes at T:%0t",$time);
     end   
  endtask
  
    property prop;       
      @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ) ##0 b ;
    endproperty
  
  assert property ( prop ) pass=pass+1; // $display("T:%0t Assertion PASS" , $time);
    
                     else  fail=fail+1; // $display("T:%0t Assertion FAILS" , $time);

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

Thanks Ben for the detailed explanation .
So b is evaluated ONLY once at T:5 i.e same time as consequent is evaluated .It isn’t evaluated again after task completes

A few questions regarding :

[Ben] Tasks do NOT block; it’s more like fire and forget.

I was referring section 16.11 of the LRM which says :

All subroutine calls attached to a sequence are executed at every end point of the sequence. For each end point, the attached calls are executed in the order they appear in the list. Assertion evaluation does not wait on or receive data back from any attached subroutine. The subroutines are scheduled in the Reactive region,like an action block.

This means that although property expression ( variables ‘a’, ‘b’ ) is evaluated in observed region the task dynamic_delay2 gets executed in Reactive region ?
So ‘b’ would be evaluated in Observed region at T:5 before $display within the task which executes in Reactive region at T:5 .
(1) As both $display in PASS/FAIL action block as well as $display in task dynamic_delay2 execute in Reactive region , is there a pre-defined order of execution b/w the 2 $displays?
(2) Also what does the following mean : “All subroutine calls attached to a sequence are executed at every end point of the sequence.” ?

In reply to MICRO_91:

In reply to ben@SystemVerilog.us:
Thanks Ben for the detailed explanation .
So b is evaluated ONLY once at T:5 i.e same time as consequent is evaluated .It isn’t evaluated again after task completes

[Ben] Correct. The way I see it, The subroutines (i.e., tasks) are scheduled in the Reactive region, like an action block. There is no blocking to the sequence within the assertion.
If you have a function that return a value, e.g., (seq, v=f(v)), the f(v) is considered
an expression and is evaluated in the Observed Region. If the function is void,
e.g., (seq, f_void(v) then f_void is executed in the Reactive Region. The task or void function
once started can complete after the assertion that called is done.
Am verifying this statement with a colleague

A few questions regarding :
I was referring section 16.11 of the LRM which says :

All subroutine calls attached to a sequence are executed at every end point of the sequence. For each end point, the attached calls are executed in the order they appear in the list. Assertion evaluation does not wait on or receive data back from any attached subroutine. The subroutines are scheduled in the Reactive region,like an action block.

This means that although property expression ( variables ‘a’, ‘b’ ) is evaluated in observed region the task dynamic_delay2 gets executed in Reactive region ?
So ‘b’ would be evaluated in Observed region at T:5 before $display within the task which executes in Reactive region at T:5 .

[Ben] Youre referring to this code:

..@( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ) ##0 b ;
task dynamic_delay2( int cnt );  
    $display("Task called at T:%0t with i/p arg == %0d",$time,cnt);
...

Yes. Also, b may have schaged value if it was updated in the NBA region.
You should use $sampled(cnt) instead of cnt.

(1) As both $display in PASS/FAIL action block as well as $display in task dynamic_delay2 execute in Reactive region , is there a pre-defined order of execution b/w the 2 $displays?

Its probably a tool thing, but my guess is that there is queue

(2) Also what does the following mean : “All subroutine calls attached to a sequence are executed at every end point of the sequence.” ?

That is true. for example: sequence s; a ##1 b; endsequence
…(a ##1 b, v=1) // v==1 after a ##1 bl the end point o that sequence
…(s, v=1) // v==1 at the end point of s
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

Thanks Ben for pointing the following :

Also, b may have schaged value if it was updated in the NBA region.
You should use $sampled(cnt) instead of cnt.

Hence in your solution to the original question at the top :


task automatic dynamic_delay2( int cnt );  
    $display("Task called at T:%0t with i/p arg == %0d",$time,cnt);
    if( cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );

// Changed to $sampled( b ) so that pre-poned value is used incase b is updated in NBA region
       am_b: assert( $sampled(b) ) $display("Assertion Pass"); 
         else  $display("Assertion Fails");
       $display("Task completes at T:%0t",$time);
     end   
  endtask
 
    property prop;       
      @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ); //  ##0 b ;
    endproperty
 
    assert property ( prop ); // PASS/FAIL within task

In reply to MICRO_91:

In reply to ben@SystemVerilog.us:
Thanks Ben for pointing the following :
Hence in your solution to the original question at the top :
…am_b: assert( $sampled(b) );

Not necessarily. If you use good RTL guidelines. Specifically,

  1. Every register is updated with the nonblocking assignment
    (e.g., always @(posedge clk) b <= q; )
  2. All comb logic has its source from those registers updated in the NBA region.
    (e.g., always_comb m=!b; )
    If the immediate assertion follows the @(posedge clk), like in your example) then
    the assertion occurs in the 1st iteration of the Active region; thus “b” has the same value as its sampled value. Example:

 always_comb  m=!b; // m is updated in the 2nd iteration of the Active region 
                    // After b's updated in the NBA region 
 always @(posedge clk) begin 
   b <= q;  
   am_m: assert(m); 
 end

HOWEVER, if I wrote something like:
…@( posedge clk ) a |-> c ##cnt ##0 b ; // illegal if cnt is dynamic
and I wanted to use a task that computes this consequent then I would need
to use the $sampled(c) since the task is executed in the Reactive region.
…@( posedge clk ) a |-> ( 1, dynamic_delay2( val ) );


// removed the debugging stuff for simplicity 
task automatic dynamic_delay2( int cnt );  
// @( posedge clk )  a  |-> c ##cnt ##0 b ; 
    am_cb: assert($sampled(c)); 
    if($sampled(c) && cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
    // NO NEED to Changed b to $sampled( b ) 
       am_b: assert(b); // b's value == $sampled(b) 
     end   
  endtask
 
    property prop;       
      @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ); 
    endproperty
 
    assert property ( prop ); // PASSes if a==1, it never fails 

NOTE: Formal input args passed by value receive sampled actual arguments.


Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh

In reply to ben@SystemVerilog.us:

NOTE: Formal input args passed by value receive sampled actual arguments.
Thus, for …@( posedge clk ) a |-> c ##cnt ##0 b ; // illegal if cnt is dynamic
and I wanted to use a task that computes this consequent then I could pass the argument c to the task.


// removed the debugging stuff for simplicity 
task automatic dynamic_delay2( int cnt, bit c );  
// @( posedge clk )  a  |-> c ##cnt ##0 b ; 
    am_cb: assert(c); // the actual is the sampled value 
    if($sampled(c) && cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
    // NO NEED to Changed b to $sampled( b ) 
       am_b: assert(b); // b's value == $sampled(b) 
     end   
  endtask
 
    property prop;       
      @( posedge clk )  a  |->  ( 1, dynamic_delay2( val, c) ); 
    endproperty
 
    assert property ( prop ); // PASSes if a==1, it never failsc

Ben

In reply to ben@SystemVerilog.us:

Hi Ben .


  bit clk , a ;
  bit [2:0] b , c ;
  
  always #5 clk = !clk ; 
  int val = 4 ;
  
  always @( posedge clk ) b <= b + 1 ; 
  always @( posedge clk ) c <= c + 1 ;

 task automatic dynamic_delay2( int cnt );  // Executes in Reactive Region
    // Trying Sequence : @( posedge clk )  a  |-> c ##dyn_delay b ; 
    $display(" Within task b == %0d",b); // I observe value updated in NBA region
    $display(" Within task c == %0d",c); // I observe value updated in NBA region
    am_cb: assert( $sampled(c) ); 
    if($sampled(c) && cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
      $display(" Delay completes at T:%0t",$time);
// For below immediate assertion : Some tools sample NBA updated value while some sample Pre-poned
     am_b: assert( b == 4 )  // Discrepancy  here ?
           $display(" PASS with b == %0d",b);
      else $display(" FAIL with b == %0d",b);
     end   
  endtask
 
  property prop;       
   @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) ); 
  endproperty
 
  assert property ( prop );

Verilog tells us that $display executes in Active region
[1] When does the $displays within the task execute ? Is it in Reactive region OR in Active region ( via loopback from Re-NBA to Active Region )
[ NOTE : There is No loopback directly from Reactive to Active Region ]

[2] It seems that some tools use updated value of b : edalink

 Hence to avoid the tool discrepancy I feel it's better to use $sampled( b ) instead .

 Within the task when we write : **repeat( cnt ) @( posedge clk );**

@(posedge clk) executes in **re-entrant Active region ( via loopback from Re-NBA to Active Region )** 

( However I believe the NBA assignment to b would execute before the loopback to Active region )
When we write the next statement as : assert(b);

(a) Are we still in Active Region ? i.e Non-blocking update to ‘b’ hasn’t occurred yet.
(b) For some tool it seems that since the subroutine execute in Reactive region , the updated value of ‘b’ is sampled ( i.e immediate assertion executes in Reactive region ).
Although @( posedge clk ) unblocks in re-entrant Active region , the NBA update to b is already done

[3] In your code : edacode
As always_comb executes at T:0 we end up using the value updated at T:0 for m within the immediate assertion at the 1st clock edge.

 Hence there is No discrepancy in output across tools in this case as the immediate assertion executes in 1st iteration of Active region prior to NBA update ( unlike the immediate assertion called in subroutine which executes in Reactive region post NBA region update )

In reply to MICRO_91:

In reply to ben@SystemVerilog.us:
Verilog tells us that $display executes in Active region
[1] When does the $displays within the task execute ? Is it in Reactive region OR in Active region ( via loopback from Re-NBA to Active Region )
[ NOTE : There is No loopback directly from Reactive to Active Region ]

With @( posedge clk ) a |-> ( 1, dynamic_delay2( val ) );
the task is started in the Reactive region.
then task automatic dynamic_delay2( int cnt ); // Executes in Reactive Region
$display(" Within task b == %0d",b);

b== current value in current region.
I would think that since $display is a statement, it executes when it is seen.
This is not an assertion. You would need a $sampled(b) unless the assertion passes b
as an actual argument to the task.

[2] It seems that some tools use updated value of b : edalink
Hence to avoid the tool discrepancy I feel it’s better to use $sampled( b ) instead .

I didn’t analyze that code, but it might be a good discipline to use the $sampled.

Within the task when we write : repeat( cnt ) @( posedge clk );
@(posedge clk) executes in re-entrant Active region ( via loopback from Re-NBA to Active Region )
( However I believe the NBA assignment to b would execute before the loopback to Active region )
When we write the next statement as : assert(b);
(a) Are we still in Active Region ? i.e Non-blocking update to ‘b’ hasn’t occurred yet.

Yes. You have

repeat( cnt ) @( posedge clk );
     am_b: assert( b == 4 ); 

The tool is sensitive events. When an event occurs, you have regions for that even:
Active, NBA, Observed, Reactive, etc…
Thus, at the least repeat @( posedge clk ); you are now in the Active region.
am_b: assert( b == 4 ); // executes immediately. b has not changed yet, as you stated.

(b) For some tool it seems that since the subroutine execute in Reactive region , the updated value of ‘b’ is sampled ( i.e immediate assertion executes in Reactive region ).
Although @( posedge clk ) unblocks in re-entrant Active region , the NBA update to b is already done

If I had the following


 ... @( posedge clk )  a  |->  ( 1, dynamic_delay2( val ) );
task automatic dynamic_delay2( int cnt );  // Executes in Reactive Region
    am_cb: assert( $sampled(c) ); 
// **** am_cb assertion executes in the Reactive region, since it is upon entry
// and since immediate assertions executes in the place they are seen 
    if($sampled(c) && cnt > 0 ) begin      
       repeat( cnt ) @( posedge clk );
     am_b: assert( b == 4 )  // Discrepancy  here ?
// *** am_b executes in the Active region since @( posedge clk ) is the event 
// that causes the simulator to enter the various regions, with Active being the 1st one. 

[3] In your code : edacode
As always_comb executes at T:0 we end up using the value updated at T:0 for m within the immediate assertion at the 1st clock edge.
Hence there is No discrepancy in output across tools in this case as the immediate assertion executes in 1st iteration of Active region prior to NBA update ( unlike the immediate assertion called in subroutine which executes in Reactive region post NBA region update )

Looks correct.
Ben

In reply to ben@SystemVerilog.us:

Thanks Ben .

Thus, at the least repeat @( posedge clk ); you are now in the Active region.
am_b: assert( b == 4 ); // executes immediately. b has not changed yet, as you stated.

So although task gets called in Reactive region of time:5 , @(posedge clk) blocks at t:5
It’s unblocked in Active region of T:15,25,35,45 ( due to repeat( 4 ) @(posedge clk); )
As a result we are currently in Active region at T:45 , immediate assertion : am_b: assert( b == 4 ) , executes in Active region of T:45 .
NBA region is yet to occur at this point .

In reply to MICRO_91:
you are correct.
Hopefully, these regions should be transparent in thesense that a user should not have to worry about regions. Just follow good coding styles.

always #(posedge clk) a=b; // BAD STYLE 
always #(posedge clk) a<=b; // Good style
always_comb c=!a; // can execute in Activ region if a changes in same time 
                  // event @(posedge clk) 
 initial forever #1 clk = !clk ;
always #(posedge clk) am_c: assert(c); // an immediate asn in always
// in tb
initial begin 
#2 a=1; // same time as @(posedge clk) 
// can cause issues in am_c assertion
#2 a=0;
@(posedge clk) a <=1; //  Good style. 
// Make assignments to signals nonblocking

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog