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  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 

 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.