RE: [sv-ac] Proposal updated for Mantis 2656 (Ballot Comment #84)

Hi Ben,

Please, see my comments below.

Dmitry

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of ben cohen
Sent: Thursday, April 30, 2009 10:43 PM
To: Thomas.Thatcher@sun.com
Cc: sv-ac@server.eda.org
Subject: Re: [sv-ac] Proposal updated for Mantis 2656 (Ballot Comment #84)

Two comments:
The table: I find "Table 16-2-Global clocking future sampled value functions" missing several entry points for the global clocking, and it is also missing the entry for $falling_gclk(clk),
That last entry is needed because the one of the points of this table is to demonstrate why the violation is at time 80.  Without that entry, it is left as an exercise for the reader to figure out how $falling_gclk(clk) fits into that table and graph.   Attached is my suggested update to the table for your considerations.
[Korchemny, Dmitry] $falling_gclk(clk) is present in Table 16-2, and in your table it appears twice. I don't think that we need to consider all ticks of the global clock in this table. If you disagree, you are welcome to  open a Mantis item with your suggestion. Unfortunately, we are not authorized to address it now.

From LRM: The following assertion states that the signal may change only on falling clock:
   a1: assert property (@$global_clock $changing_gclk(sig)
      |-> $falling_gclk(clk))
     else $error("sig is not stable");
Figure 16-4 shows that this property is violated at time 80. The vertical arrows indicate the ticks of the global clock. The error message $error("sig is not stable") is executed at time 90.

2656_global_clk_20090427.doc
Since most designs use a single edge of the clock, rather thatn both edges, I suggest that we modify the example from:
              global clocking @clk; endclocking
To the following
             global clocking @ (posedge clk); endclocking
assert property(@$global_clock a);
the assertion states that a is true at each tick of the global clock. In simulation, tThis assertion is logically
equivalent to
assert property(@ (posedge clk)  a);

[Korchemny, Dmitry] I think that global clocking @clk; endclocking also makes sense. The global clock reflects the primary clock, and the primary clock normally should tick at least at each change of clk. Consider the following assertion: the clock always ticks. You can implement it as:

assert property (@$global_clock $rising_gclk(clk)); (or $changing_gclk, $falling_gclk).

According to the definition you suggest this assertion will be violated, since the sampled value of clk is always 0 @(posedge clk).


On Mon, Apr 27, 2009 at 10:53 AM, Thomas Thatcher <Thomas.Thatcher@sun.com<mailto:Thomas.Thatcher@sun.com>> wrote:
Hello everyone,

I uploaded the proposal for Mantis 2656 that incorporates Erik's request to change "equivalent" to "logically equivalent".

The file names are
       2656_global_clk_20090427.doc
       2656_global_clk_20090427.pdf

Tom

--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.


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