RE: [sv-ac] 1731

Hi John,

This feature is useful for instance in different kinds of stability
assertions, at least in conjunction with rejecton operator. Here is an
example:

assert property(@(posedge clk) ##1 sample |->
rejecton($past(sig,,,@fast_clk)) 1'b1[*4]);

The assertion is controlled by posedge clk, while $past is written
relative to the fast clock.

There should be no semantic issues with this relaxation, because it is
pure syntactic. You can just rewrite it as:

bit psig;
always psig = $past(sig,,,@fast_clk);
assert property(@(posedge clk) ##1 sample |-> rejecton(psig) 1'b1[*4]);

The issue becomes important for library assertions.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Wednesday, March 14, 2007 9:57 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] 1731

Hi Ed:

I've looked at 1731 and I don't understand the intended
semantics when the clock of the sampled value function
is not the same as the clock determined from clock 
resolution.

I'm not saying we shouldn't have this relaxation, but 
I think we need to say more about what it means.  This
should cover the possibility that the two clocks become
simultaneous or identical, and we should check in the 
latter case whether there is a semantic discontinuity.

Should this proposal depend on a resolution to 1698?

J.H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.