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 |=> (@(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] |=> !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 ILLEGAL > implies that the tool must check for illegality of clocks. What if clk1 = 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 “and” 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. >> >> 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 “point” 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] |=> !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] |=> !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] |=> !b) >> >> Ben >> >> >> >> On Sat, Mar 14, 2009 at 6:28 PM, Lisa Piper <ljpiper619@aol.com> wrote: >> >> Hi Ben, >> >> >> >> I’ll try to answer this one. >> >> >> >> The reason is that when you flatten a sequence instance, the last step is >> to “Return the expression obtained by copying the local variable >> declarations and body *sequence_expr *from *r' *and enclosing the result >> in parentheses.” (step 7 of flatten_sequence(r) of F.4.1.1 in The rewriting >> algorithm) Furthermore, it is stated in section 16.14.3 Clock flow: “The >> 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.” >> >> >> >> 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 “##1 b” at the end >> of the sequence expression since there is no default clock, leading clock, >> or explicit clock. Hopefully it is clear that the other example you created >> 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] |=> !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] |=> !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. >> > > -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Mar 17 01:26:08 2009
This archive was generated by hypermail 2.1.8 : Tue Mar 17 2009 - 01:27:03 PDT