Subject: [sv-ac] revised regexp implications
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Sep 06 2002 - 08:01:14 PDT
Erich has pointed out to me that Sugar 2.0 has an "endpoint" construct
with which one can get the same effect as the OVA "matched" operator
(ignoring multiple clocking and synchronizing between clock domains).
Below, please find a revision of my previous mail that shows Sugar 2.0
renderings of the implications that I did not know how to write before.
Best regards,
John Havlicek
==========================================
Dear SV-AC:
Here are a few thoughts on implications between regular expressions. This is
not supposed to be an exhaustive list of possibilities.
All complications of multiple clocking, set, reset, etc. are being ignored here.
My understanding of Sugar 2.0 is based on the final Proposal to the Accellera FVTC.
My understanding of OVA/ForSpec 2.0 is based on the Technical Language Specification
document. I offer in advance my apologies for any mistakes regarding renderings in
Sugar 2.0 or OVA/ForSpec 2.0.
Let A be an alphabet. Let r be a regular expression over A and let L(r) be the
subset of A^* that is the language of r.
Let t be a trace (i.e., mathematical sequence) over A and let j <= k be indices of t.
Write t[j,k] to mean the restriction of t to the indices in [j,k]. Write
t,j,k |= r
to mean
t[j,k] \in L(r).
1. Promotion of a regular expression to a formula.
a. Forward looking: t,j |= forward(r) if there exists k >= j such that t,j,k |= r.
This is the semantics of "{true} |-> {r}!" in Sugar 2.0. (Sugar 2.0 Proposal,
pp. 61-62.)
This is the semantics of OVA/ForSpec 2.0 promotion of a regular event to
to a formula. (OVA/ForSpec 2.0 TLS, p. 14.)
b. Backward looking: t,j |= backward(r) if there exists i <= j such that t,i,j |= r.
This can be written in Sugar 2.0 as "end_r", where end_r has been defined via
endpoint end_r = {r};
This can be written as "matched(r)" in OVA/ForSpec 2.0.
2. Begin-begin implication.
t,i |= r bb_implies s if either there is no j >= i such that t,i,j |= r or
there exists k >= i such that t,i,k |= s. In terms of logical operators on
formulas, "r bb_implies s" is equivalent to "forward(r) implies forward(s)".
This can be written as
"({true} |-> {r}!) -> ({true} |-> {s}!)"
in Sugar 2.0.
This can be written as "r implies s" in OVA/ForSpec 2.0.
3. End-begin implication.
a. Unquantified: t,j |= r ueb_implies s if either there is no i <= j such
that t,i,j |= r or there exists k >= j such that t,j,k |= s. In terms
of operators on formulas, "r ueb_implies s" is equivalent to
"backward(r) implies forward(s)".
This can be written in Sugar 2.0 as "{end_r} |-> {s}!", where "end_r" is
defined as in 1.b.
This can be written in OVA/ForSpec 2.0 as "matched(r) implies s".
b. Quantified: t,i |= r qeb_implies s if, for all j >= i, either
t,i,j does not satisfy r or there exists k >= j such that t,j,k |= s.
This can be written as "{r} |-> {s}!" in Sugar 2.0.
This can be written as "r triggers s" in OVA/ForSpec 2.0.
Other end-begin implications are possible. For example:
c. t,i |= r ueb1_implies s if either there is no j >= i such that t,i,j |= r
or there exist k >= j >= i such that t,i,j |= r and t,j,k |= s.
This can be written as
"({true} |-> {r}!) -> ({true} |-> {r:s}!)"
in Sugar 2.0.
This can be written as "r implies (r #0 s)" in OVA/ForSpec 2.0.
4. Begin-end implication.
t,j |= r be_implies s if either there is no k >= j such that t,j,k |= r or
there exists i <= j such that t,i,j |= s.
This can be written in Sugar 2.0 as "({true} |-> {r}!) -> end_s", where
"end_s" is defined by
endpoint end_s = {s};
This can be written as "r implies matched(s)" in OVA/ForSpec 2.0.
5. End-end implication.
t,k |= r ee_implies s if either there is no i <= k such that t,i,k |= r or
there exists j <= k such that t,j,k |= s.
This can be written in Sugar 2.0 as "end_r -> end_s", where "end_r" and
"end_s" are defined as in 1.b and 4.
This can be written as "matched(r) implies matched(s)" in OVA/ForSpec 2.0.
Best regards,
John Havlicek
This archive was generated by hypermail 2b28 : Fri Sep 06 2002 - 08:03:35 PDT