RE: [sv-ac] RE: Call to vote. Due July 26

Hi John,

that's exactly what I was hoping that it is preserved, that the example is illegal. However, from reading the text as modified, it is not obvious that the requirement for the assertion to have a unique semantic leading clock is preserved. Or is it?

Thanks,
ed

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Wednesday, July 21, 2010 2:06 PM
To: Eduard Cerny; sv-ac@eda.org
Subject: RE: [sv-ac] RE: Call to vote. Due July 26

Hi Ed:

The change in 3147 is supposed to remove the restriction that requires a procedural concurrent assertion to be _singly_ clocked.

It is not supposed to affect the requirement that a concurrent assertion have a unique semantic leading clock.

I would say that the example you show is illegal because, despite the inferred clock, the top-level (i.e., maximal) property does not have a unique semantic leading clock. The two semantic leading clocks are "posedge clk1" and "posedge clk2"; the inferred clock plays no role in the semantic leading clocks because it is overridden.

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Eduard Cerny
Sent: Wednesday, July 21, 2010 11:32 AM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: [sv-ac] RE: Call to vote. Due July 26

SVDB 2491 __X_Yes ___No
http://www.eda-stds.org/mantis/view.php?id=2491
Vote to resolve as "No change required"

SVDB 3147 ___Yes _N__No
http://www.eda-stds.org/mantis/view.php?id=3147
http://www.eda-stds.org/mantis/file_download.php?file_id=4429&type=bug

The text in 16.15.6 says:
When a pending procedural assertion instance matures, if the current time step is one that corresponds to that
assertion instance's leading clocking event, an evaluation attempt of the assertion begins immediately within
the Observed region. If the assertion's leading clocking event has not occurred in this time step, the matured
instance shall be placed on the matured assertion queue, which will cause the assertion to begin an
evaluation attempt upon the next clocking event that corresponds to the leading clocking event of the
assertion.

So this does imply a unique leading clock. The question is then what is understood under the term "maximal property" Is it one with the inferred clock inlined, or is it one in the assertion before the inferred clock is inlined? If the latter, how is the following to evaluate?

always @(posedge clk)
A: assert property ((@(posedge clk1) x until y) or (@(posedge clk2) w));

since "or" has no "inherited clock" and the max property does not have a single leading clock, how is it to start on posedge clk?

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