RE: [sv-ac] 1731

Hi John,

I think that the semantic definition of $past requires some trivial
rewriting to deal with this enhancement.

Here is the current definition:

E.4.2 Past

w denotes a nonempty finite or infinite word over \Sigma, and j denotes
an integer so that 0 <= j < |w|.
- Let n >= 1. If there exist 0 <= i < j so that w^{i, j} , {}, {} \tight
(c ##1 c [->n - 1]), then @(c)$past(e, n)[w^j] = e[w^i]. Otherwise,
@(c)$past(e, n)[w j] has the value x.
- $past(e) == $past(e,1) .

This definition does not deal with the full syntax of $past, but always
assumes that the clock is implicit. We can rewrite $past definition with
an explicit clock: $past(e, n, clk) and make the context inference pure
syntactic, so that the semantic definition does not deal with the clock
propagation for $past. Then we will have:

E.4.2 Past

w denotes a nonempty finite or infinite word over \Sigma, and j denotes
an integer so that 0 <= j < |w|.
- Let n >= 1. If there exist 0 <= i < j so that w^{i, j} , {}, {} \tight
(c ##1 c [->n - 1]), then $past(e, n, c)[w^j] = e[w^i]. Otherwise,
$past(e, n, c)[w j] has the value x.
- $past(e) == $past(e,1) .

This definition actually means that clock of $past is independent of the
property clock, and that $past is evaluated according its own clock. I
cannot see any semantic discontinuity here, never mind what the clock
patterns are.

1698 may formalize the simulation semantics of $past, but whatever
decision is taken for 1698, it won't affect the consistency of the clock
changes in $past described in this item.
 
Thanks,
Dmitry

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Thursday, March 15, 2007 2:01 PM
To: Korchemny, Dmitry
Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
Subject: 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.