[sv-ac] change requests for my AIs.

Surrendra:

Below are the change requests for my action items from Monday's SV-AC
meeting.

Best regards,

John H.

============================================

1. We need an explanation of the attachment of sequence_match_item
   in a first_match. Add the following text to the end of Section 17.7.7:

      Sequence match items can be attached to the operand sequence of the
      {\courierbold first_match} operator. The sequence match items are
      placed within the same set of parentheses that encloses the operand.
      Thus, for example, the local variable assignment {\courier x = e}
      can be attached to the first match of {\courier seq} via
   
          {\courierbold first_match} {\courier (seq, x = e)}
   
      which is equivalent to
   
          {\courierbold first_match}{\courier ((seq, x = e))}
   
      See Sections 17.8 and 17.9 for discussion of sequence match items.

2. Discussion of implication belongs in Section 17.11 on properties,
   not in Section 17.7 on sequences.
 
   a. Move Section 17.7.11 to Section 17.11.1 and make it start after the
      following sentence in Section 17.11, p. 242:

         Nesting {\courierbold disable iff} clauses, explicitly or through
         property instantiations, is not allowed.

   b. Create a new Section "17.11.2 Property examples". It will be all the text
      beginning from the following sentence in Section 17.11 on p. 242:

         This allows for the following examples:

      and continuing up to, but not including, the old Section
      "17.11.1 Recursive properties".

   c. Change the first sentence of the new Section "17.11.2 Property examples"
      from

         This allows for the following examples:

      to

         The following examples illustrate the property forms.

   d. In Section 17.11, p. 241, last sentence of item 6). Change

         The meaning of implications has already been discussed in 17.7.11.

      to

         The meaning of implications will be discussed below in 17.11.1.

   e. Change the number of Section "17.11.1 Recursive properties" to
      "17.11.3 Recursive properties".

3. LRM discussion of finite trace semantics.
   Add the following section after Section "17.11.3 Recursive properties":

      17.11.4 Finite-length versus infinite-length behavior
      
      The formal semantics in Annex H defines whether a given property
      holds on a given behavior. How the outcome of this evaluation
      relates to the design depends on the behavior that was analyzed.
      In dynamic verification only behaviors that are finite in length
      are considered. In such a case, SystemVerilog defines four levels
      of satisfaction of a property:
      
      Holds strongly:
      
        -- no bad states have been seen
        -- all future obligations have been met
        -- the property will hold on any extension of the path
      
      Holds (but does not hold strongly):
      
        -- no bad states have been seen
        -- all future obligations have been met
        -- the property may or may not hold on a given extension of the path
      
      Pending:
      
        -- no bad states have been seen
        -- future obligations have not been met
        -- the property may or may not hold on a given extension of the path
      
      Fails:
      
        -- a bad state has been seen
        -- future obligations may or may not have been met
        -- the property will not hold on any extension of the path

4. Check non-degeneracy discussion in LRM text and Formal Semantics.
   Add the following section after Section "17.11.4 Finite-length
   versus infinite-length behavior":

      17.11.5 Non-degeneracy

      It is possible to define sequences that can never be matched.
      For example:

         {\courier (1'b1)} {\courierbold intersect} {\courier (1'b1} {\courierbold ##1} {\courier 1'b1)}

      It is also possible to define sequences that admit only empty matches.
      For example:

         {\courier 1'b1[*0]}

      A sequence that admits no match or that admits only empty matches
      is called {\italic degenerate}. A sequence that admits at least
      one non-empty match is called {\italic non-degenerate}. A more
      precise definition of non-degeneracy is given in Annex H.

      The following restrictions apply:

      1. Any sequence that is used as a property must be non-degenerate.
      2. Any sequence that is used as the antecedent of an overlapping
         implication ({\courierbold |->}) must be non-degenerate.
      3. Any sequence that is used as the antecedent of a non-overlapping
         implication ({\courierbold |=>}) must admit at least one match.
         Such a sequence can admit only empty matches.

      The reason for these restrictions is that the use of degenerate
      sequences the forbidden ways results in counterintuitive property
      semantics, especially when the property is combined with a
      {\courierbold disable iff} clause.

5. Annex H, Section H.3.3.2, p. 549. To align with the text above, change

      "pending" or "holds weakly" otherwise

   to

      "pending" or "holds (but does not hold strongly)" otherwise
Received on Wed Mar 10 14:37:52 2004