Is it possible to verify, if the signal rose within a cycle in SVA?

Hi,

I have an async signal ‘b’ that should go high immediately as trigger ‘a’ goes high ideally.

i was thiking of using something simple like below overlapping implication.
property exp1:
@(posedge clk) a |-> b;
endproperty

But, due to back annotated(SDF timing) sims, there is a small gate delay.

Is it possible to verify if b went high after a hard delay from posedge clk.
OR
b went high within that clock cycle before next clock edge?

Appreciate any help.

In reply to Adarsh24:
Use an immediate deferred assertion


    always_comb if(a) am_1: assert final(b); 
    always_comb if(a) am_2: assert #0 (b); 

From 1800: Note that if code in the Reactive region modifies signals and causes another pass to the Active region to
occur, this still may create glitching behavior in observed deferred assertions, as the new passage in the
Active region may re-execute some of the deferred assertions with different reported results. In general,
observed deferred assertions prevent glitches due to order of procedural execution, but do not prevent
glitches caused by execution loops between regions that the assignments from the Reactive region may
cause.
In the Postponed region of each simulation time step, each pending final deferred assertion report that has
not been flushed from its queue shall mature. Then the associated subroutine call (or $error, if the assertion
fails and no action block is present) is scheduled in the same Postponed region, and the pending assertion
report is cleared from the appropriate process’s deferred assertion report queue. Due to their execution in the
non-iterative Postponed region, final deferred assertions are not vulnerable to the potential glitch behavior
previously described for observed deferred assertions

In reply to ben@SystemVerilog.us:

Thank you, Ben. Let me check and update the thread.

I dont think an assert final is going to work here since SDF timing delays the signal edge by actual time.

You can use a clock delay range operator to check for this.

@(posedge clk) a |-> ##[0:1] b;

Checks for b to go high starting from 0 all the way to 1 clock cycle.
assuming your delay isnt greater than 1 clock cycle.

In reply to maddy0812:

“async signal ‘b’ that should go high immediately as trigger ‘a’ goes high ideally”
Looks like ‘b’ is a buffered (delayed) version of ‘a’ which is the output of a flop.
The following @(posedge clk) a |-> ##[0:1] b;
does not “check for b to go high starting from 0 all the way to 1 clock cycle.
assuming your delay isnt greater than 1 clock cycle.”

It is not a continuous check. All it says is that in the Preponed Region, the sampled values of ‘a’ and ‘b’ have the same values in the current and next cycle.
‘b’ can glitch at any time between those sampled times.

The assertion is OK, if that is what you want.

In reply to ben@SystemVerilog.us:

Hi,

Sorry I couldn’t get a chance to try it out yet.

I don’t think Maddy’s check is what I initially wanted.
I want to make sure b goes high before the next clock edge. Not at the clock edge.

Ideally I want to check if b goes high immediately as a goes high.
Yes, a is a flop out and b is a delayed combo out of a.

This is not an actual problem I observed. Something that I was thinking about.

Im thinking this won’t be an issue since there will be clk-to-q delay and a will be checked at next edge anyway. By that time b will be high.
So by this logic I think Maddy’s suggestion will work.

In reply to Adarsh24:
Actually, you do not need any assertion here.
Signal ‘a’ is an output of flop with a hold delay.
Signal ‘b’ is a delayed combo out of ‘a’.
Thus, what you have is basically a wire with internal delays.
The concern is a setup and hold, and this is best done by using the system functions.


module setup_time_check(input clk, data); //  SystemVerilog.us/vf/hold.sv
    timeunit 1ns;  timeprecision 100ps;
    let tSU=2ns; 
    let tHLD=2ns;
    bit notifier1;
    specify
        $setuphold( posedge clk, data, tSU, tHLD, notifier1 );
    endspecify 
endmodule

module top2(output logic clk, d);
 realtime duration= 2.0ns;
   …
setup_time_check setup_time_check1(clk, d); // built in 1800 setup and hold 
// *** If you insist on using assertions, then assert those properties 
property hold_chk;
    realtime clock_sample;
    @(posedge clk) (1,clock_sample = $realtime) |-> 
       @(d) ($realtime - clock_sample) >= duration;
 endproperty : hold_chk

property setup_chk;
   realtime clock_sample;
   @(d) (1,clock_sample = $realtime) |-> 
   @(posedge clk) ($realtime - clock_sample) >= duration);
endproperty : setup_chk 

If you insist on using an assertion for your ‘a’ ‘b’ concern, then you can simply write


// +--+                                 +--+
// |FF|----a----(gate_delays)------b--->|FF|---c
// +--+                                 +--+
// at every clocking event the sampled value of 'a' == sampled value of 'b'
ap_ab: assert property(@ (posedge clk) a==b);  

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Thanks Ben. Makes sense.