Subject: [sv-ac] regexp implications
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Sep 05 2002 - 16:26:36 PDT
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.
I don't know how to write a Sugar 2.0 formula with this meaning.
This is the semantics of OVA/ForSpec 2.0 "matched(r)". (OVA/ForSpec 2.0 TLS,
p. 20.)
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)".
I don't know how to write a Sugar 2.0 formula with this meaning.
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.
I don't know how to write a Sugar 2.0 formula with this meaning.
This can be written as "r implies matched(s)" in OVA/ForSpec 2.0.
5. End-end imlplication.
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.
I don't know how to write a Sugar 2.0 formula with this meaning.
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 : Thu Sep 05 2002 - 16:31:11 PDT