[sv-ac] [john.havlicek@freescale.com: my mistake]

Hi Folks:

I intended to send the message below to Ed and copy
SV-AC, but, as you can see, I copied myself twice
instead.

J.H.

------- Start of forwarded message -------
Date: Tue, 14 Aug 2007 12:59:35 -0500
To: eduard.cerny@synopsys.com
Cc: john.havlicek@freescale.com, john.havlicek@freescale.com
Subject: my mistake
From: John Havlicek <john.havlicek@freescale.com>
Reply-To: john.havlicek@freescale.com
X-OriginalArrivalTime: 14 Aug 2007 17:59:37.0202 (UTC) FILETIME=[E0DA5D20:01C7DE9C]

Hi Ed:

This is amusing.  I have been arguing why using "|->" in the 
proposal is preferable to using "##0", but in fact, now I have 
changed my mind.

In the proposal, it currently says that if E is non-empty and r 
admits empty match, then

   push(E, r |=> p) = ( k(r) (1,E) |-> r |=> push(<>,p) ) and push(E,p)

But we don't want to allow empty match on r in the first operand of 
the "and" -- because then we will not perform the declaration
assignment on the correct clock.  In the case of empty match of r, we 
need to push the declaration assignment into p, which is what the 
second operand of "and" is supposed to be doing.

So I think I have done it exactly wrong and that the definition 
should be 

   push(E, r |=> p) = ( k(r) (1,E) ##0 (r) |=> push(<>,p) ) and ( push(E,p) )

if r admits empty match.  [I also added parentheses around "push(E,p)"
to avoid interference with the "and".]

Does this make sense?

By the way, I noticed a while ago in working on this that our
definition of "semantic leading clock" is defective because in case
r admits empty match we should include the set of semantic leading clocks
of p in the set of semantic leading clocks of "r |=> p".  

I think I should fix this in 1668.  Do you agree?

J.H.
------- End of forwarded message -------

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