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, and is
believed to be clean.