Reply: SVA .clock and resets are deasserted synchronously

SystemVerilog
1 
// The problem in verifying that reset_n is synchronous to the clock is 
    // is that with something like 
     always   @(posedge clk) if(clear_reset) reset_n <= 1'b1; 
    // reset_n is assigned in the NBA region, but 
    // read in the Active region, and in an assertion it is read in the Preponed region.
   
    // One option is to evaluate the reset_n with a small acceptable delay (like #0).  Thus, 
    always @(posedge clk) 
        if(clear_reset) #1 p_reset0: assert(reset_n == 1'b1);

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/