[sv-champions] a few more comments on 2173

Hi Yaniv:

Below are my complete comments on 2173.  I have repeated the 
first one, which I sent yesterday.

J.H.

   . There are some semicolon problems that need to be fixed.  

     1. When property_spec is used in a concurrent assertion statement,
        no semicolon is required.  This needs to be preserved for
        backward compatibility.  Under this proposal, a semicolon is
        required for the property_statement form "property_expr ;".
     
     2. In a property declaration, there is an explicit ";" after the
        property_spec.  This proposal will result in two semicolons when
        the property_statement has the form "property_expr ;".
     
     A possible solution is to have both property_spec and property_statement_spec,
     where the former is unchanged, i.e.
     
        property_spec ::= [clocking_event] [disable iff (expression_or_dist)] property_expr
     
     and the latter requires a property_statement in place of the property_expr.
     Then use property_spec in the assertion statements (unchanged) and use 
     property_statement_spec in the property declaration, getting rid of the 
     explicit semicolon there.

   . In the discussion of non-vacuous evaluation, the definition for vacuous
     vs. non-vacuous of case without default needs to be tight.  This can be 
     done as follows:

     CHANGE

        An evaluation attempt of a property of the form 
  
           case (expression_or_dist) 
              expression_or_dist1: property_stmt1
              expression_or_dist2: property_stmt2 
              default: property_stmt3
           endcase 

        is non-vacuous iff either (expression_or_dist === expression_or_dist1)
        and the underlying evaluation attempt of property_stmt1 is non-vacuous,
        or (expression_or_dist !== expression_or_dist1 && expression_or_dist ===
        expression_or_dist2) and the underlying evaluation attempt of
        property_stmt2 is non-vacuous, or (expression_or_dist !==
        expression_or_dist1 && expression_or_dist !== expression_or_dist2) and
        the underlying evaluation of property_stmt3 is non-vacuous.

     TO

        An evaluation attempt of a property of the form 
  
           case (expression_or_dist) 
              expression_or_dist_1: property_stmt_1
              ...
              expression_or_dist_n: property_stmt_n 
              [default: property_stmt_d]
           endcase 

        is non-vacuous iff either (expression_or_dist === expression_or_dist_1)
        and the underlying evaluation attempt of property_stmt_1 is non-vacuous,
        or (expression_or_dist !== expression_or_dist1 && expression_or_dist ===
        expression_or_dist_2) and the underlying evaluation attempt of
        property_stmt_2 is non-vacuous, or ... , or the default is present and
        (expression_or_dist !== expression_or_dist_1 && expression_or_dist !==
        expression_or_dist_2 && ... && expression_or_dist !== expression_or_dist_n) 
        and the underlying evaluation of property_stmt_d is non-vacuous.

     By doing this, the statement about a case without default being vacuous "if
     (but not only if)" follows from this definition rather than being an
     independent and incomplete definition.  You might want to start that
     sentence with "Therefore".
 
     By the way, I think that setting the case off with code formatting as I
     show above is much better than streaming it in the paragraph.

   . I recommend changing

        The set of semantic leading clocks of case (b) b_1:q_1 ... b_n:q_n
        default: q_d endcase is {inherited}.

     to

        The set of semantic leading clocks of case (b) b_1:q_1 ... b_n:q_n
        [default: q_d] endcase is {inherited}.

     In other words, show the default as optional so that the definition is
     complete.

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