[sv-ac] RE: Q: Mantis 3145: define 'maximal property'?

Hi Erik,

should it be little more detailed? e.g., ... is a top-level property expression after applying rewriting algorithm. That expression is thus not contained in any other property expression in the assertion.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik
Sent: Friday, August 19, 2011 5:54 PM
To: sv-ac@eda-stds.org
Subject: [sv-ac] Q: Mantis 3145: define 'maximal property'?

In Mantis 3145 (http://www.verilog.org/mantis/view.php?id=3145 ) , we see that 'maximal property' is used in several places but not properly defined. I think it would be good to try to fix this. Here are the usages:

[16.17]
(c) A contextually inferred clocking event from a procedural block supersedes a default clocking event.
The contextually inferred clocking event is treated as though it had been written as the leading
clocking event of any concurrent assertion statement to which the inferred clock applies. The
maximal property of such a concurrent assertion statement shall be singly clocked.
...
(e) A multiclocked sequence or property can inherit the default clocking event as its leading clocking
event. If a multiclocked property is the maximal property of a concurrent assertion statement, then
the property shall have a unique semantic leading clock (see 16.17.1).

(f) If a concurrent assertion statement has no explicit leading clocking event, there is no default
clocking event, and no contextually inferred clocking event applies to the assertion statement, then
the maximal property of the assertion statement shall be an instance of a sequence or property for
which a unique leading clocking event is determined.
...
c4: cover property (s3 ##1 b);
// illegal: no default, inferred, or explicit leading
// clocking event and maximal property is not an instance

So, it looks to me like the concept is that the maximal property is the property in an assertion statement which is not itself contained in any other property. Is this a good enough basis for a definition, or do we need something more formal here?

--
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.