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

Minor Editorial change (see
http://owl.english.purdue.edu/owl/resource/607/04/ for explanation)
 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 . 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.

On Wed, Sep 21, 2011 at 12:37 PM, Seligman, Erik <erik.seligman@intel.com>wrote:

> I have uploaded a new version at
> http://www.verilog.org/mantis/view.php?id=3145, incorporating Ed’s
> suggestions.****
>
> ** **
>
> Dana- can you accept this version?****
>
> Does anyone else have comments?****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Seligman,
> Erik
> *Sent:* Tuesday, September 20, 2011 2:48 PM
> *To:* Eduard Cerny; Dana Fisman Ofek; 'sv-ac@eda-stds.org'
>
> *Subject:* [sv-ac] RE: maximal property, etc...****
>
> ** **
>
> I prefer Ed’s phrasings in green below. Dana’s version better defines the
> maximal property for a non-flattened case, but I think it makes the overall
> concept more confusing for the reader. ****
>
> ** **
>
> *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:* Dana Fisman Ofek; Eduard Cerny; 'sv-ac@eda-stds.org'
> *Subject:* [sv-ac] RE: maximal property, etc...****
>
> ** **
>
> Hi Dana,****
>
> ** **
>
> let’s see what others say…****
>
> ed****
>
> ** **
>
> ** **
>
> *From:* Dana Fisman Ofek
> *Sent:* Tuesday, September 20, 2011 5:20 PM
> *To:* Eduard Cerny; Eduard Cerny; 'sv-ac@eda-stds.org'
> *Subject:* RE: maximal property, etc...****
>
> ** **
>
> Hi Ed,****
>
> ** **
>
> The mantis item refers to 3. For that I would modify Erich proposal as
> follows:****
>
> ** **
>
> The term 'maximal property' is defined as the unique property contained in
> a given property and not contained within any other property of the given
> property. In the above ‘maximal property’ refers to the maximal flattened
> property, that is the maximal of the property obtained by applying the
> rewriting algorithm in F.4.1 to the assertion statement.****
>
> ** **
>
> Perhaps it’s better to replace the use of “maximal property” with “maximal
> flattened property” then we’ll need to twist the second sentence to say***
> *
>
> ** **
>
> The term ‘maximal flattened property’ refers to the maximal property of the
> property obtained by applying the rewriting algorithm in F.4.1 to the
> assertion statement.****
>
> ** **
>
> In the PSL LRM there is an introductory section titled “Definitions,
> acronyms, and abbreviations” where commonly used terms are introduced and
> properly defined. Perhaps we should consider adding something alike. Then we
> can define there ‘maximal property’, ‘flattened property’, and ‘maximal
> flattened property’ and remove these explanations from 16.17. Same, of
> course, for other commonly used terms.****
>
> ** **
>
> Best,****
>
> Dana****
>
> ** **
>
> ** **
>
> *From:* Eduard Cerny
> *Sent:* Tuesday, September 20, 2011 3:42 PM
> *To:* Dana Fisman Ofek; Eduard Cerny; 'sv-ac@eda-stds.org'
> *Subject:* RE: maximal property, etc...****
>
> ** **
>
> Hi Dana,****
>
> I see… so how exactly would you change (2) and (3), if at all change is
> needed?****
>
> Thanks****
>
> ed****
>
> ** **
>
> *From:* Dana Fisman Ofek [mailto:dfisman@synopsys.COM]
> *Sent:* Tuesday, September 20, 2011 3:39 PM
> *To:* Eduard Cerny; 'sv-ac@eda-stds.org'
> *Subject:* 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* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> 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* <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.