[sv-ec] RE: [sv-ac] Properties in clocking blocks

Hi Jonathan,

Clause 16.4, par. 2, has the following explanation:
"If a variable used in an assertion is a clocking block input
variable, the variable must be sampled by the clocking block with #1step
sampling. Any other type of
sampling for the clocking block variable shall result in an error. The
assertion using the clocking block
variable shall not do its own sampling on the variable, but rather use
the sampled value produced by the
clocking block. This is explained in Clause 4."

Would that be enough? 

Best regards,
ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Jonathan Bromley
> Sent: Friday, August 10, 2007 5:34 AM
> To: sv-ec@eda-stds.org; sv-ac@eda-stds.org
> Subject: [sv-ac] Properties in clocking blocks
> 
> hi AC and EC,
> 
> I think we may have a problem with the semantics of
> signal sampling for properties and sequences declared
> in a clocking block.
> 
> Clause 14 (in draft 3a) doesn't mention this at all, 
> and probably it should.  Clause 16.17 describes it, 
> but is somewhat imprecise.  I think input-clockvar sampling 
> semantics in Mantis 890 may have broken its intent.
> In any event, 16.17 needs at least a minor rewrite 
> for clarification and to bring its language into line
> with clause 14 (for example, to use the word "clockvar"
> where appropriate).
> 
> 
> Given...
> 
>   logic A;
>   clocking cb @(posedge C);
>     input #1step A;
>     sequence c; A; endsequence
>   endclocking
>   sequence s; A; endsequence
> 
> it's clear that sequence s samples A with #1step sampling.
> But what does sequence c sample?  Does it sample A, or cb.A?
> If the latter, when does the sample happen?  Is sequence c
> clocked by @(posedge C), or by @(cb) ?  Recall that 
> property evaluation and the updating of cb.A both occur
> in the Observed region, and therefore may race if the
> sequence is clocked by @(posedge C); but there is no race
> if the sequence is clocked by @(cb), because cb.A is 
> guaranteed to update before event (cb) is fired.
> 
> I have a testcase that, in at least one simulator, exhibits
> a race condition so that I randomly get different results 
> from these two expressions if they appear in properties in a 
> clocking block, whereas they behave identically - as expected - 
> if they appear in properties outside a clocking block:
> 
>   $past(S1) && !$past(S2)
>   $past(S1 && !S2)
> 
> Of course it's possible that this is just a simulator
> bug.  But I was unable to work out from the LRM what
> is really supposed to happen.
> 
> Clarification or correction welcomed.
> -- 
> Jonathan Bromley
> 
> 
> -- 
> 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.