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

Ed,

> Clause 16.4, par. 2, has the following explanation:

Thanks for the 16.4 reference - I failed to mention that in 
my original mail.

> "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

I guess it's fair to infer from this that the property
*inside* the clocking should have exactly the same sampling
semantics that it would have had if it had been *outside* 
the clocking, but clocked by the same clock event.  One of 
the particularly neat things about #1step sampling in clockings
is that it allows ordinary procedural code to have access to
the exact same signal values as were sampled by assertions.

> 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 the problem.  "The sampled value produced by the
clocking block" is, presumably, the contents of a clockvar.
This value is updated in the Observed region, and therefore
its update will race with evaluation of the assertion *if the
assertion is clocked by the original clock event*.  I am
fairly sure that this is the source of the errors I saw.

However, if we define the clocking-block property to be 
clocked not by the original clock event, but by the 
clocking block's own event @(cb), then we have a guarantee
that the assertions cannot run until after the clockvars
have been updated with their sampled values.  I believe
(but I lack the expertise to be certain) that this would
not impact the meaning of properties in formal tools.
It is *essential* if we are to get meaningful behaviour 
in simulation.

Another, follow-on question: Is it legal for properties in
a clocking block to make reference to signals that are *not*
sampled by the clocking block?  If so, does that create a
new implicit clockvar, or does the property sample those
out-of-scope signals with the regular assertion-style 
sampling semantics?

Thanks
-- 
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, Hampshire, BH24 1AW, UK
Tel: +44 (0)1425 471223                   Email: jonathan.bromley@doulos.com
Fax: +44 (0)1425 471573                           Web: http://www.doulos.com

The contents of this message may contain personal views which 
are not the views of Doulos Ltd., unless specifically stated.

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