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

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

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

* 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))

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

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