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

Hi Jonathan,

Although 890 does not clarify it clearly that there is no race between
updating of sampled values of clocking block signals and assertions
reading their values, I think that was the intention. Nowhere in 890 it
says that the sampled values of the clocking block are updated in
Observed region, it simply says that the clocking event happens in
Observed region and sampled values are available to be read at that
clocking event. Here is the text from 890:

Upon processing its specified clocking event, a clocking block shall
update its sampled values before triggering the event associated with
the clocking block name. This event shall be triggered in the Observed
region. Thus, a process that waits for the clocking block itself is
guaranteed to read the updated sampled values, regardless of the
scheduling region in which either the waiting or the triggering
processes execute.

So, I do not see any contradiction in the text here and text in
assertion section. 

Manisha

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Jonathan Bromley
Sent: Sunday, August 12, 2007 2:38 PM
To: Eduard Cerny; sv-ec@server.eda-stds.org; sv-ac@server.eda-stds.org
Subject: 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.



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