RE: [sv-ac] triggering of action blocks.

Hi John,

It's been a long time since I thought carefully on this as well (way back Cindy and I had lots of discussion about this. At the end we decided to abandon this because it seems giving semantics to action blocks limits the implementation - as in the examples you give in the document, if we choose one approach we restrict implementation to follow it, whereas in the absence of action blocks an implementation following the other approach is valid as well. We may reach that conclusion again. But perhaps not. If we found a semantic definition, I wouldn't feel too bad about restricting implementation.)

To the matter, I think it is a good idea to look at the example. Let's start with the two you give here.

Let's put some flesh on the example

R |-> S or T

Say
    S is (a ##1 (b, \alpha)[*0:$] ##1 c),
    T is (d ##1 (e, \beta) ##1 f) and
    R is r.
Consider the word <rad><be><b><b><b><b><c>.
[The notation <xy> says that xy hold in the letter and all other propositions do not.]
Thus S hold and T does not.
Then we would expect \alpha to be triggered on the 2nd to 6th letter, and \beta to be triggered on the second letter, and the proposed definition will give us that.
Now consider the word <rad><be><bf><b><b><b>. Here T holds and S may hold as well. The proposed definition will give us that \beta is triggered on the second letter and \alpha is triggered only on the 2nd and 3rd letters. So it is the tight approach as you put it, and you say the loose approach makes sense here since the success of S should not stop the evaluation of T and vice versa. But I think this does makes sense. Note that regardless of action blocks, a tool would give us only the prefix <rad><be><bf> as a witness for the pass. (you would not complain about that, right?) It is not that S is ignored because of the success of T it just means that the evaluation is stopped when success is determined and thus so does the entailed triggering.

Now let's look at

   (R, \alpha) #-# P

Say R is (a ##1 b) or (c ##1 d) and P is (d && !b ##1 e).
Consider the following words
<ac><bd>
<ac><b>
<ac><d>
All are matches of R, but only the 3rd allows a match of P. What does the proposed definition give us? If we read "a prefix of the definitive prefix" as "a (not necessarily proper) prefix of the definitive prefix" then \alpha should be triggered in all. Since the first two are the definitive prefix (and the third is a prefix of the definitive prefix). Reading it as "a proper prefix" does not make sense in case the formula holds, so we can think of a definition that requires proper prefixes for bad definitive prefixes (i.e. in case the formula is found to fail) and not necessarily proper prefixes for good definitive prefixes (i.e. in case the formula was found to hold). Under such a definition \alpha will be triggered only on the third word. Which matches the intuition better? I am not sure...

Dana

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Thursday, June 24, 2010 10:46 PM
To: Dana Fisman; Eduard Cerny; sv-ac@server.eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] triggering of action blocks.

Hi Dana:

It's been a long time since I thought carefully about this problem.

What you are proposing is interesting and it strikes me as similar to the "tight" approach described in the documents for Mantis 921. We had suggested that the "loose" approach be applied to properties because they do not join, with the exception of the top-level properties. This seems to be what the definitive prefix approach is capturing.

One thing that always bothered me was that there seemed to be some examples where we want the "tight" approach and some where we want the "loose" approach. E.g., in

   R |-> S or T

It seemed that we wanted to let S and T evaluate independently, so that if one finished successfully first it would not stop the other. But this is not the "tight" approach, so there was some inconsistency in what we suggested in those documents.

I suppose I would be happier if I could convince myself that applying definitive prefix at the top level works well in practice.

Another twist on the problem described in Mantis 921 is the question of multiplicity and multithreading. E.g., I am not sure what to do about

   (R, \alpha) #-# P

Some matches of R (and the associated local variable valuations) may enable P to succeed and some may not. At the point that R matches, though, a simulator will have to decide whether or not to execute \alpha. This is not a question that is answered by the semantics:

   w,L_0 |= (R,\alpha) #-# P

provided there exists 0 <= k < |w| and L_1 such that w^{0..k},L_0,L_1 |== R and w^{k..},L_1 |= P.

I would be interested to hear your feedback on the examples given in the documents on Mantis 921. I also have not yet looked back through the document on Mantis 1502.

J.H.

From: Dana Fisman [mailto:Dana.Fisman@synopsys.com]
Sent: Thursday, June 17, 2010 4:49 AM
To: Havlicek John-R8AAAU; Eduard Cerny; Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] triggering of action blocks.

Hi John, Ed,

For the two problems (triggering of action blocks and triggering of subroutines attached to sequences execute) I think we should first ask ourselves what is the intuition the semantics should capture. Once we answered that we can ask how to device algorithms to make that happen, and what are the complexity of those. But deciding about the semantics on the base of current implementations of certain tools does not make sense.

In other words, I would be happy if we can come up with a semantic definition that captures the intuition. Once we have it, if we can come up with an equivalent syntactic definition - this would be great. This way we enjoy that (1) the equivalence between the two definitions strengthens that we have captures the intuition correctly (2) the syntactic definition entails an algorithm for certain tools and (3) if a new operator is added to the language the semantic definition already gives it semantics and it is only left to come up with a syntactic definition for that operator that adheres to the semantic definition.

That said, allow me to make a first try for a semantic definition of when a subroutine attached to a sequence should be executed. I am assuming here subroutines do not have side effects (e.g. $display()).

Let P be a property with subroutine \alpha. Let w be a word.

Let v_\alpha be a fresh local variable over a Boolean domain.

Let P' be the property obtained by replacing every occurrence of \alpha with the assignment v_\alpha <= !v_\alpha (i.e. flipping the value of \alpha).

What is wrong with the following definition:

\alpha should be triggered on every point k <= |w| such that

w(0..k) is a prefix of the definitive prefix of P' on w

and the value of v_\alpha in the last letter w(k) is different than its value in the preceding letter w(k-1).

?

Recall that, loosely speaking, the definitive prefix of P on w is the shortest prefix of w in which one can say for sure that P holds or does not hold on w.

Dana

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Wednesday, June 16, 2010 6:22 PM
To: Eduard Cerny; Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] triggering of action blocks.

