[sv-ac] Re: next[0] as clock alignment

Hi Dmitry:

If a clock change is not interfering with the next, then next[0] 
should behave as a no-op in most cases.  There is a strength 
difference, though, so one needs to pay attention to that.

If a clock change is interfering with the next, then I think 
that the assertion writer has to face the question of how many
nexts should precede the clock change and how many should follow.
Both can be parameterized, as in 

  @(c) r |-> next[j] @(d) next[k] p ,

where r and p have no clocks written within them.

In this form, r should not match empty, and so putting j = 0 makes
next[j] behave like a no-op because the endpoint of a match of r is
aligned with c.

The related form

  @(c) r |=> next[j] @(d) next[k] p ,

in which r might match empty, does not behave as well because 
putting j = 0 will still result in an alignment with c after
|=> rather than a change of the clock over to d.  If the assertion
writer does not want alignment with c after |=>, then 

  @(c) r ##1 1[*j] |=> @(d) next[k] p

could be coded instead to get no-op behavior when j = 0.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.20,216,1186383600"; 
>    d="scan'208";a="126800387"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 6 Sep 2007 21:11:19 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: next[0] as clock alignment
> Thread-Index: Acfu6DS/5uXQ+m16Tia70mV0soHZDQBx72rg
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 06 Sep 2007 18:12:14.0085 (UTC) FILETIME=[737DCB50:01C7F0B1]
> 
> Hi John,
> 
> My original intention was to define next[0] as no-op in order to allow
> writing parameterized properties, e.g.,
> 
> property P (p, q, n);
> 	p |-> next[n] q; // n =3D delay, n =3D 0 - no delay
> endproperty
> 
> But I think that using next[0] for clock alignment does not (almost)
> affect the ability to write parameterized properties, since
> parameterized multiclocked properties are rare. As far as I understand
> it should not be difficult to define next[0] this way. If we see that
> this is not so easy, then we can disallow next[0] in the original
> proposal, and work on its definition in a separate proposal.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Tuesday, September 04, 2007 2:39 PM
> To: Bustan, Doron; Korchemny, Dmitry
> Cc: sv-ac@eda-stds.org
> Subject: next[0] as clock alignment
> 
> Hi Doron, Dmitry:
> 
> I sent a comment yesterday about not wasting the next[0] syntax
> on a no-op and that it makes sense for this to mean clock alignment.
> 
> Dana Fisman has a technical report that discusses this topic:
> 
> http://www.wisdom.weizmann.ac.il/~dana/publicatclcks_fix.pdf
> 
> 
> J.H.

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