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

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 = delay, n = 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] 
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.