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

Hi Ben,

We can only add references to the content of Mantis items that have already been resolved. The correct way to handle this is to write 3552 on top of 3213 provided 3213 has been resolved.

I modified the problematic sentence as follows:

This is because of the following. Expression s.triggered is evaluated in the Observed region. The function $rose in a concurrent assertion is also called in the Observed region after the value of s.triggered has been computed. It compares this value of s.triggered with its value in the Postponed region of the previous clock tick.

The updated version is here: http://www.eda-stds.org/mantis/file_download.php?file_id=5105&type=bug

Thanks,
Dmitry

P.S. If you have minor comments (like in 3069) it is more appropriate to send a positive vote with a friendly amendment.

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Thursday, May 26, 2011 04:29
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: Re: [sv-ac] Call to vote: Due May 30

Mantis 2556 __X__ Yes ____ No

Mantis 3069 __X__ Yes ____ No //Make the following editing:
In the following example the property p is declared in a module which contains containing a global clocking declaration

Mantis 3213 ____ Yes __X__ No
[Ben] Need to add a reference to a subsection that clarifies how .triggered is used after "The sampled value of s.triggered is its current value, and $stable(s.triggered) compares the current value of $stable(s.triggered)with its value from the Postponed region of the previous clock tick."
This reference is currently in the works and was not yet approved. It's in
http://www.eda-stds.org/svdb/view.php?id=3552
Updated on 5/24/01

1) Added

a1: assert property(@ (posedge clk) $stable(s1) |-> c );

a2: assert property(@ (posedge clk) (s1.triggered) |-> c);

2) These guidelines are in 16.14.6 Sequence methods, which is a subsection of 16.14 Multiclock support; Yet these guidelines are shown for singly clocked properties. Shouldn't these guidelines belong to the end of section "16.9.11 Detecting and using end point of a sequence"
[Ben] Editing and clarification changes needed,
This is because s.triggered is evaluated in the Observed region, and the function $rose in a concurrent assertion is also called in the Observed region after the value of s.triggered has been computed, compares this value of s.triggered with its value in the Postponed region of the previous clock tick.
This does not read well, compares this ... I don't understand it.
....
In the latter case the sampled value of s.triggered is always 0 regardless of the sequence match, and therefore $rose(s.triggered) always returns false in this context.
[Ben] Again, do we need a reference to examples, as mentioned above?

Mantis 3295 __X__ Yes ____ No
http://www.eda-stds.org/mantis/view.php?id=3295
http://www.eda-stds.org/mantis/file_download.php?file_id=5097&type=bug
---------------------------------------------------------------------
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.