[sv-ac] mantis 1674

Ed & All:

I went carefully through the proposal for mantis 1674, and I 
don't think it's ready for a vote yet.  It has dependencies on
1648, and I don't think the resolutions to the issues with 1648
have been propagated to 1674.

I also have a number of editorial suggestions.  See the notes 
below.

Best regards,

J.H.

Notes on inferred_1674_070314.pdf
---------------------------------

QUESTIONS:

* Why is the inferred enabling condition for a3 just d rather than
  !rst && d?  Reducing to d seems like an optimization.

* Has this proposal been aligned with 1648?  I am oncerned about
  whether it has been adjusted according to the discussion in our
  meeting of 2007-03-20:

  - 1648:  Default disable [EC]
    . TT reviewer.
    . TT:  only sensitivity list of always block is used to
      infer, not the logical structure of the enablers in the block.  
    . EC:  restricting to always_ff makes it easier to address
      concerns of TT.
    . EC:  For clock inference, current rule takes first event
      expression.  May need to change this definition.
    . EC will revise to remove inference of disable iff from always
      blocks (any of them), and TT will re-review.

  These concerns seem relevant to this proposal and do not seem to
  have been resolved.


EDITORIAL CONCERNS:

* Throughout, change

     inferred value function 

  to

     inferred expression function 

  RATIONALE:  I think it is confusing to call these "inferred value functions"
  because they are really returning expressions rather than the values of
  expressions.  

* Change

     The following elaboration time system functions are available to
     query the inferred value of the clock event, reset and enable signals.

  To


     The following elaboration time system functions are available to
     query the inferred clock event expression, disable expression, and enable
     condition.

   RATIONALE: Consistency and clarity of language.  I think that it is
   not the values of these expressions that are returned, but the
   expressions themselves (or copies of, or representations of, the
   expressions).  I'm not sure whether "condition" can be used
   interchangeably with "expression", but we should try to be
   consistent.  I think 1648 needs to be reviewed for consistency.

* Change

    - $inferred_clock returns the value of the inferred clock event.
    
    - $inferred_disable returns the value of the inferred disable expression.
    
    - $inferred_enable returns the value of the inferred enable condition.

  To

    - $inferred_clock returns the inferred clock event expression.
    
    - $inferred_disable returns the inferred disable expression.
    
    - $inferred_enable returns the the inferred enable condition.

* Change

     Inferred clock corresponds to the current resolved event
     expression that can be used in a clocking event definition. It is
     obtained by applying clock flow rules to the point where
     $inferred_clock is called. If there is no inferred event
     expression, $inferred_clock returns false (i.e., 1'b0).o

  To

     The inferred clock event expression is the current resolved event
     expression that can be used in a clocking event definition.  It is
     obtained by applying clock flow rules to the point where
     $inferred_clock is called.  If there is no current resolved
     event expression, then $inferred_clock returns false (i.e., 1'b0).

  RATIONALE:  Consistency and clarity of language.  You are defining "inferred 
  clock event", so I think it is confusing to say "If there is no inferred 
  event expression".

* Change

    Inferred disable expression is either the reset condition inferred
    from an always block with asynchronous reset or the default
    disable value (See 17.14 Note to editor: This is after introducing
    the proposal #1648).

  To

    The inferred disable expression is either the reset expression inferred
    from an always block with asynchronous reset or the default
    disable expression (See 17.14 Note to editor: This is after introducing
    the proposal #1648).

  RATIONALE: Consistency and clarity of language.  I think that if it
  is an "inferred disable expression", then we should try to use the
  word "expression" consistently rather than "condition" or "value".
  1648 should be reviewed in this regard.

* Change

    Inferred enable condition returned by $inferred_enable is the
    inferred condition from an always or initial block if one exists,
    the same as the condition inferred in verification statements
    placed in an if...else or a case statement (see 17.13.5). It is
    true (i.e., 1'b1) when no condition can be inferred.

  To

    The inferred enable condition is the expression defining the
    cumulative condition required to reach the current point within
    enveloping if...else and case blocks inside an always or initial
    block.  This is the same as the contextually inferred enabling
    condition for verification statements (see 17.13.5).  If there are
    no enveloping if...else or case blocks, then the cumulative
    condition is true (i.e., 1'b1).

* Change

    When a inference system function is used as the default value on a
    formal argument to a property or sequence, it is replaced by the
    inferred value at the point where the property or sequence is
    instantiated.

  To

    When an inferred expression system function is used as the default
    value on a formal argument to a property or sequence, it is
    replaced by the inferred expression at the point where the
    property or sequence is instantiated.

* Change

     property p_triggers(start_event, end_event, form, clk = $inferred_clock,
                       rst = $inferred_disable, en = $inferred enable);

  To

     property p_triggers(start_event, end_event, form, clk = $inferred_clock,
                       rst = $inferred_disable, en = $inferred_enable);

  RATIONALE:  "$inferred enable" needs the underscore.

* Change

    In assertion a2 the clock event posedge clk1 is passed explicitly
    to the property p_triggers, therefore no default value is inferred
    for it.

  To

    In assertion a2 the event expression posedge clk1 is passed to the 
    formal argument clk in the instance of property p_triggers.  Therefore, 
    the default  $inferred_clock is not used for clk in that instance.

* Change

    In assertion a3 the clock event is inferred from the control event
    of the always block

  To

    In assertion a3 the clock event is inferred from the event control
    of the always block

  RATIONALE: I think the phrase "event control" is used in the LRM
  rather than "control event".

 
* Change

    The disable condition rst1 is inferred for assertion a1 from the
    default disable statement, and the disable condition rst is
    inferred for assertion a3 from the always block.

  To

    The disable condition rst1 is inferred for assertion a1 from the
    default disable statement, and the disable condition rst is
    inferred for assertion a3 from the asynchronous reset posedge rst
    in the event control of the always block.

  RATIONALE:  Clarity.

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