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, and is
believed to be clean.