[sv-ac] RE: maximal property, etc...

Hi Ed, Erik,

I am not clear on why we should tie the definition of maximal xxxx with a flattened / unwrapped xxxx.

I think the two are orthogonal. One can consider the maximal singly clocked property of the assertion as written by the user or alternatively consider the maximal singly clocked property of the assertion obtained by applying rewriting algorithms from Annex F. For item (2) below, for instance, it does not matter. As the point is that it does not admit empty matches. Since the flattened property is equivalent to the unflattened property it the flattened does not admit empty matches so does the original.

I think that a maximal expression of type xxxx should be defined (borrowing from proposal in 3145) as the unique expression of type xxxx contained in the assertion statement and not contained within any other expression of type xxxx in the assertion statement.

If at certain places in the LRM we care about the maximal flattened expression, then we should use "maximal flattened expression (of type xxxx)" or "maximal expression (of type xxxx) obtained after applying rewrite rules in F.yyy"

Best,
Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Eduard Cerny
Sent: Tuesday, September 20, 2011 2:38 PM
To: 'sv-ac@eda-stds.org'
Subject: [sv-ac] maximal property, etc...

Hi,

I was supposed to look at the definition of maximal property, so just a couple of ideas for now:

- there are several uses of "maximal":

1. maximal Boolean: in 16.10 in relation to triggered

2. maximal singly clocked subsequence: in 16.14.1 Multiclock sequences

3. maximal property: in 16.17 Clock resolution

(1) has a sort of definition in the subsequent sentence: The application of triggered to this instance is a maximal Boolean expression. In other words, the application of triggered cannot have negation or any other expression operator applied to it.
We could leave that one as is.

(2) We could add the following sentence before "When concatenating differently clocked sequences, the maximal singly clocked subsequences are required..." on pp 386:
In the following statements, the term 'maximal singly clocked subsequence' refers to the largest singly clocked sequence appearing in a multiclock sequence resulting from the application of the rewriting algorithm in F.4. That is, such a sequence cannot be enlarged by absorbing any surrounding operators and their arguments without changing the singly clocked sequence into a multiclock sequence or to a property.

(3) Borrowing from the proposal in 3145 and slightly simplifying it: The term 'maximal property' in the above rules is defined as the unique flattened property contained in the assertion statement and obtained by applying the rewriting algorithms in F.4.

I do not think that we should go into more detail, as it can get rather complicated.... see John's comment.

Best regards
ed

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.