Subject: [sv-ac] alternative proposal to "syn1": remove binary delay
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 09 2003 - 04:06:19 PST
all,
here is an alternative proposal to "syn1", based upon an idea of john
havlicek's that was proposed offline. like "syn1", it involves removing
one kind of delay. but it chooses to remove the binary delay, rather than
the unary delay.
it is equivalent to "syn1" when a delay is used after a semi-colon, as in
"a ; [3] b", but is different than "syn1" in that it allows a leading [n]
as well. for example, in this proposal, "[3] a" is a legal sequence,
whereas "[3] a" is not legal under "syn1". i have taken the liberty of
changing the name from "unary delay" to "unary start-at", since the use of
a leading [n] in this proposal no longer gives the meaning of a delay of
"n" cycles, but rather has the inuitive meaning of "start at the nth
cycle".
the proposal assumes that we have two kinds of concatenation defined:
BINARY CONCATENATION: "r;s" is defined to mean an occurence of "r"
followed by an occurence of "s" such that the first cycle of "s" happens
the cycle after the last cycle of "r".
BINARY OVERLAPPING CONCATENATION (FUSION): "r;[0]s" is defined to mean
an occurence of "r" followed by an occurence of "s" such that there is
an overlap of one cycle between "r" and "s". that is, such that the
first cycle of "s" happens the same cycle as the last cycle of "r".
we now define the "unary start-at" operator as follows:
informally:
UNARY START-AT: "[n] r" means that r starts on the n'th cycle. thus
"[1] r" is equivalent to "r", "[2] r" is equivalent to "1;r", etc.
semi-formally:
UNARY START-AT: If n > 0, then "[n]r" is defined and it means the same
thing as "1*[n] ;[0] r".
examples:
[1] a means a
[2] a means 1;a
[3] a means 1;1;a
a ;[1] b means a ; b
a ;[2] b means a; 1; b
a ;[3] b means a; 1; 1; b
a ; ([1] b) means the same as a ;[1] b
a ; ([2] b) means the same as a ;[2] b
a ; ([3] b) means the same as a ;[3] b
the second three examples show that the definition of "unary start-at"
gives the same meaning to "a ; [n] b" as did the definition of "binary
delay" in revision 0.79. the advantage of the current proposal over "syn1"
is that in addition, it allows a "leading delay" as in the first three
examples. finally, the advantage of the current proposal over revision
0.79 is that the definition of "unary start-at" does not put undue semantic
responsibility on the parentheses, as shown by the last three examples.
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
This archive was generated by hypermail 2b28 : Sun Feb 09 2003 - 04:03:13 PST