Subject: RE: Comparison of ForSpec's 2.0 && to Sugar's &&
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Nov 19 2001 - 03:49:28 PST
Hi Bernard,
Satisfaction happens at the beginning (point i below).
The end point of the tight satisfaction is the longest WORD.
And yes, in the example below is when the word taken from e1 finishes.
Regards,
Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Sunday, November 18, 2001 11:15 PM
To: Armoni, Roy
Cc: vfv@eda.org
Subject: Re: Comparison of ForSpec's 2.0 && to Sugar's &&
Roy,
When is the combination satisfied if you AND temporal expressions of
different lengths under the scheme you describe? Is this when *all*
expressions are satisfied, that is to say when the longest expression is
satisfied? In your example should we assume "e1 && e2" is satisfied when
e1 is satisfied?
Thanks
Bernard
At 06:29 PM 11/18/2001 +0200, Armoni, Roy wrote:
>This note is in response to Erich's request from me to clarify the
>difference between the && operator proposed in ForSpec 2.0 to that of
Sugar.
>
>In ForSpec 2.0, we propose to have the && similar to the Boolean
connective.
>That is,
>pi,i,c |= e1 && e2
>iff
>pi,i,c |= e1 and pi,i,c |= e2
>iff
>There exists w1 in L(e1) and w2 in L(e2) s.t. for some j1,j2 >= i, we have
>that pi,i,j1,c |== w1 and pi,i,j2,c |== w2.
>
>That means that w1 and w2 are not necessarily of the same length. Their
>respective end points j1 and j2 may be different. In Sugar, the
requirement
>is that j1 and j2 will be the same, thus, w1 and w2 must be of the same
>length.
>
>Consider for instance the REs
>e1 := req, !gnt*, gnt;
>e2 := !rst;
>
>and a trace with the following wave form:
>req: 1 0 0 ...
>gnt: 0 0 1 ...
>rst: 0 0 0 ...
>
>e1 is satisfied by this trace because it contains the word "req,!gnt,gnt".
>e2 is satisfied by this trace because it contains the word "!rst".
>In ForSpec 2.0, also "e1 && e2" will be satisfied.
>
>In Sugar, "e1 && e2" will not be satisfied, however, "e1 && (e2,true*)"
will
>(because e2 can be extended by "true,true" to length 3).
>
>As I said in the meeting, Intel is willing to add the sugar&& operator to
>ForSpec 2.0 as well if required by the committee.
>
>Regards,
> Roy
====================================================================
SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
431-5126
Email: bdeadman@sdvinc.com Website: www.sdvinc.com
This archive was generated by hypermail 2b28 : Mon Nov 19 2001 - 03:53:35 PST