RE: [sv-ac] RE: Call to vote: Due May 16

Hi Dimitry,
 
I am still wondering about checker variables that are assigned in
re-nba. Here is an example:
 
checker test(a); // a is a regular design variable
 
bit t;
 
always @(posedge clk)
  t <= a;
 
assert property (@(posedge clk) $past(t));
assert property (@(posedge clk) $sampled(t));
 
From assertions point of view $past(t) and $sampled(t) are always same
because $past returns the value after the update from the previous time
step and $sampled returns the current value which is also same as update
has not happened yet.
 
Also, I am not comfortable with $future_gclk using value from postponed
region.
 
What if we change the postponed region to Observed region ? This will
keep assertion evaluation consistent with previous versions.
 
Thanks.
Manisha

________________________________

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Monday, May 16, 2011 12:28 PM
To: Kulshrestha, Manisha; sv-ac@eda-stds.org
Subject: RE: [sv-ac] RE: Call to vote: Due May 16

Hi Manisha,

Following Ed's comments I recently uploaded a new version with a
clarification about evaluating a sampled value in the Postponed region.
I put this clarification in the beginning of 16.9.3.

http://www.eda-stds.org/mantis/file_download.php?file_id=5033&type=bug

Is this explanation satisfactory from your point of view? If not, what
are your suggestions?

Thanks,

Dmitry

From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Monday, May 16, 2011 09:48
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: [sv-ac] RE: Call to vote: Due May 16

Mantis 3213 ___ Yes __ x __ No

http://www.eda-stds.org/mantis/view.php?id=3213

http://www.eda-stds.org/mantis/file_download.php?file_id=5003&type=bug

Here are my comments:

I do not understand the logic for picking up past value from postponed
region of previous clock tick. Shouldn't the past value be picked up
based on what assertions used in the previous clock tick ? I am
wondering about checker vars which are assigned non-blockingly (in
Re-NBA). Similarly the statement about $future_gclk(v) picking up value
from the postponed region is not clear to me. Shouldn't the values be
based on what assertions see in Observed region. If an assertion is
using $future_gclk(), does that mean the assertion has to be evaluated
in Postponed region ?

 Mantis 3385 __X_ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3385

http://www.eda-stds.org/mantis/file_download.php?file_id=4999&type=bug

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
---------------------------------------------------------------------
Intel Israel (74) Limited
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.