Mantis 2556 __X__ Yes ____ No
<http://www.eda-stds.org/mantis/file_download.php?file_id=4965&type=bug>
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 <http://www.eda-stds.org/svdb/view.php?id=3552>
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.<http://www.eda-stds.org/mantis/file_download.php?file_id=5099&type=bug>
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
-- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed May 25 18:30:29 2011
This archive was generated by hypermail 2.1.8 : Wed May 25 2011 - 18:30:35 PDT