RE: [sv-ac] mantis 1674

Hello John and all,

please find attached a corrected proposal for 1674 (also uploaded to
Mantis).

ed 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John Havlicek
> Sent: Sunday, April 08, 2007 2:08 PM
> To: sv-ac@eda-stds.org
> Subject: [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.
> 
> 

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