Re: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata.

Yes that makes sense, but the way it was written have the impression that fail of first match is different.

Ed

Sent from BlackBerry.


----- Original Message -----
From: John Havlicek <john.havlicek@freescale.com>
To: Eduard.Cerny@synopsys.COM <Eduard.Cerny@synopsys.COM>
Cc: johan.martensson@jasper-da.com <johan.martensson@jasper-da.com>; sv-ac@eda.org <sv-ac@eda.org>; doron.bustan@intel.com <doron.bustan@intel.com>
Sent: Wed Nov 21 05:16:44 2007
Subject: Re: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata.

Hi Ed:

I interpret this to be saying that if a finite trace has enough
information to demonstrate that no match of R is possible, then that
same trace has enough information to demonstrate that no match of
first_match(R) is possible.

J.H.


> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 20 Nov 2007 17:27:03 -0800
> Thread-Topic: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata.
> thread-index: AcgrkWQ4yR/LEDzMSkW9N23q933ntwASIF4g
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> X-OriginalArrivalTime: 21 Nov 2007 01:27:03.0313 (UTC) FILETIME=[9EDD5010:01C82BDD]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id lAL1RJkl001238
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> Hello Johan,
> 
> You wrote " It is also the case that a finite prefix of a trace contradicts a
>  sequence_expr if and only if it contradicts the first_match of that
>  sequence_expr." But what is the difference between "contradicting the first_match or that sequence expression" and   contradicting any match of the sequence_expression"? Since there is no first mathc there is no match at all.
> 
> Thanks,
> ed
> 
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> > Behalf Of Johan Martensson
> > Sent: Tuesday, November 20, 2007 11:20 AM
> > To: sv-ac@eda.org; Bustan, Doron
> > Subject: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata.
> > 
> > Hi Doron,
> > 
> > some problems I found in LTL.1932.20071114.pdf
> > 
> > 16.12. (The paragraph beginning with: "The result of property 
> > evaluation is either true or false.")
> > ======
> > 
> > There are lots of problems with this paragraph.
> > 
> > 1) There are now boolean operators for implication and equivalence
> > ('implies' and 'iff') which should perhaps be mentioned together with 
> > negation, disjunction and conjunction.
> > 1) I think there should be dots, not hyphen between 'if' and 'else'. 
> > 2) There should be a comma between 'strong' and 'accept_on'. 
> > 3) 'and' between 'until' and 'eventually' should have different font
> > from that of the operators.
> > 4) 'implication' and 'followed_by' are not operators and should maybe
> > have different font from that of the operators 'weak', 'strong' etc.
> > 5) Maybe the strong variants of next, until, always and 
> > eventually, and the
> > _with variants of until and s_until should also be listed.
> > 
> > 1, 4 and 5 above point to a related set of problems with this 
> > paragraph:
> > Should we list all the different operators here or should we use the
> > grouping provieded by the various following subsections
> > 16.12.2-16.12.16. It seems there is no uniform principle of reference
> > chosen in this paragraph.
> > 
> > Table 16.25
> > ===========
> > 
> > The operators 'throughout', 'within', 'intersect', 'and' 
> > 'or', 'implies'
> > and 'iff' are written with a initial capital letter.
> > 
> > The operators 'implies' and 'iff' are rendered with different 
> > font from
> > the others..
> > 
> > 16.12.1 Sequence property
> > =========================
> > (The paragraph beginning with "Since only one match is 
> > needed, properties 
> > ...")
> > 
> > This paragraph is a little strange. The discription seems to apply
> > to strong embedding of sequences. For weak embedding not even 
> > one match
> > of the sequence is required.
> > 
> > If we decide to keep this section maybe it should be split in 
> > two giving
> > different explanations for the weak and strong case respectively.
> > 
> > REPLACE
> >  Since only one match is needed, properties of the form sequence_expr,
> >  (weak(sequence_expr)), and (strong(sequence_expr)) are evaluated to
> >  true if and only if the properties first_match(sequence_expr),
> >  (weak(first_match(sequence_expr))) and
> >  (strong(first_match(sequence_expr))) are evaluated to true
> >  respectively.  As soon as a match of sequence_expr is determined, the
> >  evaluation of the property is considered to be true, and no other
> > WITH 
> >  Since for strong(sequence_expr) only one match is needed, 
> > properties of
> >  this form are evaluated to true if and only if the corresponding
> >  properties of the form (strong(first_match(sequence_expr))) are
> >  evaluated to true respectively.  As soon as a match of 
> > sequence_expr is
> >  determined, the evaluation of the property is considered to be true,
> >  and no other matches are required for that evaluation attempt.
> > 
> >  It is also the case that a finite prefix of a trace contradicts a
> >  sequence_expr if and only if it contradicts the first_match of that
> >  sequence_expr. Hence properties of the form weak(sequence_expr) are
> >  evaluated to true if and only if the corresponding properties of the
> >  form (weak(first_match(sequence_expr))) are evaluated to true
> >  respectively.
> > 
> > 16.12.1-16.12.16
> > ================
> > 
> > The headings of these sequences don't seem to be uniformly 
> > capitalized,
> > for example 16.2.10 has initial capital in "Next property" but 16.2.11
> > has "always property". 
> > 
> > These headings seem to serve the purpose of naming different operator
> > groups. For example an until property has one of the operators until,
> > until_with, s_until or s_until_with as its top level 
> > operator. Maybe we
> > should define explicit corresponding operator groups for use 
> > for examples in
> > the section under 16.12 discussed above.
> > 
> > This review was only partial, for this time :-(.
> > 
> > Regards,
> > 
> > Johan M
> > 
> > On Wed, Nov 07, 2007 at 11:38:31AM +0100, Johan Martensson wrote:
> > > Hi Doron,
> > > 
> > > some further errors I found in LTL.1932.20071030.pdf
> > > 
> > > 16.12. (The paragraph beginning with: The result of 
> > property evaluation
> > > is either true or false.)
> > > 
> > > REPLACE (dot after always, should be comma, no comman after 
> > followed by,
> > > and between accept_on and reject_on should not be bold.)
> > > 
> > > The result of property evaluation is either true or false. 
> > Properties
> > > may be built from other properties or sequences using instantiation,
> > > boolean operators (negation, disjunction, conjunction, if...else,
> > > implication, followed_by weak, strong and iff) and temporal 
> > operators
> > > (next, always. until, eventually, accept_on and reject_on) 
> > described in
> > > the following subclauses.
> > > 
> > > WITH
> > > The result of property evaluation is either true or false. 
> > Properties
> > > may be built from other properties or sequences using instantiation,
> > > boolean operators (negation, disjunction, conjunction, if...else,
> > > implication, followed_by, weak, strong and iff) and 
> > temporal operators
> > > (next, always, until, eventually, accept_on and reject_on) 
> > described in
> > > the following subclauses.
> > > 
> > > 
> > > 
> > > 16.12.9 followed_by property 
> > > 
> > > REPLACE (I don't think proceed is the right word here)
> > > The followed_by construct specifies that the checking of a 
> > property is
> > > required to proceed a match of a sequential antecedent
> > > WITH
> > > The followed_by construct specifies that the checking of a 
> > property is
> > > required to be preceded by a match of a sequential antecedent
> > > 
> > > REPLACE (followed => followed_by, "at the end point of the match" =>
> > > "the end point of this match")
> > > Two forms of followed_by are provided: overlapped using 
> > operator #-# and
> > > nonoverlapped using operator #=#. For overlapped followed, 
> > there shall
> > > be a match for the antecedent sequence_expr, where at the 
> > end point of
> > > the match is the start point of the evaluation of the consequent
> > > property_expr. For nonoverlapped followed_by, the start point of the
> > > evaluation of the consequent property_expr is the clock 
> > tick after the
> > > end point of the match.
> > > WITH
> > > Two forms of followed_by are provided: overlapped using 
> > operator #-# and
> > > nonoverlapped using operator #=#. For overlapped 
> > followed_by, there shall
> > > be a match for the antecedent sequence_expr, where the end point of
> > > this match is the start point of the evaluation of the consequent
> > > property_expr. For nonoverlapped followed_by, the start point of the
> > > evaluation of the consequent property_expr is the clock 
> > tick after the
> > > end point of the match.
> > > 
> > > REPLACE (remove ##1 in two places)
> > > The followed_by operators are the duals of the implication 
> > operators.
> > > Therefore, sequence_expr #-# property_expr is equivalent to 
> > the following: 
> > > 
> > > not sequence_expr ##1 1 |-> not property_expr 
> > > 
> > > and sequence_expr #=# property_expr is equivalent to the following: 
> > > 
> > > not sequence_expr ##1 1 |=> not property_expr
> > > WITH
> > > The followed_by operators are the duals of the implication 
> > operators.
> > > Therefore, sequence_expr #-# property_expr is equivalent to 
> > the following: 
> > > 
> > > not sequence_expr |-> not property_expr 
> > > 
> > > and sequence_expr #=# property_expr is equivalent to the following: 
> > > 
> > > not sequence_expr |=> not property_expr
> > > 
> > > 16.12.10
> > > 
> > > REPLACE (expression => const_expression, constants => 
> > const_expression,
> > > constant_expression => const_expression)
> > > Weak next property evaluates to true if property_expr holds 
> > at the next
> > > clock tick or if there are no further clock ticks. To 
> > require the clock
> > > tick to occur, use the strong form s_next property_expr. Weak next
> > > property with expression evaluates to true if property_expr 
> > holds in the
> > > specified of future clock ticks indicated by the constants, 
> > or if there
> > > are not enough clock ticks for the property to complete the 
> > evaluation.
> > > To require the necessary clock ticks to occur use the 
> > strong form s_next
> > > [constant_expression] property_expr.
> > > WITH
> > > Weak next property evaluates to true if property_expr holds 
> > at the next
> > > clock tick or if there are no further clock ticks. To 
> > require the clock
> > > tick to occur, use the strong form s_next property_expr. Weak next
> > > property with const_expression evaluates to true if 
> > property_expr holds in the
> > > specified of future clock ticks indicated by the 
> > const_expression, or if there
> > > are not enough clock ticks for the property to complete the 
> > evaluation.
> > > To require the necessary clock ticks to occur use the 
> > strong form s_next
> > > [const_expression] property_expr.
> > > 
> > > I just read to this poin this time. Hopefully I get some 
> > time to read
> > > the rest.
> > > 
> > > Best Regards,
> > > 
> > > Johan
> > > 
> > > 
> > > -- 
> > > ------------------------------------------------------------
> > > Johan Mårtensson                 Office: +46 31 7451913
> > > Jasper Design Automation         Mobile: +46 703749681 
> > > Arvid Hedvalls backe 4           Fax: +46 31 7451939
> > > 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> > > ------------------------------------------------------------
> > 
> > -- 
> > ------------------------------------------------------------
> > Johan Mårtensson                 Office: +46 31 7451913
> > Jasper Design Automation         Mobile: +46 703749681 
> > Arvid Hedvalls backe 4           Fax: +46 31 7451939
> > 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> > ------------------------------------------------------------
> > 
> > 
> > -- 
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> > 
> > 
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 

-- This message has been scanned for viruses anddangerous content by MailScanner, and isbelieved to be clean.