Overlap between the two asynchronous reset signals

[Redfoo]

I need assertions about 2 asynchronous reset signal,they will be set at rtl module(verilog),two signals’ reset must has an overlap,so there will be 6 permitted situations or more,3 of them are below,the other 3 are src and dst signals swapped.I believe Immediate Assertions must be used since there is no clk,and the flag logic added,but I cannot handle it.

[ben2]

I really do not understand your requirements, but you can use this type of template to design your VF code. Essentially, you fire an autimatic task upon the detect of edges and values of “cond” that provides info about past history.
Then you test whiuchh edge can me first or last and write an immediate assertion.

module m;
  bit a, b;
  bit[2:0] cond, stat;

  task automatic ta_falls();  // afall, then bfall brise arise 
     bit stat0, stat1;
    fork
       begin
           @(negedge b) stat0=1;
       end

       begin 
        @(posedge b( stat0=1;
       end
    join_any
    // based on set status bit do something 
    cond=2;
    am_label: assert (stat==stat0);
  endtask

  always @(negedge a) if(cond==1) ta_falls();



  endmodule

let me know how thius would work for you

[Redfoo]

Sorry for my poor expression，and thanks for your generous help，ben！
I saw your fork join_any magic,and I wrote my solution base on yours below.

module m;
  bit src_rst_n,dst_rst_n;

  task automatic t_src_falls();  
    bit dst_rst_n_fell_before_src_rst_n_rose = 0;
    fork
       begin
           @(negedge dst_rst_n) dst_rst_n_fell_before_src_rst_n_rose=1;
       End

       begin 
        	@(posedge src_rst_n) dst_rst_n_fell_before_src_rst_n_rose=0;
       end
    join_any
    // based on set status bit do something 
must_fell: assert(dst_rst_n_fell_before_src_rst_n_rose == 1);
must_an_overlap_1_timeslot:assert final(dst_rst_n_fell_before_src_rst_n_rose == 1);
  endtask


task automatic t_dst_falls();  
    bit src_rst_n_fell_before_dst_rst_n_rose = 0;
    fork
       begin
           @(negedge src_rst_n) src_rst_n_fell_before_dst_rst_n_rose =1;
       End

       begin 
        	@(posedge dst_rst_n) src_rst_n_fell_before_dst_rst_n_rose =0;
       end
    join_any
    // based on set status bit do something 
must_fell: assert(src_rst_n_fell_before_dst_rst_n_rose == 1);
must_an_overlap_1_timeslot:assert final(src_rst_n_fell_before_dst_rst_n_rose == 1);
  endtask

  always @(negedge src_rst_n) if(dst_rst_n) t_src_falls();
 always @(negedge dst_rst_n) if(src_rst_n) t_dst_falls();

Did I missing anything else?Did I do something wrong?I guess there are more things in your code I did not realize.
And also , did I use deferred assertion correctly? I wanna assert there will be 1 timeslot longer overlap between two signals.

[ben2]

1. Need to consider the case where @(negedge src_rst_n) and @(posedge dst_rst_n) occur at the same time point. Same Q for the other case.
   Sothing like:
   must_fell: assert(src_rst_n_fell_before_dst_rst_n_rose == 1 &&
   dst_rst_n==0:

2. You don’t need assert final.
   per Understanding and Using Immediate Assertions
   Understanding and Using Immediate Assertions
   Provides guidelines
   Final deferred immediate assertions recommendation: Use final deferred immediate assertions when variables used in the immediate assertion are either driven in any action block or driven in a program block.

3. For documentation: Write the requirements in English.
   Clarify them with AI (e.g., perplexity.ai
   Something like: Fix the English and style. Clarify, tell me what is implied and what is missing from the requirements

[Redfoo]

Thanks for your guidance！
My requirements completed：
1.Two input signals from different clock domain,src_rst_n and dst_rst_n,any clock frequency and phase for each is possible.
2.Each reset signal requires at least one timeslot for its reset action. (1->0->1).
3.When one of them reset, the other must also do reset action，which means their reset pulses must overlap by at least one timeslot.