[sv-ac] implication operator on finite path

What should be the results of assertion thread if we will finish at the 
moment when antecedent is in progress?
In such case at the end of simulation we should wave vacuous pass?
Or property should hold as LSH of |-> is weak (neutral)
Is there any different if RHS will be strong - can such strong on the 
LHS be a future obligation or it will become future obligation only at 
the moment when LHS success?

Here is example ilustrating my problem

    module top;
       bit a,b,c,d,clk;
       always #5 clk =  ~clk;

        initial begin
          @(posedge clk);
          a=0;b=0;c=0;d=0;
          @(posedge clk);
          a=0;b=0;c=0;d=0;
          @(posedge clk);
          a=1;b=0;c=0;d=0;
          @(posedge clk);#1;
          $finish;
        end

        as1:assert property (@(posedge clk) a ##1 b |=> c ##1 d);
        as2:assert property (@(posedge clk) a ##1 b |=> strong(c ##1 d));

    endmodule




DANiel

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.