Subject: RE: [sv-ac] semantics of match
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Feb 27 2003 - 06:47:19 PST
Hi Cindy,
I believe that the key issue here is synchronization between two clocks.
Note that "matched" in OVA 2.0 is a template that is defined by means of the
"ended" operator. Looking at the syntax definition of ended, we see that e
may be a clocked regular expression. So let's look at the following
example:
clock c1 {
event e : ... ;
}
clock c {
formula f: ... matched(e) ... ;
}
In this example, matched is being evaluated in the context of the clock c.
However, e changes clock to c1. Thus, in most cases, e will indeed end in a
tick point of c1, which is not necessarily a tick point of c. In the
definition on page 20, l ranges over all trace points that exist on and
after the end point of e on c1 until before the evaluation point of
matched(e) and makes sure that there are no additional tick points in this
range. Does it make any sense?
Regards,
Roy
-----Original Message-----
From: Cindy Eisner [mailto:EISNER@il.ibm.com]
Sent: Wednesday, February 26, 2003 4:14 PM
To: sv-ac@eda.org
Subject: [sv-ac] semantics of match
roy, surrendra,
i am trying to understand the semantics of match as presented on page 20 of
the ova document. let's assume for the moment that a and r are both false.
then we get that
pi, j, c, false, false |= matched (e) if the following two hold:
- pi, j |= c
- there exists i <= k < j s.t. pi,i,k,c \modelstightly e and for all l, k
<= l < j, pi, l |= !c
i don't understand the "<=" in "k <= l < j". i think that if
pi,i,k,c \modelstightly e
then according to page 14, c holds at pi^k. is that correct? if so, then
how can it ever be that "for all l, k <= l < j, pi, l |= !c"? shouldn't it
be "k < l < j" instead?
thanks,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Thu Feb 27 2003 - 06:54:47 PST