Re: [sv-ac] 1731

Hi Dmitry:

> 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 =3D $past(sig,,,@fast_clk);
> assert property(@(posedge clk) ##1 sample |-> rejecton(psig) 1'b1[*4]);

This is one way of defining the semantics, and this
way makes 1731 dependent on 1698.

The question still remains of whether there is
a semantic discontinuity in the original form

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

as you let fast_clk --> posedge clk.

There is also the possibility fast_clk is
not identical as event to posedge clk, but
at some points fast_clk and posedge clk 
occur simultaneously.  I would like to see how
the semantics behaves in such cases.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,288,1170662400"; 
>    d="scan'208"; a="210052663:sNHT45208401"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 15 Mar 2007 13:44:01 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1731
> thread-index: Acdmcz0QPxBWCfbtS3CLUqiHzpw/9wAgfb7w
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 15 Mar 2007 11:44:15.0509 (UTC) FILETIME=[4216BC50:01C766F7]
> 
> 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 =3D $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=20
> resolution.
> 
> I'm not saying we shouldn't have this relaxation, but=20
> 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=20
> latter case whether there is a semantic discontinuity.
> 
> Should this proposal depend on a resolution to 1698?
> 
> J.H.
> 
> --=20
> 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.