Subject: Re: [sv-ac] semantics of match
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Thu Feb 27 2003 - 08:27:35 PST
Hi Cindy and All,
The document that Steve sent with regards to matched definition was revised
(after it was written) to take care of the synthesis issues. The new
definition introduced 1 cycle delay when the match occurs and the two clock
edges happen to coincide. Otherwise, there is no change. Please see below
the revised definition:
Template form:
matched (e): ended(ended(e) #1 any);
Explicit definition:
pi,j,c,a,r |= matched(e) if either
pi ,j,c |= a, or
the following 3 hold:
pi,j,c |= !r, and
pi,j |= c, and
there exists i<=k < j, s.t, pi,i,k,c |== e and
for all l, k< l < j, pi,l = !c
The following changes were made in the explicit definition:
1) k always less than j, to eliminate the case of a match at the time when
the two clocks are aligned
2) l is between k and j, to consider the case when the two clock ticks are
aligned, but the match is delayed by one clock
Surrendra
At 04:13 PM 2/26/2003 +0200, you wrote:
>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
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Thu Feb 27 2003 - 08:29:21 PST