Subject: RE: [sv-ac] Re: R58c - access to past values ... with enable
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Sep 26 2002 - 08:27:20 PDT
all,
so what is the bottom line? if i have followed the discussion correctly,
it seems that r58c can already be expressed as:
prev(expr, 1)@(posedge clk iff clk_en)
is this correct?
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
Simon Davidmann <simond@co-design.com>@eda.org on 25/09/2002 20:15:14
Sent by: owner-sv-ac@eda.org
To: Joseph Lu <Juin-Yeu.Lu@sun.com>
cc: sv-ac@eda.org
Subject: RE: [sv-ac] Re: R58c - access to past values ... with enable
Hi Joseph
At 06:12 PM 9/23/2002, Joseph Lu wrote:
>Hi Simon,
>
>Ok, to me "iff" based on SV3.0 manuali s a gardian expression for the
>event exp rather than
>a logical iff operators. Here is what i grasped from the SV3.0 manual.
>Usually "iff" is
>used as an if-and-only-if operator.
yes I know iff is normally used for if and only if - in
superlog/systemverilog we were looking for some of guard - and iff sort of
seemed to work - ie 'there is an event only if the expression is true'
people seem to think it works well.
Simon
> The event expression only triggers if the expression after the iff is
> true, in this case when
> enable is equal to 1. Note that such an expression is evaluated when clk
> changes, and not when
> enable changes.
>
>--Joseph
>
>
> >X-Sender: his-home@pop3.demon.co.uk
> >Date: Mon, 23 Sep 2002 15:57:26 -0700
> >To: Joseph Lu <Juin-Yeu.Lu@Sun.COM>, fitz@co-design.com,
bassam@novas.com
> >From: Simon Davidmann <simond@co-design.com>
> >Subject: RE: [sv-ac] Re: R58c - access to past values ... with enable
> >Cc: sv-ac@eda.org
> >Mime-Version: 1.0
> >X-OriginalArrivalTime: 23 Sep 2002 22:58:24.0244 (UTC)
> FILETIME=[B86E6340:01C26354]
> >
> >Joseph - actually that is not what the SystemVerilog 'iff' means. I
cannot
> >recall the full definition - but it is in the SystemVerilog3.0 manual.
> >
> >Simon
> >
> >At 03:44 PM 9/23/2002, Joseph Lu wrote:
> >
> >>Hi Tom,
> >>
> >>Since "A iff B" is interpreted as "A imply B AND B imply A",
> >>there are two scenarios by which the even expression holds. That is:
> >>
> >> 1) posedge clk -- True
> >> clk_en -- True
> >>
> >> 2) posedge clk -- False
> >> clk_en -- False
> >>
> >>It does not quite serve the original purpose.
> >>
> >>
> >>Regards,
> >>
> >>--Joseph
> >>
> >>
> >>
> >> >From: "Tom Fitzpatrick" <fitz@co-design.com>
> >> >To: "Joseph Lu" <Juin-Yeu.Lu@sun.com>, "Bassam Tabbara"
> <bassam@novas.com>
> >> >Cc: <sv-ac@eda.org>
> >> >Subject: RE: [sv-ac] Re: R58c - access to past values ... with enable
> >> >Date: Mon, 23 Sep 2002 16:40:39 -0400
> >> >MIME-Version: 1.0
> >> >Content-Transfer-Encoding: 7bit
> >> >X-Priority: 3 (Normal)
> >> >X-MSMail-Priority: Normal
> >> >X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2600.0000
> >> >Importance: Normal
> >> >
> >> >Hi Joseph,
> >> >
> >> >Actually, SystemVerilog defines the 'iff' event operator, so your
example
> >> >could be written in SystemVerilog as
> >> >
> >> >prev(expr, 1)@(posedge clk iff clk_en)
> >> >
> >> >By extension from SystemVerilog, this would only count posedge clk
> events at
> >> >which clk_en was also true.
> >> >
> >> >-Tom
> >> >
> >> >
> >> >> -----Original Message-----
> >> >> From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org]On
> >> >> Behalf Of Joseph Lu
> >> >> Sent: Friday, September 20, 2002 2:33 PM
> >> >> To: Bassam Tabbara
> >> >> Cc: sv-ac@server.eda.org
> >> >> Subject: Re: [sv-ac] Re: R58c - access to past values ... with
enable
> >> >>
> >> >>
> >> >>
> >> >> So, what is your semantics of evaluating this event expression?
> >> >>
> >> >> prev(expr, 1)@(posedge (clk) && clk_en)
> >> >>
> >> >> --Joseph
> >> >>
> >> >>
> >> >> >Date: Fri, 20 Sep 2002 11:26:02 -0700 (PDT)
> >> >> >From: Joseph Lu <Juin-Yeu.Lu@sun.com>
> >> >> >Subject: Re: [sv-ac] Re: R58c - access to past values ... with
enable
> >> >> >To: Juin-Yeu.Lu@sun.com
> >> >> >MIME-Version: 1.0
> >> >> >Content-MD5: iPNL0SFhlcoW2dP/5DtlYA==
> >> >> >
> >> >> >Who's talking about Verilog ? prev ??? Yes as I said this is an
> >> >> event expression so in a pseudo
> >> >> >assertion description
> >> >> >sync the_clk: posedge(clk) && clk_en
> >> >> >
> >> >> >prev(expr, 1)@@(the_clk) in some way/shape or form
(DAS/OVA/PSL...)
> >> >> >
> >> >> >-Bassam.
> >> >> >
> >> >> >Joseph Lu wrote:
> >> >> >
> >> >> > >Date: Thu, 19 Sep 2002 15:08:27 -0700
> >> >> > >From: Bassam Tabbara <bassam@novas.com>
> >> >> > >X-Accept-Language: en
> >> >> > >MIME-Version: 1.0
> >> >> > >To: Adam Krolnik <krolnik@lsil.com>
> >> >> > >CC: Cindy Eisner <EISNER@il.ibm.com>, sv-ac@eda.org
> >> >> > >Subject: [sv-ac] Re: R58c - access to past values ... with
enable
> >> >> > >Content-Transfer-Encoding: 7bit
> >> >> > >X-OriginalArrivalTime: 19 Sep 2002 22:08:27.0227 (UTC)
> >> >> FILETIME=[146AE2B0:01C26029]
> >> >> > >
> >> >> >
> >> >> > >Adam,
> >> >> > >
> >> >> > >Thx for the example, 2 things.
> >> >> > >
> >> >> > >1) I think you are making a statement about -sampling-, so as
> >> >> I said earlier, I do not see
> >> >> why
> >> >> >this is limited
> >> >> > >to "prev", you are giving one example using that construct, if
> >> >> > >there is an enhancement to sampling I'm sure there are other
> >> >> examples of this symptom.
> >> >> > >2) In the example, I'm afraid I don't see why doing:
> >> >> > >
> >> >> > >.... prev(expr, 1)@(posedge (clk) && clk_en) does not do what
> >> >> you want to do for:
> >> >> >
> >> >> > I am wondering if Verilog allow you to do @(posedge (clk) &&
> >> >> clk_en). It is an event
> >> >> >expression.
> >> >> > The only operator to compose two event expressions is or.
> >> >> >
> >> >> > --Joseph
> >> >> >
> >> >> > >
> >> >> > >always @(posedge clk) (2)
> >> >> > > if (clk_en) p_expr <= expr;
> >> >> >>Date: Fri, 20 Sep 2002 11:20:19 -0700
> >> >> >>From: Bassam Tabbara <bassam@novas.com>
> >> >> >>X-Accept-Language: en
> >> >> >>MIME-Version: 1.0
> >> >> >>To: Joseph Lu <Juin-Yeu.Lu@sun.com>
> >> >> >>CC: sv-ac@eda.org
> >> >> >>Subject: Re: [sv-ac] Re: R58c - access to past values ... with
enable
> >> >> >>Content-Transfer-Encoding: 7bit
> >> >> >>X-OriginalArrivalTime: 20 Sep 2002 18:20:19.0557 (UTC)
> >> >> FILETIME=[6057F150:01C260D2]
> >> >> >>
> >> >> >
> >> >>
> >> >> --------------------------------------------------
> >> >> Joseph Lu, Ph.D
> >> >> Global Validation, Processor Product Group
> >> >> Sun Microsystems
> >> >> M/S USUN 03-202, 430 N. Mary Ave.,
> >> >> Sunnyvale, CA 94086
> >> >> 408-616-5887
> >> >> joseph@eng.sun.com
> >> >> --------------------------------------------------
> >> >>
> >> >>
> >> >
> >
This archive was generated by hypermail 2b28 : Thu Sep 26 2002 - 08:26:47 PDT