RE: [sv-ac] implication operator on finite path

Hi Daniel:

In your example, an evaluation attempt of an assertion that is in the process of matching the antecedent, but has not completed match, at the end of simulation has the following dispositions:


1.       It is satisfied weakly and neutrally, but not strongly.  See F.5.3.1, F.5.3.2.

2.       It is said to “hold (but not strongly)” in .  See F.5.3.2.

3.       It is not non-vacuous.  See F.5.3.3.

Thus, it is correct for a tool to say that the attempt is a “vacuous pass” and for a tool to say that the assertion “holds (but not strongly)”.  It makes no difference what the consequent property is, weak or strong.

You mention “strong on the LHS” and ask whether such can be a future obligation.  The antecedent of |-> or |=> is always evaluated in a weak sense and does not produce a future obligation.  Contrast this with the antecedent of dual operators #-# or #=#, which is evaluated in a strong sense and can produce future obligations.

Regarding the question of exactly when a future obligation comes in force for |-> or |=>, it is at the point where evaluation of the consequent begins.   The existence of that point is not required by |-> or |=> (i.e., existence of that point is treated weakly).  In particular, after the match of the antecedent, the extra time advance specified by |=> is treated weakly – if simulation ends before getting to the point where evaluation of the consequent (even a strong consequent) should begin, then the result is “vacuous pass” and “holds (but not strongly)”.

Best regards,

John Havlicek

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Daniel Mlynek
Sent: Tuesday, December 18, 2012 7:05 AM
To: sv-ac@eda-stds.org
Subject: [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<http://www.mailscanner.info/>, and is
believed to be clean.

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