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

John,

I am in favour of this proposal if it is updated to handle the sampling
issue.

I am in favour of sampling the declaration assignments using the
previous clocks, it does not make sense to syntactically look forward to
know the clock.

I never knew the non-overlapping implication rewrite rule put the clock
in "no mans land".  Can this be changed to keep the clock as ev0? What
was the reasoning with the "no mans land" sampling clock change?

"and the rewrite for "|=>" would give

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

Thanks

Hillel Miller>


-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Friday, March 02, 2007 7:36 PM
To: dmitry.korchemny@intel.com
Cc: Havlicek John-r8aaau; sv-ac@eda-stds.org
Subject: 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.


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