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

Hi John,

I think that most (if not all) library assertions may be written using
'|->' only, without using '|=>', therefore your definition of next[0]
should work OK in practice.

Regards,
Dmitry 

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Friday, September 07, 2007 4:36 PM
To: Korchemny, Dmitry
Cc: john.havlicek@freescale.com; Bustan, Doron; sv-ac@eda-stds.org
Subject: 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.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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