[sv-ac] ideas for semantics for 1668

All:

We have not been making progress with 1668 because
I have not provided any proposed solution to the 
problems with the semantics of local variable declaration
assignments in the presence of multiple clocks.

I think I have known for a while what the semantics 
should be, but I have struggled with writing it in 
a reasonably simple way.

I think I have found a resonable way to do it.  Below 
are some notes.

I would like to get feedback so that we can converge on
the technical solution before revising the proposal for
another vote.

Best regards,

John H.

-------------------------------
2007-05-28

Let E be the list of local variable declaration assignments.  There
still seems to be disagreement on whether the declaration order should
be used to determine the order of the assignments in E.  I think it 
should.

For a declared sequence with local variable declaration assignments, 
no elaborated sequence instance can admit empty match of the body 
sequence expression.  The current multi-clock rules require the 
sequence expression to have a unique semantic leading clock.  

Let r be an instance of the declared seqeunce.  If the semantic leading 
clock of r is inherited, then the semantics of the instance with 
declaration assignments is that of

  (1,E) ##0 r

Otherwise, the semantics of the instance with declaration assignments
is 

  @(semantic_leading_clok(r)) (1,E) ##0 r


For a declared property with local variable declaration assignments,
we give an inductive definition of prepend(E,p).  The idea is to use
the sequence definition as a base and to descend into the various
subproperties with distinct semantic leading clocks to ensure that the
declaration assignment is aligned with the semantic leading clock of
the subproperty.

r denotes a sequence expression.  p, q denote property expressions.

BASIS:

. Let p be equal to the sequential expression r.  According to the
  multi-clock rules, r has a unique semantic leading clock.  

  If semantic_leading_clock(r) = inherited, then

     prepend(E, p) = (1,E) ##0 r

  Otherwise

     prepend(E, p) = @(semantic_leading_clock(r))(1,E) ##0 r

INDUCTIVE CASES:

. prepend(E, ( p )) = ( prepend(E, p) )

. prepend(E, not p) = not prepend(E, p)

. prepend(E, p or q) = prepend(E, p) or prepend(E, q)

. prepend(E, p and q) = prepend(E, p) and prepend(E, q)

. If semantic_leading_clock(r) = inherited, then

     prepend(E, r |-> p) = (1,E) ##0 r |-> p

  Otherwise

     prepend(E, r |-> p) = @(semantic_leading_clock(r))(1,E) ##0 r |-> p

. If semantic_leading_clock(r) = inherited, then

     prepend(E, r |=> p) = (1,E) ##0 r |=> p

  Otherwise

     prepend(E, r |=> p) = @(semantic_leading_clock(r))(1,E) ##0 r |=> p

. prepend(E, if (b) p [ else q ]) = (1,E) |-> if (b) p [ else q ]

. prepend(E, <property instance>) results by first flattening the property
  instance (see formal semantics of arguments) and then proceeding with this
  definition.

. prepend(E, @c p) = @c prepend(E, p)


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