Hi Doron, I think the sentence "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." might just exhaust the power of comprehension of the intended audience. I rewrote my suggested replacement to better reflect the informal semantic explanation in the paragraph above this. Also I don't think we need to give a separate explanation for the property sequence_expr since that is defaulting to either strong(sequence_expr) or weak(sequence_expr) as the case may be. 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. Similarly 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. The reason is that a finite prefix of a trace vitnesses a non-match of a sequence_expr if and only if it vitnesses a non-match of the first_match of that sequence_expr. Best Regards, Johan On Wed, Nov 28, 2007 at 02:03:00PM +0200, Bustan, Doron wrote: > > 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. -- ------------------------------------------------------------ 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.Received on Wed Nov 28 05:55:11 2007
This archive was generated by hypermail 2.1.8 : Wed Nov 28 2007 - 05:55:23 PST