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.