RE: [sv-ac] Issue #1551

Hi Ed,

 

In LRM it is written regarding clocking event inference.

 

The following rules are used to infer the clocking event:

- If used in an assertion, the appropriate clocking event from the
assertion is used.

- If used in an action block of a singly clocked assertion, the clock of
the assertion is used.

- If used in a procedural block, the inferred clock, if any, for the
procedural code (see 17.13.5) is used.

 

Regards,

Dmitry

 

________________________________

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
Sent: Tuesday, October 03, 2006 6:01 PM
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: [sv-ac] Issue #1551

 

Dmitry,

 

why would the clock propagate to $sampled in

 

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

We do not do that for $past...

 

ed

 

	 

	
________________________________


	From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf
Of Korchemny, Dmitry
	Sent: Tuesday, October 03, 2006 11:52 AM
	To: sv-ac@eda-stds.org
	Subject: [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