[sv-ec] 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.