[sv-ac] Issue #1551

Hi all,

 

I would like to summarize our discussion regarding disable iff behavior.

 

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.

 

However, the second version is problematic (as I pointed in #1551) since
the formal verification will give different results than the dynamic
simulation. Therefore we have the following options:

 

1.	Define that the reset value is sampled in the preponed region,
which is not backward compatible de facto
2.	Adopt the second version, and use explicit $sampled value on the
reset (e.g., disable iff ($sampled(rst)))
3.	Adopt the second version and in addition define new operators -
accepton and rejecton
4.	Adopt the second version and introduce a new general reset
operator - disable iff1 :-)

 

The second option looks problematic: firstly, it is not intuitive to
always write $sampled function in disable iff as a right methodology,
and it will be hardly accepted by new users; secondly, in the following
example:

 

always @(posedge clk) assert property (disable iff ($sampled(rst)) ...),
the reset will be synchronous, since in this case $sampled(rst) =
$sampled(rst, @(posedge clk).

 

As for the third option, it has a different problem. Though introduction
of operators accepton and rejecton is very useful (and I can give a
couple of examples when they are really needed) since they may be used
with any property expression, using them as the main reset operator, we
lose the general reset operator disable iff making it obsolete. It means
that all the disabled semantics becomes not relevant anymore since
disable iff in its current form does not have clean formal semantics.
We'll also have to use different reset operators for assert/assume and
cover: accepton for assert/assume and rejecton for cover. It will be
more difficult to formally define which accepton operator in the formula
is the main reset.

 

Introducing one more general reset operator (the last option) along with
accepton and rejecton looks strange.

 

Thanks,

Dmitry