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