RE: [sv-ac] mantis 1674

From: Eduard Cerny <Eduard.Cerny_at_.....> Date: Mon Apr 09 2007 - 06:49:45 PDT · This archive was generated by hypermail 2.1.8 : Mon Apr 09 2007 - 06:50:55 PDT

Hello John,

I think that your notes on 1648 are not relevant anymore, please see the
attached email from TT in which he accepts the changes to 1648. (I also
attach the proposal here, it was deposited on Mantis on 04/04.) 

Please see my comments on the rest below, in summary - I will change the
text accordingly.

Best regards,
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.  

Fine.

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

OK

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

OK

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

OK

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

This has to be changed too in view of updated 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).

OK

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

OK

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

OK

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

OK

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

OK

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

This has to change too in view of 1648.

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