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

Hi Daniel:

I can think of “vacuous pass” and “holds (but not strongly)” as predicates over an evaluation.  Both can be true, as they are in your example.  For the purpose of determining the action block execution, the tool must pay attention to the “vacuous pass” predicate; the tool is not at liberty to ignore it.  In saying that both predicates are true, I did not mean to imply that a tool can ignore one or the other in some circumstance.

You are probably right that “neutral” is used only in Appendix F.  But when we say “holds, but not strongly”, this means “holds neutrally, but not strongly”.  And when we say “pending”, this means “holds weakly, but not neutrally”.  Neutral sits between strong and weak in the sense that


-          holds neutrally implies holds weakly

-          holds strongly implies holds neutrally

In the LRM we use neutral satisfaction and the special letters \top and \bot to define strong and weak satisfaction, but it is possible to define strong and weak satisfaction more directly – see

Cindy Eisner<http://dblp.dagstuhl.de/pers/hd/e/Eisner:Cindy.html>, Dana Fisman<http://dblp.dagstuhl.de/pers/hd/f/Fisman:Dana.html>, John Havlicek, Yoad Lustig<http://dblp.dagstuhl.de/pers/hd/l/Lustig:Yoad.html>, Anthony McIsaac<http://dblp.dagstuhl.de/pers/hd/m/McIsaac:Anthony.html>, David Van Campenhout<http://dblp.dagstuhl.de/pers/hd/c/Campenhout:David_Van.html>: Reasoning with Temporal Logic on Truncated Paths. CAV 2003<http://dblp.dagstuhl.de/db/conf/cav/cav2003.html#EisnerFHLMC03>: 27-39

Best regards,

John Havlicek

From: Daniel Mlynek [mailto:danielm@aldec.com.pl]
Sent: Wednesday, December 19, 2012 7:12 AM
To: John Havlicek
Cc: sv-ac@eda-stds.org
Subject: Re: [sv-ac] implication operator on finite path

Thank you for the response.

1.
As I understand for my example both are correct at endsim "vacucous pass"  and "hold (not strongly) in your opinion
If so then the problem is if action block should be executed. We can turn off action blocks for vacuous passes by $assertvacuousoff and then  action block should be called only if property passes non vacuously.
I think that we cannot say that both results are ok, if we can then we should defined which if action block should execute with assertvacuousoff.

2.
The term neutrally is used only in APPENDIX F. Is this neutral satisfaction used by some SV directive? LRM uses only strong and weak for cover and asssert directoves. Neutral is used only to in define strong and weak ?

3.
"You mention “strong on the LHS” ".....
I mean RHS here I was courious if strong on RHS can be a future obligation even it was not even started.
For |-> antecedent I would rather not use term weak/strong bcos it is a sequence - sequence cannot be strong or weak - only property can


DANiel
W dniu 12/18/2012 2:50 PM, John Havlicek pisze:
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> [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<mailto: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.