[sv-ac] example showing problem when not uniquefying

Hi Dmitry:

I had an action item to send an example showing what might go wrong
with the things I added to the 1549 formal document if we don't
uniquefy the local variable identifiers.

See the notes attached.

The good thing is that there seems to be an easy fix (see the bottom).

This is making more sense to me, and problems like this need to be
sorted out if local variable declarations are to be allowed as a part
of sequence and property expressions in the future (something that 
I would like to see).

J.H.

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


2007-07-10
----------

Here is an example to show how failing to uniquefy the local variable 
identifiers in the flattening could lead to trouble with the scoping
and my initial definition of the changes to the satisfaction relations.

Suppose we start with 

   sequence t;
      logic v;
      (1, v = c) ##1 v == d
      ;
   endsequence      


   sequence s;
      logic v; 
      (1, v=a) ##1 t ##1 v == b
      ;
   endsequence

   assert property (e |-> s);

Let's flatten without uniquefying the names.  We get

   assert property 
   (
      e
      |->
      (
         logic v;
         (1, v=a) 
         ##1 
         (
            logic v;
            (1, v = c) ##1 v == d
         )
         ##1 
         v == b
      )
   );

Let w be a finite natural word.  Let a,b,c,d be logic signals.  In the unclocked 
semantics, we get

   w,{},L |== (logic v; (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b)
   
   iff w,{},L |== (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b
   
   iff |w| > 0 and w^{1..},{(v,a[w^0])},L |== (logic v; (1, v = c) ##1 v == d) ##1 v == b
   
   iff |w| > 0 and there exists 1 <= i < |w| and L' s.t.
       w^{1,i-1},{(v,a[w^0])},L' |== (logic v; (1, v = c) ##1 v == d) and 
       w^{i..},L',L |== v == b
       
   iff [w^{i..},L',L |== v == b iff i = |w|-1 and L' = L and L(v) == b[w^{|w|-1}]]
       |w| >= 2 and 
       w^{1,|w|-2},{(v,a[w^0])},L |== (logic v; (1, v = c) ##1 v == d) and 
       L(v) == b[w^{|w|-1}]
   
   iff [use the "broken" rule w,L_0,L_1 |== (t v; R) iff w,L_0|_D,L_1 |== R,
       where D = dom(L_0) - {v}]
       |w| >= 2 and 
       w^{1,|w|-2},{},L |== (1, v = c) ##1 v == d and 
       L(v) == b[w^{|w|-1}]
   
   iff |w| = 4 and c[w^1] == d[w^2] and c[w^1] == b[w^3]

The semantics we want is 
  
   w,{},L |== (logic v; (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b)

   iff |w| = 4 and c[w^1] == d[w^2] and a[w^0] == b[w^3]


The rule

   w,L,L' |== (t v; R)  iff  w,L|_{dom(L) - {v}},L' |== R

is broken -- it needs to be changed to something like the following.

To simplify notation, let 

   L[v] = L|_{v}              // L on v
   L\v  = L|_{dom(L) - {v}}   // L off v

so that L = L[v] U L\v is a disjoint union.  Then

   w,L,L' |== (t v; R) 
   iff there exists L" s.t. w,L\v,L" |== R
       and L' = L"\v U L[v],