Hi Ben, yes, that is my interpretation too. ed From: ben cohen [mailto:hdlcohen@gmail.com] Sent: Tuesday, March 17, 2009 12:34 PM To: Eduard Cerny Cc: Lisa Piper; sv-ac@eda.org Subject: Re: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick questions Ed, OK, so in essence, an assertion must have a unique leading clocking event. Thus, assert property ( (@ (posedge clk1) a ) and (@ (posedge clk2) b) ); // ILLEGAL because there is no unique leading clocking event for the assertion. First operand of the AND has a different clock than the 2nd operand of the AND. but assert property ( (@ (posedge clk1) a ) and (@ (posedge clk1) b) ); // LEGAL, same clock assert property ( @ (posedge clk) c |=> (@ (posedge clk1) a ) and (@ (posedge clk2) b) )) ; // LEGAL because @ (posedge clk) is the leading clocking event for the assertion. Ben On Tue, Mar 17, 2009 at 6:40 AM, Eduard Cerny <Eduard.Cerny@synopsys.com<mailto:Eduard.Cerny@synopsys.com>> wrote: Hello Ben, please see my answers below ed From: ben cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>] Sent: Monday, March 16, 2009 7:10 PM To: Eduard Cerny Cc: Lisa Piper; sv-ac@eda.org<mailto:sv-ac@eda.org> Subject: Re: [sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick questions 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? [Ed:] posedge clk0. Quote: The set of semantic leading clocks of m |=> p is equal to the set of semantic leading clocks of m. Here it also more specifically that m is s0, its leading clock is "inherited", and it inherits posedge clk0 from clock flow. 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); [Ed:] After substitution into the assertion you get assert property (($rose(a) |-> ##[1:5] b) and (@(posedge clk2) b[*3] |=> !b)); so, in my view, you have posedge clk2 as the leading clock of the second operand of "and" and inherited for the first one. The inheritance is from default clocking which is posedge clk. the inherited clock has no effect on the 2nd operand, since it has a clock. So in my opinion this is illegal. Perhaps someone else can comment too. // 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<mailto: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> [mailto: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<mailto:ben@systemverilog.us> Cc: sv-ac@eda.org<mailto: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<mailto:hdlcohen@gmail.com>] Sent: Saturday, March 14, 2009 10:35 PM To: Lisa Piper Cc: sv-ac@server.eda.org<mailto: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<mailto: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> [mailto: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<mailto: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 12:24:46 2009
This archive was generated by hypermail 2.1.8 : Tue Mar 17 2009 - 12:28:00 PDT