RE: [sv-ac] review of 2168

Hi John,

Please, see my comments below. I am attaching the updated version of the
proposal.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Sunday, January 27, 2008 9:08 PM
To: Korchemny, Dmitry; sv-ac@server.eda.org
Subject: [sv-ac] review of 2168

Hi Dmitry:

I read 2168 and wrote the comments below.

J.H.

2008-01-27:  Review of 2168
---------------------------

Major Comment:

* My main negative feedback is that I am not very comfortable fixing
this as the
  definition of the transformation from SystemVerilog clocking events to
Annex F.

  I understand that if you want to define this transformation of
clocking events 
  in terms of global clocking and account for sampled values in such a
way that you
  get the right thing for 

     assert property(@(posedge clk) clk);

  then you will be led to the proposed definition.

  In the past we have left this transformation undefined because it
involves
  certain choices about how to handle changing value events (changing in
terms
  of what?) and how to handle sampled values.  Under differing
circumstances,
  different choices for the transformation might be intuitive and
appropriate.

  For example, if all assertions are clocked @(posedge clk), one might
make a 
  transformation where the abstract assertion is clocked @1 and each
letter
  of an input word represents the sampled values @(posedge clk) of the
various
  variables referenced in the assertions.

  I think that the proposed definition says that the global clock must
be strictly
  finer than all other expression-based clocking events, because they
will only
  have events when there are changes with respect to the global clock.
I don't 
  think that this is something that was already specified in the global
clock proposal.

  I would be happier if the proposed transformation were represented as
one possibility,
  but in a non-normative way.

[Korchemny, Dmitry] I think that having an explicit definition of the
transformation from the edge sensitive clocks to the level sensitive
clocks is important, since the current specification in Annex F may be
confusing. When I started learning SVA I was sure that assert
property(@1 a); means that a is always true, and it took to me a couple
of months to understand that this was not the case. Moreover, there are
EDA vendors who understood SVA semantics this way, and made a
corresponding implementation.

[Korchemny, Dmitry] I don't think that the current proposal prevents an
implementation from abstracting @(posedge clk) internally when this is
legal.

[Korchemny, Dmitry] assert property(@(posedge clk) clk);

[Korchemny, Dmitry] should be legal, and it fits our intuition: before
the rising clock the value of clk is false, and therefore this assertion
should fail.

[Korchemny, Dmitry] This proposal is talking only about formal semantics
in Annex F, and not about the simulation semantics. The formal semantics
of the global clock is a reference clock, therefore @$global_clock is
@1, as was explicitly stated in the global clocking proposal. It was
also stated there that there were no additional conditions imposed on
the synchronization of other clocks with the global clock in simulation.


Other Comments:

* Currently in Annex F, we write @(b) where b is understood to denote a
  boolean expression.  I think that the language of this proposal should
  mesh better with what is already there.  

  The proposal starts by saying that in Annex F, "the clock controls are

  considered level-sensitive".  I think that what is accurate is to say
  that the clock controls are considered to be "boolean conditions" or
  "boolean functions on the input alphabet".

[Korchemny, Dmitry] Fixed: "level-sensitive" -> "boolean functions on
the input alphabet".

* I'm not sure it is accurate to say that @c designates an
edge-sensitive event
  control.  We should avoid language that is conflicting with 9.4.2.
  "Value-change sensitive" seems more accurate and aligned with 9.4.2.

  One may want to avoid making general motivational statements that
might
  not be 100% accurate.

[Korchemny, Dmitry] Done.

* The rules for \tau do not deal with all cases.  Note that we have 

     clocking_event ::= 
          @ identifier
        | @ ( event_expression )
     
     event_expression^{37} ::=
          [ edge_identifier ] expression [ iff expression ]
        | sequence_instance [ iff expression ]
        | event_expression or event_expression
        | event_expression , event_expression
        | ( event_expression )
     
     edge_identifier ::= posedge | negedge

  According to 9.4.2, only the lsb is considered in posedge/negedge, so
it seems
  one would want to generalize to something like
 
     \tau(e) = $changing_gclk(e) for e \not= $global_clock
     \tau(posedge e) = $rising_gclk(lsb(e))
     \tau(negedge e) = $falling_gclk(lsb(e))

[Korchemny, Dmitry] The proposed definition should be correct since
$rising_gclk and $falling_gclk take only lsb(e) into account.

* This proposal does not handle the case of declared events.  E.g.

     event foo;
     
     // some other code determines when foo is triggered
     
     a_foo_bar:  assert property(@(foo) bar);

  I don't think it is correct to transform @(foo) to
$changing_gclk(foo).

[Korchemny, Dmitry] No, this proposal does not handle the case of
declared events and for them the transformation @(foo) to
$changing_gclk(foo) is incorrect. I added the following bullet:

- \tau(e) = $future_gclk(b), for a named event e (see 15.5), and for a
dummy bit variable b associated with the event e, such that b has value
1 in the time slots when the event e is triggered, and value 0 in all
other time slots.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, 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.