Subject: Re: [sv-ac] regexp implications
From: Ambar Sarkar (ambar.sarkar@paradigm-works.com)
Date: Thu Sep 12 2002 - 04:56:25 PDT
All,
My action item was to specify various implication scenarios. However, John
did such a wonderful job of laying out various implication scenarios that I
don't think I can add much to it.
I was primarily thinking of *implies*in terms of begin-begin implication.
Requirements-wise, as long as the LRM provides convenient ways to specify
following expressions:
a. forward-looking promotion
b. backward-looking promotion
c. begin-begin implication (implies ?)
d. trigger implication (as in OVA triggers ?)
we should be able to express all the combinations described below. I am not
too worried about the exact form used in a to d.
My 2 cents.
Regards,
-Ambar
----- Original Message -----
From: "John Havlicek" <john.havlicek@motorola.com>
To: <sv-ac@eda.org>
Cc: <john.havlicek@mot.com>
Sent: Thursday, September 05, 2002 7:26 PM
Subject: [sv-ac] regexp implications
> 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 12 2002 - 04:57:40 PDT