Re: [sv-ac] call to vote on 1668

Hi Dmitry:

> Therefore a property cannot be satisfied by an empty word. So, what kind
> of definition extension of satisfiability relation on empty words do you
> expect?=20

See, e.g., "A Topological Characterization of Weakness", by C. Eisner, 
D. Fisman, and J. Havlicek in the proceedings of PODC 2005.

> We could have only one rewrite rule, say the one with "|->", but=20
> in that case I would like to leave a reminder that this will become
> broken if we extend the semantics to define property satisfaction on
> the empty word.
> 
> [Korchemny, Dmitry] In your original proposal you reserved "|->" for
> properties satisfied by the empty word. Could you, please, elaborate?

I meant in the sense of an extended semantics like that referenced
above, although on further thought the problem involves more than just
the empty word in the presence of clocks.  See below.

> 
> Would this satisfy you?
> 
> [Korchemny, Dmitry] I don't think we should mention in the LRM that the
> definition will change when the semantics changes.

I didn't intend necessarily to make a negative statement about something
breaking.  This could be done by noting the assumption on which the 
device is predicated.

> I don't think "disable iff" should be considered in these
> restrictions.  We have changed our language concerning "disable iff"
> to say that an attempt that is terminated by the "disable iff"
> condition is called "disabled", not "passing" or "failing".  According
> to the Draft 1 revisions to Annex E, the "disable iff" condition is
> relevant to the disposition of one of the satisfaction relations only
> in the case of a non-empty word.  (Technically, we are only talking
> about non-empty words in that context, as I pointed out above, but I
> mean if you read the conditions imagining the possibility that the
> word be empty.)
> 
> Do you agree?  Does this satisfy you?
> 
> [Korchemny, Dmitry] If accepton operator is introduced then all these
> issues (if they exist) become relevant again. I think that the
> definition should be robust relative to such changes.


I have thought carefully about your comments involving the 
two forms of rewrite for properties with local variables with 
declaration assignments and your concern about how the semantics
of the declaration assignments will interact with nestable 
accept_on/reject_on operators.

I think there is a problem with my proposal that needs to be addressed
and is substantial enough to abort the current ballot, so I suggest
that you go ahead and vote no based on your concerns.  You can also
point to the discussion in this mail.  Others should feel free, of
course, to continue commenting on the current proposal.

The problem involves the interaction of clocking and clock changes
with the local variable declaration assignments.  This problem may
have been raised by others in the past and subsequently forgotten 
by me.  To illustrate, consider this example:

   property foo;
      logic v = e;
      @(ev1) q1
      and
      @(ev2) q2
      ;
   endproperty

   a:  assert property (@(ev0) r |=> foo);

For simplicity, let's assume that no clocking event appears in
the property expressions q1,q2 or the sequence expression r.

Assuming that we use the "|->" rewrite rule, we would get

   @(ev0) r |=> ((1,v=e) |-> (@(ev1) q1 and @(ev2) q2))

and the rewrite for "|=>" would give

   @(ev0) r ##1 (@(1)1) |-> ((1,v=e) |-> (@(ev1) q1 and @(ev2) q2))

This leaves some doubt as to when the (1,v=e) should actually 
occur -- is is sort of floating in "no man's land" between the 
old clock @(ev0) and the two new clocks @(ev1) and @(ev2).

For continuity reasons with the singly clock case, it seems to me
that we need to push the (1,v=e) to occur on the new clocks.  
Sampling the "e" expression in "no man's land", e.g. with the @(1)1,
seems like a bad idea and it is semantically discontinuous when 
we let ev0, ev1, and ev2 become the same.

In order to solve this problem, we need a more elaborate description
of how to attach the declaration assignments to the various beginnings
of a property.

I am hopeful that this can be done in a way that will also put the 
declaration assignments underneath the scopes of any relevant 
accept_on/reject_on operators.

But the solution will require some discussion, an update of the proposal,
and a new vote.

Best regards,

John H.

> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,239,1170662400"; 
>    d="scan'208"; a="52297993:sNHT27284805"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Fri, 2 Mar 2007 05:07:28 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on 1668
> Thread-Index: AcdcAniN/QIiuaCJSdOZhk6iSDH6BwAcUMzQ
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 02 Mar 2007 03:07:32.0686 (UTC) FILETIME=[EB989EE0:01C75C77]
> 
> Hi John,
> 
> Please, see my comments below.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Thursday, March 01, 2007 3:07 PM
> To: Korchemny, Dmitry
> Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
> Subject: Re: [sv-ac] call to vote on 1668
> 
> Hi Dmitry:
> 
> I don't really see this as an inconsistency.  Sequences and properties
> are different kinds of things, and we have different satisfaction
> relations for the two.
> 
> In fact, our neutral satisfaction relation for properties is not
> currently defined on empty words.  The definition can be extended to
> include empty words, and I expect it eventually will be.  It was with
> that vision that I thought we ought to have the two cases for
> rewriting the semantics of a property with local variables with
> declaration assignments.
> 
> [Korchemny, Dmitry] Yes, indeed, I noticed that
> 
> w |=3D R iff there exists 0 <=3D j < |w| so that w^{0, j} \tight R,
> therefore if sequence can be satisfied by an empty word, the
> property-sequence cannot (though I don't know why).
> 
> Also,
> w |=3D disable iff (b) P iff either w |=3D P or there exists 0 < k < |w| =
> so
> that w^k |=3D b and w^{0, k-1} \top ^ \omega |=3D P. Here, w^{0, -1} =
> denotes
> the empty word.=20
> 
> Therefore a property cannot be satisfied by an empty word. So, what kind
> of definition extension of satisfiability relation on empty words do you
> expect?=20
> 
> My intention has been to place as few restrictions as possible, but
> when we don't have a good solution I prefer to make things illegal
> and leave the possibility of relaxing the restriction later if we
> can come up with a good definition.
> 
> So I am willing to modify the proposal to say that local variable
> declaration assignments are illegal in the declaration of a named
> property whose body property expression is a sequence expression that=20
> admits an empty match.
> 
> Would this satisfy you?
> 
> [Korchemny, Dmitry] Yes, I agree with this approach.
> 
> We could have only one rewrite rule, say the one with "|->", but=20
> in that case I would like to leave a reminder that this will become
> broken if we extend the semantics to define property satisfaction on
> the empty word.
> 
> [Korchemny, Dmitry] In your original proposal you reserved "|->" for
> properties satisfied by the empty word. Could you, please, elaborate?
> 
> Would this satisfy you?
> 
> [Korchemny, Dmitry] I don't think we should mention in the LRM that the
> definition will change when the semantics changes.
> 
> I don't think "disable iff" should be considered in these
> restrictions.  We have changed our language concerning "disable iff"
> to say that an attempt that is terminated by the "disable iff"
> condition is called "disabled", not "passing" or "failing".  According
> to the Draft 1 revisions to Annex E, the "disable iff" condition is
> relevant to the disposition of one of the satisfaction relations only
> in the case of a non-empty word.  (Technically, we are only talking
> about non-empty words in that context, as I pointed out above, but I
> mean if you read the conditions imagining the possibility that the
> word be empty.)
> 
> Do you agree?  Does this satisfy you?
> 
> [Korchemny, Dmitry] If accepton operator is introduced then all these
> issues (if they exist) become relevant again. I think that the
> definition should be robust relative to such changes.
> 
> Best regards,
> 
> John H.
> 
> 

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