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 )