Asynchronous Stable Signal SVA

In reply to ben@SystemVerilog.us:

Hello,

Thank you for this insight. After testing in simulation, it appears to work as desired.

    initial begin
        sig = '0;
        rst = '1;
        #10;
        sig = '1;
        rst = '0;
        #20;
        sig = '0;
        #5;
        rst = '1;
        sig = '1;
        #10;
        rst = '0;

    end

    always @(rst)  begin
        #1 rst_stretch = 1;
        #1 rst_stretch = 0;
    end
    always @(sig)  begin
        #1 sig_stretch = 1;
        #1 sig_stretch = 0; 
    end
      
    am_sig: assert #0 (!(sig_stretch && !rst_stretch));

Are you aware of a way to get the same functionality to work in a formal application rather than in simulation? In the solution you shared it is still dependent on the timescale of the testbench.