Subject: RE: [sv-ac] nested implication example
From: Erich Marschner (erichm@cadence.com)
Date: Thu Feb 13 2003 - 13:57:22 PST
Adam, Surrendra,
Regarding
| (!e*[0:inf]; e) is equal to (first_match ([0:inf]; $rose(e)))
In PSL this is simply
e[->]
which is the degenerate case of
e[->n]
meaning "go to the nth ocurrence of e" (where the default value of n=1).
The DWG considered including this capability in SVA, but it was ultimately left out because this was not in OVA, and therefore not in the common subset. Perhaps that decision ought to be reconsidered, since the notion of 'next_event' as you defined it above is fairly common.
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: dudani@us04.synopsys.com [mailto:Surrendra.Dudani@synopsys.com]
| Sent: Thursday, February 13, 2003 3:52 PM
| To: sv-ac@eda.org
| Subject: Re: [sv-ac] nested implication example
|
|
| Hi Adam,
|
| 1) (!e*[0:inf]; e) // this creates one match and completes
| as soon as e is
| true
| 2) ([0:inf]; $rose(e)) // this creates a match for every
| $rose(e) in the future
|
| 2) is equivalent to 1) by the first_match transformation:
|
| (!e*[0:inf]; e) is equal to (first_match ([0:inf]; $rose(e)))
|
| Surrendra
| At 11:30 AM 2/13/2003 -0600, you wrote:
|
|
| >Good morning Surrendra, all;
| >
| >You wrote:
| >
| > >sequence next_event(e) = ((!e * [0:inf]) ; e);
| > >property p15 = ((write_valid ; true) =>
| > > ((int addr = addr_bus[0:7])
| > > (true ; next_event(write_valid))
| > > => (true;(addr !=
| addr_bus[0:7]))))
| >
| >Specifically the use of next_event()
| >
| >Is (!e*[0:inf; e) the same as
| >
| > ([0:inf]; $rose(e))
| >
| >
| >
| > Adam Krolnik
| > Verification Mgr.
| > LSI Logic Corp.
| > Plano TX. 75074
|
|
|
| **********************************************
| Surrendra A. Dudani
| Synopsys, Inc.
| 377 Simarano Drive
| Suite 300
| Marlboro, MA 01752
|
| Tel: 508-263-8072
| Fax: 508-263-8123
| email: dudani@synopsys.com
| **********************************************
|
|
This archive was generated by hypermail 2b28 : Thu Feb 13 2003 - 14:02:52 PST