Subject: Comparison of ForSpec's 2.0 && to Sugar's &&
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sun Nov 18 2001 - 08:29:43 PST
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
This archive was generated by hypermail 2b28 : Sun Nov 18 2001 - 08:35:56 PST