RE: [sv-ac] Issue #1551

Hi John,

This is a legitimate interpretation, but this behavior is inconsistent
with FV. Why we should care for reset glitches only in the concurrent
assertions, while ignore glitches of all other variables?

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Tuesday, October 31, 2006 3:22 PM
To: sv-ac@server.eda-stds.org
Subject: Re: [sv-ac] Issue #1551

Hi Dmitry:

> 	Current LRM definition states:
> 
> 	The expression in the disable iff clause is evaluated using the
> current values of variables (not sampled).
> 
> 	This is ambiguous: one can understand it either as the reset is
> asynchronous (but nevertheless sampled at the preponed region) or that
> the reset is asynchronous and sampled in the observed region. It is
> enough add an explanation that the first version is correct to be
> formally backward compatible. Actually, if we choose the first
version,
> the backward compatibility will be broken since most users and tool
> developers (and I among them) understood that the value in the
observed
> region is taken.

There is another interpretation.  It is that the "disable iff"
condition is tested in all regions of all timesteps.  If there is
an evaluation attempt that is underway during some region of
some timestep in which the "disable iff" condition is true, then
this is enough to pre-empt the evaluation attempt.

This interpretation is why people have said that a glitch on 
the "disable iff" condition in the active region is enough 
to pre-empt the assertion evaluation.

Best regards,

John H.