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

HI Manisha,

Please, see my comments below.

Thanks,
Dmitry

From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Monday, May 16, 2011 10:21
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: 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.
[Korchemny, Dmitry]

Let's consider assertions:
a1: assert property (@(posedge clk) cond |-> $past(t));
a2: assert property (@(posedge clk) cond |-> $sampled(t));

where cond is some conditions. The original assertions are almost identical because of the implicit always, except for the fact that the first one fails at the initial clock tick.
Assertions a1 and a2 are different. a1 uses the sampled value of t, i.e., its preponed value in the current clock tick. a2 uses the sampled value of t evaluated in the Postponed region of the previous clock tick. Since the sampled value of a regular checker variable is its preponed value, it is stable during the entire tick, and therefore its value in the Postponed region of the previous clock tick is the preponed value in that tick.

This is exactly the same behavior that we have now.

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.
[Korchemny, Dmitry] This is not easy to do since you need also specify in what point of the Observed region the value is taken. E.g., if v is an active checker free variable, it gets its new value in the Observed region, and its new value should be take in $future_gclk(v). Therefore it is easier to say that the sampled value is taken from the Postponed region in the future global clock tick.

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.
---------------------------------------------------------------------
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.