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

Hi Ed,

In 2, the phrase is:

"A multiclocked sequence has well-defined starting and ending clocking events and well-defined clock
changes because of the restriction that maximal singly clocked subsequences not match the empty word. If
clk1 and clk2 are not identical, then the sequence"

So the assumption is that you are given a multi clocked sequences, and thus the restriction does apply.

Anyway, my point is that there are two things (1) maximality of expression and (2) flattening of properties.
In many places we look at the result of first flattening and then taking the maximal expression. That is perfectly fine.
What I am saying is that the definitions need not be combined. Each should be defined separately. If at certain points the LRM refers to the results of doing both, then it can be easily stated and understood. Its defining them together that leads to confusion of the definition and the intent.

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.