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

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Sunday, May 03, 2009 9:36 PM
To: Korchemny, Dmitry
Cc: Thomas.Thatcher@sun.com; sv-ac@server.eda.org
Subject: Re: [sv-ac] Proposal updated for Mantis 2656 (Ballot Comment #84)


[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.
I have version IEEE P1800/D7a
Below is the heading of Table 16.2.  I see $falling_gclk(sig),but not $falling_gclk(clk)
Perhaps I am looking at an earlier version of the P1800-2009 .
page 334:
Time $sampled(sig) $future_gclk(sig) $rising_gclk(sig) $falling_gclk(sig) $changing_gclk(sig) $steady_gclk(sig)
[Korchemny, Dmitry] You are right regarding $falling_gclk(clk). But the LRM states: Table 16-2 shows the values returned by the global clocking future sampled value functions for sig at different time moments.



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).
[Ben Cohen] I must have a misconception in the use of the @$global_clock. If my understanding is correct, if I have a portion of my design that is synchronous to one clock, I could in simulation and in formal verification declare a global clocking, and use the @$global_clock as my clocking event.  Thus, if my FF trigger on positive edge, I could state
 global clocking @ (posedge clk); endclocking
  p1: assert property (@$global_clock req |=> ack);
p1 may or may not necessarily hold on each edge of the clock.
[Korchemny, Dmitry] This is correct.

The use of "global clocking @clk; endclocking" may be implying that this is the way to use a global clocking.  Yet, from the 16.5 update: A reference to $global_clock  (see 14.14 ) is understood to be a reference to the clocking_event  defined in the global clocking  declaration. The global clock behaves just as any other clocking event. In formal verification, however, $global_clock  has additional significance, as it is considered to be the primary system clock (see F.5.1 ). Thus, in the following example
            global clocking @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 equivalent to
            assert property(@clk a);


[Korchemny, Dmitry] Note that in formal verification the global clock is the finest granularity clock and all signal changes are synchronized with it. The definition   global clocking @ (posedge clk); endclocking works if you don't have to address anything that is not synchronized by @(posedge clk). In some cases it may be reasonable, in other cases it does not work, especially when you want to reason anything about the clock itself, for example to assume that it is fair. Therefore, I think that the definition of the global clock as @clk is at least as natural as @(posedge clk).
---------------------------------------------------------------------
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.