Synchronous assertion to check asynchronous reset

Hi,

I want to do SVA checking on an asynchronous reset signal, if the reset is asserted the en signal must be 0 from the past 10 clock cycles before.

property(@(posedge clk) $fell(reset) |-> ($past(en,10) == 0));

The problem with the above snippet is the checking only happens on posedge of the clk but the reset is asynchronous which asserted non dependent to the clk. But the $past syntax wouldn’t have any clock reference if I didn’t put the clk.

Other than that, I believe this kind of way will affect the simulation performance.

If you guys have better way to suggest feel free to respond. Thanks in advance.

In reply to musyantsa:

  1. You can use the endpoint for en==0 for 10 cycles.
  2. First Synchronize the sync
    Edit code - EDA Playground

module m; 
  bit en, reset_sync, reset, clk; 
  sequence s_en; 
    @(posedge clk) en==0[*10];
  endsequence
    
  ap_reset_en: assert property(@(posedge clk) $fell(reset) |-> s_en.triggered);
    
  // Option: 1st synchonize the reset
  always @(posedge clk) reset_sync <= reset; 
  
  // Use en==0 for 10 clocks starting from the synced reset
  // Thus, you get 10+ clocks from the async reset
   ap_resetsync__en: assert property(@(posedge clk) $fell(reset_sync) |->
                                                   s_en.triggered);
endmodule

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:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.