Hi Ben: Sorry for the long delay in getting to this. There is no rule about operands of "and" or "or" having identical leading clocks. The rule is that a top-level property must have a unique semantic leading clock. If a property has "and" as its top-level operator, then this does require the operands to have the same semantic leading clock. However, if "and" is not the top-level operator, then there is no such requirement. E.g., the following is legal: assert property ( @(posedge clk0) a ##1 b |-> @(posedge clk1) prop1 and @(posedge clk2) prop2 ); J.H. > X-BigFish: vps-45(zf7Iz1432R9370P98dR936eQ1805M936fK9371P45c8szz2cfT1202h10dco10adjzz5a6ciz2fh5eh6bh5fh61h) > X-Spam-TCS-SCL: 0:0 > X-FB-SS: 5,5, > X-MS-Exchange-Organization-Antispam-Report: OrigIP: 171.67.73.10;Service: EHS > X-eda.org-MailScanner-Watermark: 1237882352.01944@Cn0Hb/E3oxjIO4GE4eFglw > X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f > X-eda.org-MailScanner-Watermark: 1237881490.49764@LtyKbHxFPYz5OUhByAFmkg > DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; > d=gmail.com; s=gamma; > h=domainkey-signature:mime-version:received:reply-to:in-reply-to > :references:date:message-id:subject:from:to:cc:content-type; > bh=ZFEAD8EpnNpDa5aO+MHFHA2olOr3VEdskn400bKvUGQ=; > b=WNo0PBi35latovgcB2QFcufEjGB2Jv4iIGTcz5QxJfW3xavYNj6Fni3SuTDBDrL8TE > PrXiqAXNXF++MqeTN9eq6IPZ1MV85FDYoTRcwg2P9JztB3XdTK0b6/q5+9DzYiMAc1W4 > S0lcXn++DIdHhC7woorjcwR4KdRIyk3dZg/rY= > DomainKey-Signature: a=rsa-sha1; c=nofws; > d=gmail.com; s=gamma; > h=mime-version:reply-to:in-reply-to:references:date:message-id > :subject:from:to:cc:content-type; > b=PWTk274ctWyMJu//hh557Qz2ixGlxQ77v9kt9KHLxsysIXO2tOfR1Z4osYcA17ZMJa > FDsU9kF9ZroPq8113Vek8wK3M4yzzATtpfN46ZGAIM+WEDoxzGnjEWBFAZ9pfaiHwkkh > ums1p7zUqomyNjFjBB0HLyu1H7+C6DXXtUSic= > Reply-To: ben@systemverilog.us > Date: Mon, 16 Mar 2009 18:32:11 -0700 > From: ben cohen <hdlcohen@gmail.com> > Cc: Lisa Piper <ljpiper619@aol.com>, "sv-ac@eda.org" <sv-ac@eda.org> > X-eda.org-MailScanner: Found to be clean, Found to be clean > X-Spam-Status: No, No > Sender: owner-sv-ac@eda.org > X-eda.org-MailScanner-Information: Please contact the ISP for more information > X-MailScanner-ID: n2H8BLVr029660 > X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org > X-OriginalArrivalTime: 17 Mar 2009 08:27:58.0976 (UTC) FILETIME=[47852800:01C9A6DA] > > > --000e0cd2e0823ceac704654689d8 > Content-Type: text/plain; charset=windows-1252 > Content-Transfer-Encoding: quoted-printable > > code in 16.17.1 page 409 seems to indicate that an asssertion anding 2 > properrties musst have those properties use the identical leading clocks > Same for the ORing of 2 properties. > All thesee other examples seem confusing if that is the rule. > Ben > On 3/16/09, ben cohen <hdlcohen@gmail.com> wrote: > > > > Ed, Sorry to elaborate more on this, but a few more clarifications: > > 16.17.1: "The set of semantic leading clocks of q1 and q2 is the union of > > the set of semantic leading clocks of q1 with the set of semantic leading > > clocks of q2. " > > What does that really mean? For example in assert property ( > > @(posedge clk0) s0 |=3D> (@(posedge clk1) s1) and (@(posedge clk2) s2)); > > What is the leading clocking event? > > Changing the LRM example to the following, would that still be illegal? > > > > default clocking posedge_clk @(posedge clk); .. endclocking > > property q1; $rose(a) |-> ##[1:5] b; endproperty > > property q5; @(posedge clk2) b[*3] |=3D> !b; endproperty > > property q6; q1 and q5; endproperty > > *a5: assert property (q6); * > > > > // *illegal*: default leading clocking event, @(posedge clk), ??????????? > > // but semantic leading clock is not unique > > I can see the LRM example with the and of one property with negedge, and > > the other with posedge of same clock, thus, there is no possibility of the > > 2 properties starting at the same time. But declaring that this is ILLEG= > AL > > implies that the tool must check for illegality of clocks. What if clk1 = > =3D 3 > > times the frequency of clk2, but offset by 1 ns? I don't believe that the > > posedge of both clocks will ever be same. Is the tool to check for that > > too? > > Why can't the example in the LRM be treated as simply 2 separate clock? > > > > if the semantic leading clock set has more than one member it is an error. > > In the above examples, what are the leading clocks? > > Ben > > > > > > > > On Mon, Mar 16, 2009 at 5:00 AM, Eduard Cerny <Eduard.Cerny@synopsys.com>= > wrote: > > > >> Hi, > >> > >> > >> > >> The property in 16.14.2 containing the lonely =93and=94 is not shown (and > >> meant) as a maximal property in an assertion, it just explains its meani= > ng. > >> A few lines below it shows another one with a unique leading clock. > >> > >> In other words, the requirement of a unique leading clock is only when a > >> property is in an assertion and clock flow has been applied. Then if the > >> semantic leading clock set has more than one member it is an error. > >> > >> > >> > >> Best regards, > >> > >> ed > >> > >> > >> > >> > >> > >> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *= > Lisa > >> Piper > >> *Sent:* Sunday, March 15, 2009 12:39 AM > >> *To:* ben@systemverilog.us > >> *Cc:* sv-ac@eda.org > >> *Subject:* RE: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick > >> questions > >> > >> > >> > >> Sorry Ben, > >> > >> > >> > >> I stopped to answer the first question and did not even see the second > >> one. > >> > >> However, in 16.14.2 it says: > >> > >> > >> > >> The following example shows how to form a multiclocked property using > >> boolean property operators: > >> > >> > >> > >> (@(*posedge *clk0) sig0) *and *(@(*posedge *clk1) sig1) > >> > >> > >> > >> This is a multiclocked property, but it is not a multiclocked sequence. > >> This property evaluates to true at a > >> > >> point if, and only if, the two sequences > >> > >> @(*posedge *clk0) sig0 > >> > >> and > >> > >> @(*posedge *clk1) sig1 > >> > >> both have matches beginning at the point. > >> > >> > >> > >> For the example in question, there is no =93point=94 when both are true = > since > >> (posedge clk) can never be true when (negedge clk) is true: > >> > >> > >> > >> default clocking posedge_clk @(posedge clk); .. endclocking > >> property q1; $rose(a) |-> ##[1:5] b; endproperty > >> property q5; @(*negedge *clk) b[*3] |=3D> !b; endproperty > >> property q6; q1 and q5; endproperty > >> *a5: assert property (q6); * > >> > >> // *illegal*: default leading clocking event, @(posedge clk), > >> // but semantic leading clock is not unique > >> > >> Hopefully somebody else will help to clarify this better. I think this > >> also violates the statement on page 405 that: > >> > >> > >> > >> e) A multiclocked sequence or property can inherit the default clocking > >> event as its leading clocking > >> > >> event. If a multiclocked property is the maximal property of a concurrent > >> assertion statement, then > >> > >> the property shall have a unique semantic leading clock (see 16.17.1). > >> > >> > >> > >> Lisa > >> > >> > >> ------------------------------ > >> > >> *From:* ben cohen [mailto:hdlcohen@gmail.com] > >> *Sent:* Saturday, March 14, 2009 10:35 PM > >> *To:* Lisa Piper > >> *Cc:* sv-ac@server.eda.org > >> *Subject:* Re: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick > >> questions > >> > >> > >> > >> Thanks Lisa for the detailed explanation. Now, on the 2nd half of the > >> question, what's the answer? > >> > >> Page 406 > >> default clocking posedge_clk @(posedge clk); .. endclocking > >> property q1; $rose(a) |-> ##[1:5] b; endproperty > >> property q5; @(*negedge *clk) b[*3] |=3D> !b; endproperty > >> property q6; q1 and q5; endproperty > >> *a5: assert property (q6); ** > >> *// *illegal*: default leading clocking event, @(posedge clk), > >> // but semantic leading clock is not unique > >> Page 408 > >> The set of semantic leading clocks of q1 and q2 is the union of the set = > of > >> semantic leading clocks of q1 with the set of semantic leading clocks of= > q2. > >> > >> *Ben question: Not sure what "*union of the set of semantic ..." *means, > >> but in q6, isn't that equivalent to: " (@ (posedge clk) $rose(a) -> // = > the > >> default clock ##[1:5] b) and > >> (*@(*negedge *clk) b[*3] |=3D> !b) > >> > >> Ben > >> > >> > >> > >> On Sat, Mar 14, 2009 at 6:28 PM, Lisa Piper <ljpiper619@aol.com> wrote: > >> > >> Hi Ben, > >> > >> > >> > >> I=92ll try to answer this one. > >> > >> > >> > >> The reason is that when you flatten a sequence instance, the last step is > >> to =93Return the expression obtained by copying the local variable > >> declarations and body *sequence_expr *from *r' *and enclosing the result > >> in parentheses.=94 (step 7 of flatten_sequence(r) of F.4.1.1 in The rew= > riting > >> algorithm) Furthermore, it is stated in section 16.14.3 Clock flow: = > =93The > >> scope of a clocking event flows into parenthesized subexpressions and, if > >> the subexpression is a sequence, also flows left to right across the > >> parenthesized subexpression. However, the scope of a clocking event does= > not > >> flow out of enclosing parentheses.=94 > >> > >> > >> > >> So for the example in question: > >> > >> > >> > >> sequence s3; @(negedge clk) s2; endsequence > >> > >> c4: cover property (s3 ##1 b); > >> > >> > >> > >> the rewrite results in: > >> > >> > >> > >> c4: cover property ( (@(negedge clk) ($rose(a) ##[1:5] b) ) ##1 b; > >> > >> > >> > >> The issue is that there is no clock associated with the =93##1 b=94 at t= > he end > >> of the sequence expression since there is no default clock, leading cloc= > k, > >> or explicit clock. Hopefully it is clear that the other example you cre= > ated > >> is also not legal since there is no clock associated with s9. > >> > >> > >> > >> Lisa > >> > >> > >> > >> > >> > >> > >> ------------------------------ > >> > >> *From:* owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] *= > On > >> Behalf Of *ben cohen > >> *Sent:* Saturday, March 14, 2009 6:06 PM > >> *To:* sv-ac@server.eda.org > >> *Subject:* [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick > >> questions > >> > >> > >> > >> Am having a hard time understanding the following points. Your help is > >> appreciated. > >> > >> Ben > >> > >> page 406-407 > >> > >> module examples_without_default (input logic a, b, c, clk); > >> > >> sequence s2; $rose(a) ##[1:5] b; endsequence > >> > >> sequence s3; @(negedge clk) s2; endsequence > >> > >> > >> > >> c4: cover property (s3 ##1 b); > >> > >> // illegal: no default, inferred, or explicit leading > >> > >> // clocking event and maximal property is not an instance > >> > >> *Ben question: Why isn't s3 equivalent to: * > >> > >> *c4: cover property (@(negedge clk) $rose(a) ##[1:5] b ##1 b);* > >> > >> *Ben question: would this be OK? * > >> > >> *sequence s9; b; endsequence : * > >> > >> c4b: cover property (s3 ##1 s9); > >> > >> --- > >> > >> Page 406 > >> > >> default clocking posedge_clk @(posedge clk); .. endclocking > >> > >> property q1; $rose(a) |-> ##[1:5] b; endproperty > >> > >> property q5; @(*negedge *clk) b[*3] |=3D> !b; endproperty > >> > >> property q6; q1 and q5; endproperty > >> > >> *a5: assert property (q6);* > >> > >> // *illegal*: default leading clocking event, @(posedge clk), > >> > >> // but semantic leading clock is not unique > >> > >> Page 408 > >> > >> The set of semantic leading clocks of q1 and q2 is the union of the set = > of > >> semantic leading clocks of q1 with the set of semantic leading clocks of= > q2. > >> > >> *Ben question: Not sure what "*union of the set of semantic .." *means, > >> but in q6, isn't that equivalent to: " @ (posedge clk) $ose(a) -> // the > >> default clock* > >> > >> * ##[1:5] b and *@(*negedge > >> *clk) b[*3] |=3D> !b > >> > >> > >> > >> > >> > >> > >> > >> > >> -- > >> 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. > >> > > > > > > --=20 > This message has been scanned for viruses and > dangerous content by MailScanner, and is > believed to be clean. > > > --000e0cd2e0823ceac704654689d8 > Content-Type: text/html; charset=windows-1252 > Content-Transfer-Encoding: quoted-printable > > code in 16.17.1 page 409 seems to indicate that an asssertion anding 2 prop= > errties musst have those=A0 properties use the identical=A0 leading clocks<= > br>Same for the ORing of 2 properties. <br>All thesee other examples seem c= > onfusing if that is the rule. <br> > Ben<br><div><span class=3D"gmail_quote">On 3/16/09, <b class=3D"gmail_sende= > rname">ben cohen</b> <<a href=3D"mailto:hdlcohen@gmail.com">hdlcohen@gma= > il.com</a>> wrote:</span><blockquote class=3D"gmail_quote" style=3D"bord= > er-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-l= > eft: 1ex;"> > Ed,=A0<div>Sorry to elaborate more on this, but a few more clarifications:= > =A0</div><div>16.17.1: "The set of semantic leading clocks of q1 and q= > 2 is the union of the set of semantic leading clocks of=A0q1 with the set o= > f semantic leading clocks of q2. "=A0</div> > > <div>What does that really mean? =A0For example in a<span style=3D"font-wei= > ght: bold;">ssert propert</span>y (</div><div>@(posedge clk0) s0 |=3D> (= > @(posedge clk1) s1) and (@(posedge clk2) s2));=A0<br></div> > <div>What is the leading clocking event?=A0</div><div>Changing the LRM exam= > ple to the following, would that still be illegal?=A0</div><div><p><span st= > yle=3D"color: rgb(80, 0, 80);"><span class=3D"q">default clocking posedge_c= > lk @(posedge clk); .. endclocking=A0<br> > > property q1; =A0$rose(a) |-> ##[1:5] b;=A0endproperty=A0<br></span>prope= > rty q5;=A0@(<span style=3D"font-weight: bold;">posedge=A0</span>clk2) b[*3]= > |=3D> !b;=A0endproperty=A0<span class=3D"q"><br>property q6;=A0q1 and q= > 5;=A0endproperty=A0<br> > > </span></span><span><b><span style=3D"color: red;">a5: assert property (q6)= > ;=A0</span></b></span></p><span class=3D"q"><p style=3D"margin-bottom: 12pt= > ;"><span><span style=3D"color: rgb(80, 0, 80);">//=A0<b>illegal</b>: defaul= > t leading clocking event, @(posedge clk), =A0???????????</span></span><span= > style=3D"color: rgb(80, 0, 80);"><br> > > <span>// but semantic leading clock is not unique</span></span></p></span><= > /div><div>I can see the LRM example with the <span style=3D"font-weight: bo= > ld;">and </span>of one property with <span style=3D"font-weight: bold;">neg= > edge</span>, and the other with <span style=3D"font-weight: bold;">posedge = > </span>of same clock, thus, there is no possibility of the 2 properties sta= > rting at the same time. =A0But declaring that this is ILLEGAL implies that = > the tool must check for=A0illegality=A0of clocks. =A0What if clk1 =3D 3 tim= > es the frequency of clk2, but offset by 1 ns? I don't believe that the = > posedge of both clocks will ever be same. =A0Is the tool to check for that = > too?=A0</div> > > <div>Why can't the example in the LRM be treated as simply 2 separate c= > lock?=A0</div><span class=3D"q"><div><br></div><div><span style=3D"color: r= > gb(0, 0, 128);">if the semantic leading clock set has more than one member = > it is an error.</span><br> > > </div></span><div>In the above examples, what are the leading clocks?<span = > style=3D"color: rgb(0, 0, 128);">=A0</span></div><div>Ben=A0</div><div><spa= > n class=3D"e" id=3D"q_120118cd05874571_9"><div><p><span style=3D"color: rgb= > (80, 0, 80);"><br> > > </span></p></div><div><br><div class=3D"gmail_quote">On Mon, Mar 16, 2009 a= > t 5:00 AM, Eduard Cerny <span dir=3D"ltr"><<a href=3D"mailto:Eduard.Cern= > y@synopsys.com" target=3D"_blank" onclick=3D"return top.js.OpenExtLink(wind= > ow,event,this)">Eduard.Cerny@synopsys.com</a>></span> wrote:<br> > <blockquote class=3D"gmail_quote" style=3D"border-left: 1px solid rgb(204, = > 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> > > > > > > > > > > > <div link=3D"blue" vlink=3D"blue" lang=3D"EN-US"> > > <div> > > <p><span style=3D"color: navy;">Hi, > </span></p> > > <p><span style=3D"color: navy;">=A0</span></p> > > <p><span style=3D"color: navy;">The > property in 16.14.2 containing the lonely =93and=94 is not shown (and > meant) as a maximal property in an assertion, it just explains its meaning.= > A > few lines below it shows another one with a unique leading clock.</span></p> > > <p><span style=3D"color: navy;">In > other words, the requirement of a unique leading clock is only when a prope= > rty > is in an assertion and clock flow has been applied. =A0Then if the semantic > leading clock set has more than one member it is an error.</span></p> > > <p><span style=3D"color: navy;">=A0</span></p> > > <p><span style=3D"color: navy;">Best > regards,</span></p> > > <p><span style=3D"color: navy;">ed</span></p> > > <p><span style=3D"color: navy;">=A0</span></p> > > <p><span style=3D"color: navy;">=A0</span></p> > > <div> > > <div style=3D"border-style: solid none none; border-color: rgb(181, 196, 22= > 3) -moz-use-text-color -moz-use-text-color; border-width: 1pt medium medium= > ; padding: 3pt 0in 0in;"> > > <p><b><span style=3D"font-size: 10pt;">From:</span></b><span style=3D"font-= > size: 10pt;"> <a href=3D"mailto:owner-sv-ac@eda.org" target=3D"_blank" oncl= > ick=3D"return top.js.OpenExtLink(window,event,this)">owner-sv-ac@eda.org</a> > [mailto:<a href=3D"mailto:owner-sv-ac@eda.org" target=3D"_blank" onclick=3D= > "return top.js.OpenExtLink(window,event,this)">owner-sv-ac@eda.org</a>] <b>= > On Behalf Of </b>Lisa Piper<br> > <b>Sent:</b> Sunday, March 15, 2009 12:39 AM<br> > <b>To:</b> <a href=3D"mailto:ben@systemverilog.us" target=3D"_blank" onclic= > k=3D"return top.js.OpenExtLink(window,event,this)">ben@systemverilog.us</a>= > <br> > <b>Cc:</b> <a href=3D"mailto:sv-ac@eda.org" target=3D"_blank" onclick=3D"re= > turn top.js.OpenExtLink(window,event,this)">sv-ac@eda.org</a><br> > <b>Subject:</b> RE: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // qui= > ck > questions</span></p> > > </div> > > </div><div><div></div><div> > > <p>=A0</p> > > <p><span style=3D"font-size: 10pt; color: navy;">Sorry Ben,</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">I stopped to answer the fi= > rst question and did not even see the > second one.=A0 </span><span><span style=3D"color: rgb(80, 0, 80);"></span><= > /span></p> > > <p><span><span style=3D"color: rgb(80, 0, 80);">However, > in 16.14.2 it says:</span></span></p> > > <p><span><span style=3D"color: rgb(80, 0, 80);">=A0</span></span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">The following example shows how to form a > multiclocked property using boolean property operators:</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">=A0</span></p> > > <p style=3D"text-indent: 0.5in;"><span style=3D"font-size: 9pt; font-family= > : CourierNewPSMT;">(@(</span><b><span style=3D"font-size: 9pt; font-family:= > CourierNewPS-BoldMT;">posedge </span></b><span style=3D"font-size: 9pt; fo= > nt-family: CourierNewPSMT;">clk0) sig0) </span><b><span style=3D"font-size:= > 9pt; font-family: CourierNewPS-BoldMT;">and </span></b><span style=3D"font= > -size: 9pt; font-family: CourierNewPSMT;">(@(</span><b><span style=3D"font-= > size: 9pt; font-family: CourierNewPS-BoldMT;">posedge </span></b><span styl= > e=3D"font-size: 9pt; font-family: CourierNewPSMT;">clk1) sig1)</span></p> > > > > <p style=3D"text-indent: 0.5in;"><span style=3D"font-size: 9pt; font-family= > : CourierNewPSMT;">=A0</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">This is a multiclocked property, but it is not a > multiclocked sequence. This property evaluates to true at a</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">point if, and only if, the two sequences</span></p> > > <p style=3D"text-indent: 0.5in;"><span style=3D"font-size: 9pt; font-family= > : CourierNewPSMT;">@(</span><b><span style=3D"font-size: 9pt; font-family: = > CourierNewPS-BoldMT;">posedge </span></b><span style=3D"font-size: 9pt; fon= > t-family: CourierNewPSMT;">clk0) sig0</span></p> > > > > <p style=3D"margin-left: 0.5in; text-indent: 0.5in;"><span style=3D"font-si= > ze: 10pt; font-family: TimesNewRomanPSMT;">and</span></p> > > <p style=3D"text-indent: 0.5in;"><span style=3D"font-size: 9pt; font-family= > : CourierNewPSMT;">@(</span><b><span style=3D"font-size: 9pt; font-family: = > CourierNewPS-BoldMT;">posedge </span></b><span style=3D"font-size: 9pt; fon= > t-family: CourierNewPSMT;">clk1) sig1</span></p> > > > > <p><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSMT;">both > have matches beginning at the point.</span></p> > > <p><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSMT;">=A0</sp= > an></p> > > <p><span style=3D"font-family: TimesNewRomanPSMT; color: purple;">For > the example in question, there is no =93point=94 when both are true > since (posedge clk) can never be true when (negedge clk) is true: </span></= > p> > > <p><span style=3D"font-family: TimesNewRomanPSMT; color: purple;">=A0</span= > ></p> > > <p><span style=3D"color: rgb(80, 0, 80);">default clocking posedge_clk > @(posedge clk); .. endclocking=A0<br> > property q1; =A0$rose(a) |-> ##[1:5] b;=A0endproperty=A0<br> > property q5;=A0@(<b>negedge=A0</b>clk) b[*3] |=3D> > !b;=A0endproperty=A0<br> > property q6;=A0q1 and q5;=A0endproperty=A0<br> > </span><span><b><span style=3D"color: red;">a5: assert > property (q6);=A0</span></b></span></p> > > <p style=3D"margin-bottom: 12pt;"><span><span style=3D"color: rgb(80, 0, 80= > );">//=A0<b>illegal</b>: default leading clocking event, > @(posedge clk),=A0</span></span><span style=3D"color: rgb(80, 0, 80);"><br> > <span>// but semantic leading clock is not unique</span></span></p> > > <p style=3D""><span style=3D"font-size: 10pt; color: navy;">Hopefully someb= > ody else will help > to clarify this better.=A0=A0 I think this also violates the statement on > page 405 that:</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T; color: black;">e) A multiclocked sequence or > property can inherit the default clocking event as its leading clocking</sp= > an></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T; color: black;">event. If a multiclocked property is > the maximal property of a concurrent assertion statement, then</span></p> > > <p><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSMT; color: b= > lack;">the property shall have a unique semantic leading clock (see </span>= > <span style=3D"font-size: 10pt; font-family: TimesNewRomanPSMT; color: blue= > ;">16.17.1</span><span style=3D"font-size: 10pt; font-family: TimesNewRoman= > PSMT; color: black;">).</span><span style=3D"font-size: 10pt; color: navy;"= > ></span></p> > > > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">Lisa</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <div> > > <div style=3D"text-align: center;" align=3D"center"> > > <hr align=3D"center" size=3D"2" width=3D"100%"> > > </div> > > <p><b><span style=3D"font-size: 10pt;">From:</span></b><span style=3D"font-= > size: 10pt;"> ben cohen > [mailto:<a href=3D"mailto:hdlcohen@gmail.com" target=3D"_blank" onclick=3D"= > return top.js.OpenExtLink(window,event,this)">hdlcohen@gmail.com</a>] <br> > <b>Sent:</b> Saturday, March 14, 2009 10:35 PM<br> > <b>To:</b> Lisa Piper<br> > <b>Cc:</b> <a href=3D"mailto:sv-ac@server.eda.org" target=3D"_blank" onclic= > k=3D"return top.js.OpenExtLink(window,event,this)">sv-ac@server.eda.org</a>= > <br> > <b>Subject:</b> Re: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // qui= > ck > questions</span></p> > > </div> > > <p>=A0</p> > > <p>Thanks Lisa for the detailed explanation. =A0Now, on the > 2nd half of the question, what's the answer?=A0</p> > > <div> > > <div> > > <p><span style=3D"color: rgb(80, 0, 80);">Page 406<br> > default clocking posedge_clk @(posedge clk); .. endclocking=A0<br> > property q1; =A0$rose(a) |-> ##[1:5] b;=A0endproperty=A0<br> > property q5;=A0@(<b>negedge=A0</b>clk) b[*3] |=3D> > !b;=A0endproperty=A0<br> > property q6;=A0q1 and q5;=A0endproperty=A0<br> > </span><span><b><span style=3D"color: red;">a5: assert > property (q6);=A0</span></b></span><b><span style=3D"color: red;"><br> > </span></b><span><span style=3D"color: rgb(80, 0, 80);">//=A0<b>illegal</b>: > default leading clocking event, @(posedge clk),=A0</span></span><span style= > =3D"color: rgb(80, 0, 80);"><br> > <span>// but semantic leading clock is not unique</span><br> > <span>Page 408=A0</span><br> > <span>The set of semantic leading clocks of q1 and q2 is > the union of the set of semantic leading clocks of=A0q1 with the set of > semantic leading clocks of q2.</span></span></p> > > </div> > > <div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">Ben question: Not sure what= > "</span></i></b><span style=3D"color: rgb(80, 0, 80);">union of the s= > et of semantic ..."=A0</span><b><i><span style=3D"color: rgb(0, 0, 153= > );">means, but in q6, isn't that equivalent to: " (@ > (posedge clk) $rose(a) -> =A0// the default clock<span>=A0=A0 =A0 =A0 = > =A0 =A0 =A0 =A0 > =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 > =A0 =A0 =A0 ##[1:5] b) =A0 =A0and (</span></span></i></b><span><span style= > =3D"color: black;">@(<b>negedge=A0</b>clk) > b[*3] |=3D> !b)</span></span><span style=3D"color: rgb(80, 0, 80);"></sp= > an></p> > > <p><span><span style=3D"color: black;">Ben=A0</span></span><span style=3D"c= > olor: rgb(80, 0, 80);"></span></p> > > </div> > > </div> > > <p>=A0</p> > > <div> > > <p>On Sat, Mar 14, 2009 at 6:28 PM, Lisa Piper <<a href=3D"mailto:ljpipe= > r619@aol.com" target=3D"_blank" onclick=3D"return top.js.OpenExtLink(window= > ,event,this)">ljpiper619@aol.com</a>> wrote:</p> > > <div> > > <div> > > <p><span style=3D"font-size: 10pt; color: navy;">Hi > Ben,</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">I=92ll > try to answer this one.=A0=A0 </span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; color: navy;">The reason is t= > hat when you flatten a sequence instance, the last > step is to =93</span><span style=3D"font-size: 10pt; font-family: TimesNewR= > omanPSMT;">Return > the expression obtained by copying the local variable declarations and body= > </span><i><span style=3D"font-size: 10pt; font-family: TimesNewRomanPS-Ita= > licMT;">sequence_expr=A0 > </span></i><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSMT;"= > >from </span><i><span style=3D"font-size: 10pt; font-family: TimesNewRomanP= > S-ItalicMT;">r' </span></i><span style=3D"font-size: 10pt; font-family:= > TimesNewRomanPSMT;">and enclosing the result > in parentheses.=94=A0 (step 7 of flatten_sequence(r) of F.4.1.1 in The > rewriting algorithm)=A0=A0 Furthermore, it is stated in section 16.14.3 > Clock flow:=A0 =93The scope of a clocking event flows into parenthesized > subexpressions and, if the subexpression is a sequence, also flows left to > right across the parenthesized subexpression. However, the scope of a clock= > ing > event does not flow out of enclosing parentheses.=94</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">=A0</span></p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">So > for the example in question:</span></p> > > <div> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">=A0</span></p> > > <p style=3D"text-indent: 0.5in;">sequence s3;=A0@(negedge clk) > s2;=A0endsequence </p> > > <p style=3D"text-indent: 0.5in;">c4: cover property (s3 ##1 b);</p> > > <p>=A0</p> > > </div> > > <p>the rewrite results in:</p> > > <p>=A0</p> > > <p style=3D"text-indent: 0.5in;">c4: cover property ( (@(negedge clk) ($ros= > e(a) > ##[1:5] b) =A0)=A0 ##1 b;</p> > > <p style=3D"text-indent: 0.5in;">=A0</p> > > <p>The issue is that there is no clock associated with the =93##1 b=94 > at the end of the sequence expression since there is no default clock, lead= > ing > clock, or explicit clock.=A0 Hopefully it is clear that the other example > you created is also not legal since there is no clock associated with s9.</= > p> > > <p>=A0</p> > > <p>Lisa</p> > > <div> > > <p>=A0</p> > > <p style=3D""><span style=3D"font-size: 10pt; font-family: TimesNewRomanPSM= > T;">=A0</span></p> > > <p><span style=3D"font-size: 10pt; color: navy;">=A0</span></p> > > <div> > > <div style=3D"text-align: center;" align=3D"center"> > > <hr align=3D"center" size=3D"2" width=3D"100%"> > > </div> > > <p><b><span style=3D"font-size: 10pt;">From:</span></b><span style=3D"font-= > size: 10pt;"> <a href=3D"mailto:owner-sv-ac@server.eda.org" target=3D"_blan= > k" onclick=3D"return top.js.OpenExtLink(window,event,this)">owner-sv-ac@ser= > ver.eda.org</a> > [mailto:<a href=3D"mailto:owner-sv-ac@server.eda.org" target=3D"_blank" onc= > lick=3D"return top.js.OpenExtLink(window,event,this)">owner-sv-ac@server.ed= > a.org</a>] > <b>On Behalf Of </b>ben cohen<br> > <b>Sent:</b> Saturday, March 14, 2009 6:06 PM<br> > <b>To:</b> <a href=3D"mailto:sv-ac@server.eda.org" target=3D"_blank" onclic= > k=3D"return top.js.OpenExtLink(window,event,this)">sv-ac@server.eda.org</a>= > <br> > <b>Subject:</b> [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick > questions</span></p> > > </div> > > <p>=A0</p> > > </div> > > <div> > > <div> > > <p>Am having a hard time understanding the following points. =A0Your help is > appreciated.=A0</p> > > </div> > > <div> > > <div> > > <div> > > <p>Ben=A0</p> > > </div> > > <div> > > <div> > > <div> > > <div> > > <p>page 406-407</p> > > </div> > > <div> > > <p>module examples_without_default (input logic a, b, c, clk);</p> > > </div> > > </div> > > </div> > > <div> > > <div> > > <p>sequence s2;=A0$rose(a) ##[1:5] b;=A0endsequence</p> > > </div> > > <div> > > <div> > > <p>sequence s3;=A0@(negedge clk) s2;=A0endsequence</p> > > </div> > > <div> > > <p>=A0</p> > > </div> > > <div> > > <div> > > <p>c4: cover property (s3 ##1 b);</p> > > </div> > > <div> > > <p>// illegal: no default, inferred, or explicit leading</p> > > </div> > > <div> > > <p>// clocking event and maximal property is not an instance</p> > > </div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">Ben question: Why isn't= > s3 equivalent > to:=A0</span></i></b></p> > > </div> > > <div> > > <p><b><span style=3D"color: red;">c4: cover property (@(negedge clk)=A0$ros= > e(a) > ##[1:5] b=A0##1 b);</span></b></p> > > </div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">Ben question: would this be= > OK?=A0</span></i></b></p> > > </div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">sequence s9; =A0 b; endsequ= > ence :=A0</span></i></b></p> > > </div> > > <div> > > <p><span style=3D"color: black;">c4b: cover property (s3 ##1 s9);</span></p> > > </div> > > <div> > > <p>---</p> > > </div> > > <div> > > <p>Page 406</p> > > </div> > > <div> > > <p>default clocking posedge_clk @(posedge clk); .. endclocking=A0</p> > > </div> > > <div> > > <div> > > <p>property q1; =A0$rose(a) |-> ##[1:5] b;=A0endproperty</p> > > </div> > > </div> > > <div> > > <div> > > <p>property q5;=A0@(<b>negedge </b>clk) b[*3] |=3D> !b;=A0endproperty</p> > > </div> > > </div> > > <div> > > <div> > > <p>property q6;=A0q1 and q5;=A0endproperty</p> > > </div> > > </div> > > <div> > > <div> > > <p><b><span style=3D"color: red;">a5: assert property (q6);</span></b></p> > > </div> > > <div> > > <p>// <b>illegal</b>: default leading clocking event, @(posedge clk),</p> > > </div> > > <div> > > <p>// but semantic leading clock is not unique</p> > > </div> > > </div> > > <div> > > <p>Page 408</p> > > </div> > > <div> > > <div> > > <p>The set of semantic leading clocks of q1 and q2 is the union of the set = > of > semantic leading clocks of=A0q1 with the set of semantic leading clocks of > q2.</p> > > </div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">Ben question: Not sure what= > "</span></i></b>union > of the set of semantic .." <b><i><span style=3D"color: rgb(0, 0, 153);= > ">means, but in > q6, isn't that equivalent to: " @ (posedge clk) $ose(a) -> =A0/= > / the > default clock</span></i></b></p> > > </div> > > <div> > > <p><b><i><span style=3D"color: rgb(0, 0, 153);">=A0=A0 =A0 =A0 =A0 =A0 > =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 > =A0 =A0 =A0 =A0 =A0 ##[1:5] b =A0 =A0and=A0</span></i></b><span style=3D"co= > lor: black;">@(<b>negedge=A0</b>clk) b[*3] |=3D> !b</span></p> > > </div> > > </div> > > <div> > > <p>=A0</p> > > </div> > > <div> > > <p>=A0</p> > > </div> > > </div> > > </div> > > </div> > > </div> > > </div> > > </div> > > </div> > > <p>=A0</p> > > <div> > > <p><br> > -- <br> > This message has been scanned for viruses and <br> > dangerous content by <a href=3D"http://www.mailscanner.info/" target=3D"_bl= > ank" onclick=3D"return top.js.OpenExtLink(window,event,this)"><b>MailScanne= > r</b></a>, > and is <br> > believed to be clean. </p> > > </div> > > </div> > > </div> > > </div> > > <p>=A0</p> > > </div> > > <p><br> > -- <br> > This message has been scanned for viruses and <br> > dangerous content by <a href=3D"http://www.mailscanner.info/" target=3D"_bl= > ank" onclick=3D"return top.js.OpenExtLink(window,event,this)"><b>MailScanne= > r</b></a>, > and is <br> > believed to be clean. </p> > > </div></div></div> > > </div> > > > </blockquote></div><br></div> > </span></div></blockquote></div><br> > <br />--=20 > <br />This message has been scanned for viruses and > <br />dangerous content by > <a href=3D"http://www.mailscanner.info/"><b>MailScanner</b></a>, and is > <br />believed to be clean. > > > --000e0cd2e0823ceac704654689d8-- > -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Sun Apr 26 17:24:16 2009
This archive was generated by hypermail 2.1.8 : Sun Apr 26 2009 - 17:25:21 PDT