Subject: Re: [sv-ac] semantics of match
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sat Mar 01 2003 - 17:31:09 PST
surrendra,
thanks. i think i understand now. so let's get back to joseph's proposal
for using match in order to define the semantics of multiple clocks. this
is what joseph suggested:
(a1; a2; a3) @clk_a => (b1; b2; b3) @clk_b (1)
(a1; a2; a3; matched ((b1; b2; b3) @clk_b) ) @clk_a (2)
i think that what he meant was that (2) be used for the semantics of (1).
if so, i see a couple of problems with this:
a. (2) is not an implication. therefore, it requires a1, a2, and a3,
whereas (1) requires nothing if a1, a2, and a3 don't hold on consecutive
ticks of clk_a.
b. "matched" doesn't seem to care where the sequence started. therefore,
we could conceivably have ticks of clk_a at times 100, 105, 110, at which
we see a1, a2, and a3, respectively. let there be an additional tick of
clk_a at time 120, and assume there are no other ticks of clk_a. now, if
we have ticks of clk_b at times 50, 55, and 115, at which b1, b2, and b3
hold, and no other ticks of clk_b, then it seems to me that (2) holds on
our path. have i got that right? here are my calculations:
pi, 120, clk_a, false, false |= matched({b1; b2; b3) @clk_b)
therefore,
(a1; a2; a3; pi[120]) @clk_a
holds on our path.
if i've got all that right (and even if i haven't), then i think i can see
the intention in all of this. it must be something like:
pi |= (seq_a @ clk_a) => (seq_b @ clk_b) <==>
for every j such that pi^{0,j} |== seq_a @ clk_a, there exists k such
that pi^{j+1,k) |== seq_b @clk_b
looking forward to your (and everyone else's) comments.
regards,
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 Dudani <Surrendra.Dudani@synopsys.com>@eda.org on 02/27/2003
06:27:35 PM
Sent by: owner-sv-ac@eda.org
To: sv-ac@eda.org
cc:
Subject: Re: [sv-ac] semantics of match
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 : Sun Mar 02 2003 - 00:32:42 PST