[sv-ac] notes on 1648

From: John Havlicek <john.havlicek_at_.....>
Date: Mon Apr 30 2007 - 06:40:26 PDT
All:

1648 currently has a negative vote.

I looked over the proposal and made some notes.  See below.
I think we will need to try to address some of these points
before voting again.

J.H.

JH Notes on 1648:  2007-04-30
-----------------------------

. The text says:

     Only one default disable can be specified in a module, interface, or
     program. Specifying a default disable more than once in the same
     module, interface, or program shall result in a compilation error.
     
     A default disable is valid only within the scope containing the
     default disable specification. This scope includes the module,
     interface or program that contains the declaration as well as any
     nested modules or interfaces. It does not include instantiated modules
     or interfaces.

  Question:  If there are nested module or interface declarations, can each
  module or interface have a default disable?  Or is this a violation of the
  "only one default disable" rule?  

  I would expect the default disable to be allowed in a nested
  declaration and to override an outer default disable, but the
  description would need to be clarified.  Alignment with the scoping
  of default clocking should be checked.

. Lisa asked whether default disable applies to assertions before the 
  default disable.  My reading of 

     A default disable is valid only within the scope containing the
     default disable specification. This scope includes the module,
     interface or program that contains the declaration as well as any
     nested modules or interfaces.

  says that the answer is "yes", the default disable applies to preceding
  assertions in the same module.  The scoping should be aligned with that
  of default clocking.

  Lisa also asked whether the default disable applies to assertions within 
  generate scopes within a module.  I think the same text says "yes".

. Change

     The following rules apply for the reset resolution:

  to

     The following rules apply for the disable resolution:

  Rationale:  The section title is "Disable resolution".


. The following appears in module examples_without_default:

     // Only enable condition and clocking event are inferred from an always block
     // Assertion a8 is equivalent to @(posedge clk) !rst |-> (a |=> b)
     
     always @(posedge clk or posedge rst)
     if (rst)
        ...
     else begin
        a8 : assert property ( a |=> b);
        ...
     end

  Should there be a similar example in module examples_with_default?  

  Also, there has been some discussion of the the inference of the
  enabling condition when 4-state values are considered and alignment
  with Verilog if..else semantics.

  Jonathan Bromley has suggested a formulation like

     !(bit'(rst != 0)) |-> (a |=> b)

  rather than 

     !rst |-> (a |=> b)

  in order to align the semantics with Verilog if..else.  This alignment
  may require changes to the discussion of inferred enabling conditions
  in 17.13.5.

  In the discussion, Jonathan Bromley suggested changing the order-based
  clock inference in 17.13.5:

     The existing 1800-2005 clock inference rule that appeals to the
     *ordering* of the event control is absurd.

     The inference of clock and reset in such a block is [can be made]
     straightforward:
     
     * pos[neg]edge delay control on a signal that does not
       otherwise appear in the logic: it's a clock
       (and, presumably, there should be only one such);
     * pos[neg]edge delay control on a signal that's used
       to conditionally enable some assignments to outputs:
       it's an asynchronous reset (or preload, if tools 
       and target technology support it).

  Will this be addressed in some other Mantis item?



-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon Apr 30 06:40:45 2007

This archive was generated by hypermail 2.1.8 : Mon Apr 30 2007 - 06:40:58 PDT