SVA: Implementing Dynamic Delay using procedural Immediate assertion

SystemVerilog
, ,
1

Hi All,
For practice reasons I was trying to implement dynamic delay in SVA using immediate assertion embedded within always procedural block.
The intention is to implement ::
$fell(rd_) |-> ##( readLatency ) ( read_data == expected_data );
where ‘readLatency’ is essentially a run-time variable.

Here is my attempt :: edaplayground

I have 2 questions

(Q1) Shouldn’t $fell( rd_ ) infer the clocking event from always procedural block ?
Out of the 3 tools that I tried the code on, 2 throw a compilation Error

LRM 16.9.3 Sampled value functions mentions ::

For a sampled value function other than $sampled, the clocking event shall be explicitly specified as an argument or inferred from the code where the function is called. The following rules are used to infer the
clocking event:
— If called in an assertion, sequence, or property, the appropriate clocking event as determined by
clock flow rules (see 16.13.3) is used.
— Otherwise, if called in a disable condition or a clock expression in an assertion, sequence, or
property, it shall be explicitly clocked.
— Otherwise, if called in an action block of an assertion, the leading clock of the assertion is used.
— Otherwise, if called in a procedure, the inferred clock, if any, from the procedural context (see
16.14.6) is used.

(a) Doesn’t the last line confirm the same ?

A work-around for the tools throwing the compilation error is to mention the clocking event explicitly i.e

 always @(posedge clk) begin
    if( $fell(rd_) , @(posedge clk) ) begin // Clocking event explicitly specified
    ....

(Q2) For the 5th case i.e +define+M5, why does the assertion pass ?
The immediate assertion uses the updated values for ‘read_data’ & ‘expected_data’.
Shouldn’t it take the preponed values leading to assertion failure at time:5 units ?

2

A1) clock inferencing only occurs within the context of a concurrent assertion (see 16.14.6). That last line refers to a function called as part of the evaluation of the assertion.

A2) Immediate assertions do not use sampled values. You have a race condition between the always block and initial block. Use NBAs in your initial block.

3

Thanks Dave.
So the sampled value function should be part of procedural concurrent assertion for clock inference.

I tested $fell(rd_) |=> $rose(rd_) using procedural concurrent assertion.
Both of the following work across all EDA tools.

always@(posedge clk) begin    
    ap1:assert property( $fell(rd_) |=> $rose(rd_) ) $display("T:%0t ap1 Pass",$time);
                                                else $display("T:%0t ap1 Fails",$time);    
end    
  
always@(posedge clk) begin    
    if( $fell(rd_) ) // Infers clock although it isn't written within 'assert property' !!
      ap2:assert property( 1 |=> $rose(rd_) ) $display("T:%0t ap2 Pass",$time);
                                         else $display("T:%0t ap2 Fails",$time);    
end

I find it it Interesting that for the 2nd always block, tools are able to interpret that $fell(rd) is part of the antecedent ( as a result $fell(rd_) infers the clock from always block )

4

For dynamic delays and repeats, see
SVA Package: Dynamic and range delays and repeats
SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy Provides a library and model solutions
See example at:
Need help in coding an assertion - #2 by ben2

Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf

5

Hi Dave,
A question related to the above discussion

module tb;
  // Code 1
   bit   rd_ = 1 , clk ;
  always  #5  clk = !clk ;

  initial begin
    #30 rd_ = 0;
    #10 $finish(); 
  end  
  
  always @(posedge clk) begin
    if( $fell(rd_) ) begin
      $display("T:%0t $fell(rd_) is True",$time);
    end
  end 
endmodule

I observe that this code compiles across all eda tools with output as :: T:35 $fell(rd_) is True

On changing the always block to ::

// Code 2
always @(posedge clk) begin
    if( $fell(rd_) ) begin
      #0 ; // Added a delay
      $display("T:%0t $fell(rd_) is True",$time);
    end
  end

I observe that one of the tools throws a compilation error (similar to the code at the top of this thread) “Clock for sampled value function $fell could not be resolved”

As per LRM Section 16.9.3 ::

For a sampled value function other than $sampled, the clocking event shall be explicitly specified as an argument or inferred from the code where the function is called. The following rules are used to infer the clocking event:
– Otherwise, if called in a procedure, the inferred clock, if any, from the procedural context (see16.14.6) is used.

LRM Section 16.14.6 further mentions ::

A clock shall be inferred for the context of an always or initial procedure that satisfies the following requirements:
a) There is no blocking timing control in the procedure.
b) There is exactly one event control in the procedure.
c) One and only one event expression within the event control of the procedure …

Due to #0, $fell in Code2 violates (a) and is unable to infer the clocking event from always procedural block
Whereas in Code1 all the above pts (a),(b),(c) were being satisfied.
Hence Code1 was treated as legal

Is my interpretation of the above LRM quotes correct ?

NOTE :: Code 2 is legal in presence of default clocking block

1 Like
6

Your interpretation of the LRM is correct. However, it appears that most tools adhere to conventional synthesis coding styles and disregard the timing controls.

1 Like