Assertion to check Synchronous de-assertion

In reply to ben@SystemVerilog.us:

I am assuming that at the fell of rst_n the clk is running.

    Yes , the clk  would  be  running  throughout .

I am also assuming that by synchronous, you mean within acceptable bounds of a period.

    This  part  I  was  confused  about .

The requirement ( from AXI Spec ) was simply mentioned as “but deassertion must be synchronous after the rising edge of clock”

Ben have 2 follow-up questions ::

(1) The clocking - event written in assert property can be removed right ?

as @(posedge rst_n) in antecedent would override @(posedge clk) in assert property

(2) What if I were to write it as ::


     property p;
     realtime v;
     @(posedge clk) (1, v=$realtime)   // @( posedge clk ) written  First
     ##0  @(posedge rst_n) ($realtime - v) inside { [ min : max ] } ; 
   endproperty 

   ap_p: assert property( p );