Subject: Re: [sv-ac] nested implication example
From: dudani@us04.synopsys.com
Date: Thu Feb 13 2003 - 12:52:14 PST
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 - 12:56:05 PST