Subject: RE: [sv-ac] regexp implications
From: Erich Marschner (erichm@cadence.com)
Date: Thu Sep 12 2002 - 06:07:16 PDT
Ambar,
Your note below was a reply to, and includes, John's original email message, which was missing some information about how Sugar supports these capabilities. I would like to point out that John's later message demonstrated that Sugar supports all of the four combinations that he outlined.
I've included John's later message below for reference.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Ambar Sarkar [mailto:ambar.sarkar@paradigm-works.com]
| Sent: Thursday, September 12, 2002 7:56 AM
| To: john.havlicek@motorola.com; sv-ac@eda.org
| Subject: Re: [sv-ac] regexp implications
|
|
| 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 [mailto:john.havlicek@motorola.com]
| Sent: Friday, September 06, 2002 11:01 AM
| To: sv-ac@eda.org
| Cc: john.havlicek@mot.com
| Subject: [sv-ac] revised regexp implications
|
|
| 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
|
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
This archive was generated by hypermail 2b28 : Thu Sep 12 2002 - 06:08:12 PDT