[sv-ac] RE: Q: clock inference for $past in sequence

I have submitted this issue to Mantis:
http://www.verilog.org/mantis/view.php?id=4991


-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Prabhakar, Anupam
Sent: Friday, August 08, 2014 11:42 AM
To: Seligman, Erik; John Havlicek; sv-ac@eda.org
Cc: Bingham, Jesse D
Subject: [sv-ac] RE: Q: clock inference for $past in sequence

Inferring clock from context for a sequence instance on which a method is applied is something new in IEEE1800-2012

From Sec 16.13.3
Similarly, the scope of a clocking event flows into an instance of a named property or sequence, regardless of whether method triggered or method matched is applied to the instance of the sequence.

And from 16.9.3
If called in an assertion, the appropriate clocking event as determined by clock flow rules (see
16.13.3) is used.

I think this should imply that $past is clocked (although I think 'triggered' should have been used instead of 'matched').

There are similar examples in the LRM Sec 16.13.6 (if needed we can modify the comment to say 'e4 and $rose(b) infer .....') sequence e4;
$rose(b) ##1 c;
endsequence
// e4 infers posedge clk_a as per clock flow rules
a1: assert property (@(posedge clk_a) a |=> e4.triggered);

Anupam

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik
Sent: Friday, August 08, 2014 11:31 AM
To: John Havlicek; sv-ac@eda.org
Cc: Bingham, Jesse D
Subject: [sv-ac] RE: Q: clock inference for $past in sequence

Hmmm...  So are you saying that the intention was for the $past to be treated like a ##1 in an assertion, and get the clock from the instantiation context?   Is this something we need to file a clarification Mantis on?

-----Original Message-----
From: John Havlicek [mailto:johnh@cadence.com]
Sent: Friday, August 08, 2014 11:10 AM
To: Seligman, Erik; sv-ac@eda.org
Cc: Bingham, Jesse D
Subject: RE: Q: clock inference for $past in sequence

Interesting.  For the purpose of discussion, let's assume that your prop3 is instantiated somewhere, say in a concurrent assertion statement.

Then I would expect the example you show to compile with the @(posedge clk) flowing into the instance of sig_is_stable, and from there attaching to the sampled value function $past.

I see that the language in 16.9.3 might be interpreted differently if one just reads

"For a sampled value function other than $sampled, the clocking event shall be explicitly specified as an argument or inferred from the code where the function is called."

One might take this to mean that the clock for $past must be resolved in the context of the declaration of sequence sig_is_stable, because that is where the function is called.  But if one reads further, it says that the rules about to be described apply, and the first of these rules says

"If called in an assertion, the appropriate clocking event as determined by clock flow rules (see 16.13.3) is used."

To me, that says that the clock flows into the instance of the sequence as I described above.  In general, clocking is resolved at instances, not at declarations.

I also see the argument that $past is not called directly in the assertion, but rather in an instance in an instance in an assertion.  But I believe that the intention was that clock flow apply throughout these instances since clock flow explicitly says the clock scope descends into instances.

Best regards,

John Havlicek
  

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik
Sent: Friday, August 08, 2014 11:09 AM
To: sv-ac@eda.org
Cc: Bingham, Jesse D
Subject: [sv-ac] Q: clock inference for $past in sequence

In a sequence, is a sampled value function required to infer a clock from the sequence declaration, rather than the sequence instantiation?     This is how tools I'm using interpret the current LRM language in 16.9.3, though this difference vs the ##n operator seems counter-intuitive for some users.    

If this is correct, was it done intentionally, or is it an unintended side effect of our wording?

-----------------

// Code below generates compile error due to no clock for $past, even though clock is in context when sequence instantiated sequence sig_is_stable(sig);
  (sig == $past(sig,1));
endsequence

property prop3(untyped sig, int upto);
   @(posedge clk) disable iff(reset) trigger |-> sig_is_stable(sig).matched; endproperty

--
This message has been scanned for viruses and dangerous content by 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.




--
This message has been scanned for viruses and dangerous content by 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.