[sv-ac] excluding emptyword matches


Subject: [sv-ac] excluding emptyword matches
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Feb 26 2004 - 13:46:36 PST


All:

Below are suggested changes to exclude empty match of a sequence that
is a property.

The current semantics "ignores" empty word matches when promoting a
sequence to a property. In other words, if s is a sequence, then as a
property s is equivalent to "s and 1'b1".

This raises the potential for backward compatibility issues if the
semantics is extended in the future to allow properties that match the
emptyword to be treated like "true".

Best regards,

John H.

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

1. Section 17.11, p. 234. Change

      1) A property that is a sequence evaluates to true if and only if
         there is a match of the sequence.

   to

      1) A property that is a sequence evaluates to true if and only if
         there is a non-empty match of the sequence. A sequence that
         admits an empty match is not allowed as a property.

2. Annex H, p. 535. Change

      Each instance of {\italic R} in this production must be a non-degenerate
      unclocked sequence. See H.3.2 and H.3.5 for the definition of non-degeneracy.

   to

      Each instance of {\italic R} in this production must be a non-degenerate
      unclocked sequence. In the "sequence" form, {\italic R} must not be
      tightly satisfied by the empty word. See H.3.2 and H.3.5 for the definitions
      of non-degeneracy and tight satisfaction.

3. Annex H, p. 535. Change

      Each instance of {\italic S} in this production must be a non-degenerate
      clocked sequence. See H.3.2 and H.3.5 for the definition of non-degeneracy.

   to

      Each instance of {\italic S} in this production must be a non-degenerate
      clocked sequence. In the "sequence" form, {\italic S} must not be
      tightly satisfied by the empty word. See H.3.2 and H.3.5 for the definitions
      of non-degeneracy and tight satisfaction.



This archive was generated by hypermail 2b28 : Fri Feb 27 2004 - 00:02:57 PST