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>wrote:

>  Hello Ben,
>
> please see my answers below
>
> ed
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Monday, March 16, 2009 7:10 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,
>
> 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 a*ssert propert*y (
>
> @(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>
> 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.