Hi Ed:

So how does the automaton account for aborts? E.g.,

   sync_accept_on (ab)
   precondition |-> (a[*2], $display("foo")) and (1[*] ##1 false)

?

J.H.

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Eduard Cerny
Sent: Wednesday, June 16, 2010 9:17 AM
To: Havlicek John-R8AAAU; Eduard Cerny; Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] triggering of action blocks.
Hi John,

but one may be using the same automaton as in formal for simulation, e.g., for reasons of speed of evaluation.

ed

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Wednesday, June 16, 2010 10:11 AM
To: Eduard Cerny; Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] triggering of action blocks.

Hi Ed:

I understand your point. An extreme example is something like

   (a[*2], $display("foo")) and (1[*] ##1 false)

where an optimized automaton could be empty. However, the language has aborts already, and those can prevent this sort of optimization at the property level.

I would be happy to come up with a precise definition that works well in practice for simulation, but allow deviation for other verification flows (e.g., formal).

J.H.

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Eduard Cerny
Sent: Wednesday, June 16, 2010 9:03 AM
To: Havlicek John-R8AAAU; Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry; Eduard Cerny
Subject: RE: [sv-ac] triggering of action blocks.
Hi John,

for the sequence match items, it may be difficult to enforce one or the other, it depends how the sequence is evaluated, syntactically or as an automaton (possibly optimized).

ed

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Wednesday, June 16, 2010 10:02 AM
To: Dana Fisman; sv-ac@server.eda.org
Cc: Korchemny, Dmitry; Eduard Cerny
Subject: RE: [sv-ac] triggering of action blocks.

Hi Dana:

See also Mantis 0921 on making precise when subroutines attached to sequences execute. It is similar to, but not the same as, the problem for action blocks.

It may be that a semantic approach works better for action blocks, while a syntactic approach works better for subroutines attached to sequences.

A question that was never really decided was whether the policy for subroutines should be liberal or conservative, or allow both, with some controls to specify when a liberal or conservative policy applies.

J.H.

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dana Fisman
Sent: Thursday, June 03, 2010 4:52 AM
To: sv-ac@server.eda.org
Cc: Korchemny, Dmitry; Eduard Cerny
Subject: [sv-ac] triggering of action blocks.
 Hi all,

I added a comment to mantis item 1509. (This follows a mantis item 3099 I opened before Dmitry pointed me to this one. Here you can see properties exemplifying the problem.)

The issue is that the LRM does not define when an action block should be triggered. Doron and Dmitry proposed a syntactic definition (that is a definition based on the structure of the assertion). I commented that we can use a semantic definition as per the paper [EFHLMV03]. I believe that even if we would like to have the syntactic definition, we can benefit by comparing the two.

Regardless, we should decide about the cases where there is no point to trigger the fail/pass action block statements. Should this be allowed or not?

Best regards,
Dana

1509: http://www.eda-twiki.org/mantis/view.php?id=1502
3099: http://www.eda-twiki.org/mantis/view.php?id=3099
[EFHLMV03]: Cindy Eisner<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/e/Eisner:Cindy.html>, Dana Fisman, John Havlicek<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Havlicek:John.html>, Yoad Lustig<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/l/Lustig:Yoad.html>, Anthony McIsaac<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/m/McIsaac:Anthony.html>, David Van Campenhout<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/c/Campenhout:David_Van.html>: Reasoning with Temporal Logic on Truncated Paths. CAV 2003<http://www.informatik.uni-trier.de/~ley/db/conf/cav/cav2003.html#EisnerFHLMC03>: 27-39

--
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<http://www.mailscanner.info/>, and is
believed to be clean.
--
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.