I wrote the following paragraph, "Given a simulation run w, a sequence s may have multiple matches over prefixes of w. Furthermore, even if there is no prefix of w that matches s, it could be that every prefix has the potential to match s in the future in multiple ways. Once considered a property, s, strong(s) and weak(s) are evaluated to true or false. The multiplicity of the matches/potential matches beyond whether there exists one, does not effect the evaluation. Therefore, 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." What do you think? Doron >>-----Original Message----- >>From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On >>Behalf Of Eduard Cerny >>Sent: Wednesday, November 21, 2007 3:46 PM >>To: john.havlicek@freescale.com; Eduard.Cerny@synopsys.com >>Cc: johan.martensson@jasper-da.com; sv-ac@server.eda.org; Bustan, Doron >>Subject: 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. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Nov 28 04:03:33 2007
This archive was generated by hypermail 2.1.8 : Wed Nov 28 2007 - 04:04:00 PST