[sv-ac] RE: using |-> rather than ##0

Hi John,

Thank you.  but apart from the emptiness of the antecedent, the main
difff is that the formulation is simpler with |-> and mor eintuitive.
Correct?

best...
ed


> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com] 
> Sent: Tuesday, August 14, 2007 12:42 PM
> To: eduard.cerny@synopsys.COM
> Cc: sv-ac@eda-stds.org
> Subject: using |-> rather than ##0
> 
> Hi Ed:
> 
> You asked before about why the 1668 proposal for Annex F
> uses |-> rather than ##0.
> 
> I said that I don't think there is any difference, but 
> I was wrong and I actually thought about this before.
> 
> I think that |-> is preferable when combining with |=>
> because |=> does not require the antecedent to match 
> non-empty.  Another point is that the associativity
> is counterintuitive with ##0.
> 
> I wrote some notes back in July using only the 
> unclocked semantics.  I've copied them below.
> 
> J.H.
> 
> -------------------------------
> 2007-07-06
> 
> Q:  What is the difference between 
> 
>   1 |-> r |-> p  and  1 ##0 r |-> p
> 
> ?
> 
> Recall that neutral satisfaction is not defined for the empty word.
> Let |w| > 0.
> 
> w |= 1 |-> r |-> p
> iff  w |= r |-> p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r, yz |= p
> 
> w |= 1 ##0 r |-> p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and xy |== 1 ##0 
> r, yz |= p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r, yz |= p
> iff  w |= r |-> p
> 
> 
> -------------------------------
> 2007-07-05
> 
> Q:  What is the difference between 
> 
>   1 |-> r |=> p  and  1 ##0 r |=> p
> 
> ?
> 
> Using old semantics of |=> (unclocked)
> --------------------------------------
> 
> Recall that neutral satisfaction is not defined for the empty word.
> Let |w| > 0.
> 
> w |= 1 |-> r |=> p
> iff  w |= r |=> p
> iff  w |= r ##1 1 |-> p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and  xy |== r ##1 
> 1, yz |= p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and  x |== r, yz |= p
> iff  for all u,v s.t. w = uv and |v| > 0 and  u |== r, v |= p
> 
> w |= 1 ##0 r |=> p
> iff  w |= (1 ##0 r) ##1 1 |-> p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and xy |== (1 ##0 
> r) ##1 1, yz |= p
> iff  for all x,y,z s.t. w = xyz and |y| = 1 and x |== (1 ##0 
> r), yz |= p
> iff  for all u,v s.t. w = uv and |u| > 0 and |v| > 0 and  u 
> |== r, v |= p
> 
> Thus, for |w| > 0, the formulation
> 
>    1 |-> r |=> p
> 
> is preferable.
> 
> 
> Using new semantics of |=> (unclocked)
> --------------------------------------
> 
> Recall that neutral satisfaction is not defined for the empty word.
> Let |w| > 0.
> 
> w |= 1 |-> r |=> p
> iff  w |= r |=> p
> iff  [new semantics of |=>]
>      for all x,y s.t. w = xy and x |== r, y |= p
> 
> There is something potentially ill-defined here, since we 
> have not required
> |y| > 0 when we make inductive reference to y |= p.
> 
> w |= 1 ##0 r |=> p
> iff  [new semantics of |=>]
>      for all x,y s.t. w = xy and x |== 1 ##0 r, y |= p
> iff  for all x,y s.t. w = xy and |x| > 0 and x |== r, y |= p
> 
> Again, there is something potentially ill-defined here, since 
> we have not 
> required |y| > 0 when we make inductive reference to y |= p.
> 
> Thus, for |w| > 0, the formulation
> 
>    1 |-> r |=> p
> 
> is preferable.
> 
> 

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