Hi Manisha: I think that the proposed definition of $past gives the intended value in the observed region. As a sanity check, we expect assert property (@(posedge clk) v |=> $past(v)); never to fail. Let t < t' be two time slots in which "posedge clk" occurs and such that "posedge clk" does not occur in any intermediate time slot. Suppose that the preponed value of v in t is 1. Then the return value of $past(v) changes from whatever it was before to 1 in the postponed region of t. $past(v) still returns value 1 in the observed region of t', which is what we expect. Only in the postponed region of t' will the return value of $past(v) change to whatever the preponed value of v was in t'. Best regards, John H. > X-MimeOLE: Produced By Microsoft Exchange V6.5 > Content-class: urn:content-classes:message > Date: Thu, 2 Nov 2006 11:13:41 -0800 > X-MS-Has-Attach: > X-MS-TNEF-Correlator: > Thread-Topic: [sv-ac] mantis 1550 > Thread-Index: Acb+j4hFCYP8sfsBR0avmxNqtXjgewABQSDgAAdpOpc= > From: "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com> > X-OriginalArrivalTime: 02 Nov 2006 19:13:42.0694 (UTC) FILETIME=[02D7DC60:01C6FEB3] > > This is a multi-part message in MIME format. > > ------_=_NextPart_001_01C6FEB3.02130F0F > Content-Type: text/plain; > charset="iso-8859-1" > Content-Transfer-Encoding: quoted-printable > > Hi, > > I am still confused about these statements. In the proposal it says that = > the value of $past is updated in the postponed region of the simulation = > time step in which clock tick occurred. Now, if the $past is used in the = > assertion, which value it will see: new value or old value. As per this = > statement, it should be old value (assertions are evaluated in Observe = > region) but that is not the intention (I think). =20 > > Manisha > > > -----Original Message----- > From: owner-sv-ac@server.eda.org on behalf of Rich, Dave > Sent: Thu 11/2/2006 7:53 AM > To: john.havlicek@freescale.com; sv-ac@server.eda-stds.org > Subject: RE: [sv-ac] mantis 1550 > =20 > I think the semantics of the return value of these function is no > different then the simple Verilog system function $time.=20 > > You have to distinguish between the values returned by references to the > function versus evaluation events scheduled by a processes waiting on > the event expression. This is somewhat harder to put into words than to > actually implement it. > > I think it is OK to say that the value that will be returned by the > function is updated in the postponed region because no one can schedule > a call in that region. You can also say that an update event is > scheduled for the active region of the next time slot. > > Dave > > > > -----Original Message----- > > From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] > On > > Behalf Of John Havlicek > > Sent: Thursday, November 02, 2006 6:59 AM > > To: sv-ac@server.eda-stds.org > > Subject: [sv-ac] mantis 1550 > >=20 > > Hi Ed: > >=20 > > In general, I like the semantics for $sampled and $past in your 1550 > > proposal, but I have some concerns that make me vote "no" at this > > time. > >=20 > > 1. I don't think we have yet clarified when the return values of these > > functions change. You say that $sampled is stable throughout the > > simulator timestep and that $past changes in the postponed region. > >=20 > > Can the return value of $past really change in the postponed > region? > >=20 > > I think it is bad if there can be calls/references to any of the > > sampled value functions between the point that the return value > > of one changes and the point that the return value of another > > changes in the same timestep. > >=20 > > 2. A related question is that of the semantics of events that refer > > to sampled value functions. The intuition seems to be that the > > return values of sampled value functions change "in between" the > > simulation timesteps, so when do we schedule something like > >=20 > > @($sampled(p)) S1 > >=20 > > when written in various contexts (e.g., in a module, in a program)? > >=20 > >=20 > > 3. I would like to see $rose, $fell, and $stable defined in terms of > > $sampled and $past. I think this should be easy. > >=20 > > We may need to get some SV-BC or other help with items 1 and 2. > >=20 > > Best regards, > >=20 > > John H. > > > > ------_=_NextPart_001_01C6FEB3.02130F0F > Content-Type: text/html; > charset="iso-8859-1" > Content-Transfer-Encoding: quoted-printable > > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN"> > <HTML> > <HEAD> > <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; = > charset=3Diso-8859-1"> > <META NAME=3D"Generator" CONTENT=3D"MS Exchange Server version = > 6.5.7650.28"> > <TITLE>RE: [sv-ac] mantis 1550</TITLE> > </HEAD> > <BODY> > <!-- Converted from text/plain format --> > > <P><FONT SIZE=3D2>Hi,<BR> > <BR> > I am still confused about these statements. In the proposal it says that = > the value of $past is updated in the postponed region of the simulation = > time step in which clock tick occurred. Now, if the $past is used in the = > assertion, which value it will see: new value or old value. As per this = > statement, it should be old value (assertions are evaluated in Observe = > region) but that is not the intention (I think). <BR> > <BR> > Manisha<BR> > <BR> > <BR> > -----Original Message-----<BR> > From: owner-sv-ac@server.eda.org on behalf of Rich, Dave<BR> > Sent: Thu 11/2/2006 7:53 AM<BR> > To: john.havlicek@freescale.com; sv-ac@server.eda-stds.org<BR> > Subject: RE: [sv-ac] mantis 1550<BR> > <BR> > I think the semantics of the return value of these function is no<BR> > different then the simple Verilog system function $time.<BR> > <BR> > You have to distinguish between the values returned by references to = > the<BR> > function versus evaluation events scheduled by a processes waiting = > on<BR> > the event expression. This is somewhat harder to put into words than = > to<BR> > actually implement it.<BR> > <BR> > I think it is OK to say that the value that will be returned by the<BR> > function is updated in the postponed region because no one can = > schedule<BR> > a call in that region. You can also say that an update event is<BR> > scheduled for the active region of the next time slot.<BR> > <BR> > Dave<BR> > <BR> > <BR> > > -----Original Message-----<BR> > > From: owner-sv-ac@server.eda.org [<A = > HREF=3D"mailto:owner-sv-ac@server.eda.org">mailto:owner-sv-ac@server.eda.= > org</A>]<BR> > On<BR> > > Behalf Of John Havlicek<BR> > > Sent: Thursday, November 02, 2006 6:59 AM<BR> > > To: sv-ac@server.eda-stds.org<BR> > > Subject: [sv-ac] mantis 1550<BR> > ><BR> > > Hi Ed:<BR> > ><BR> > > In general, I like the semantics for $sampled and $past in your = > 1550<BR> > > proposal, but I have some concerns that make me vote "no" = > at this<BR> > > time.<BR> > ><BR> > > 1. I don't think we have yet clarified when the return values of = > these<BR> > > functions change. You say that $sampled is = > stable throughout the<BR> > > simulator timestep and that $past changes in the = > postponed region.<BR> > ><BR> > > Can the return value of $past really change in = > the postponed<BR> > region?<BR> > ><BR> > > I think it is bad if there can be = > calls/references to any of the<BR> > > sampled value functions between the point that = > the return value<BR> > > of one changes and the point that the return = > value of another<BR> > > changes in the same timestep.<BR> > ><BR> > > 2. A related question is that of the semantics of events that = > refer<BR> > > to sampled value functions. The intuition = > seems to be that the<BR> > > return values of sampled value functions change = > "in between" the<BR> > > simulation timesteps, so when do we schedule = > something like<BR> > ><BR> > > @($sampled(p)) S1<BR> > ><BR> > > when written in various contexts (e.g., in a = > module, in a program)?<BR> > ><BR> > ><BR> > > 3. I would like to see $rose, $fell, and $stable defined in terms = > of<BR> > > $sampled and $past. I think this should be = > easy.<BR> > ><BR> > > We may need to get some SV-BC or other help with items 1 and 2.<BR> > ><BR> > > Best regards,<BR> > ><BR> > > John H.<BR> > <BR> > <BR> > </FONT> > </P> > > </BODY> > </HTML> > ------_=_NextPart_001_01C6FEB3.02130F0F--Received on Thu Nov 2 11:54:16 2006
This archive was generated by hypermail 2.1.8 : Thu Nov 02 2006 - 11:54:25 PST