Re: Group A - first draft LRM changes

Eratta
This should be:
sequence qAbort; @ (posedge clk) my_abort; endsequence
property p; @(posedge clk) disable iff (qAbort.triggered)
   a |=> ##[0:10] b;
endproperty

On Sun, 19 Dec 2004 09:24:28 -0800, ben cohen <hdlcohen@gmail.com> wrote:
> Erich, Cindy,
> What about doing something like what is done in SVA? Use a
> synchronous endpoint as the asynchronous abort condition?
> One note: We need to examine the timing, but I believe that the abort
> with a synchronous endpoint would occur delta time (or equivalent)
> after the clock edge.
> In SVA, a synchronous abort is done as follows:
> sequence qAbort; @ (posedge clk) my_abort; endsequence
> property p; @(posedge clk) disable iff (my_abort.triggered)
> a |=> ##[0:10] b;
> endproperty
> The "disable iff" is asynchronous, but the disabling condition is synchronous.
> The triggered method is used instead of the ended method because a
> triggered event state lasts throughout the time-time -- an SV timing
> thing.
>
> In PSL, the equivalent would then be:
> endpoint e_my_abort = {my_abort} @(posedge clk);
> property p= always ({a |=> [*0:10] b} @(posedge clk) abort e_my_abort);
>
> Bottom line, there is no need to introduce a a new synchronous abort operator.
> Ben Cohen
>
>
> On Sun, 19 Dec 2004 13:28:00 +0200, Cindy Eisner <EISNER@il.ibm.com> wrote:
> >
> >
> > erich,
> >
> > ok, you've done the research, so i can't argue with the history. perhaps
> > what i was remembering as the mandate to make aborts asynchronous came from
> > the alignment sub-committee. in any case, i completely agree with johan,
> > who said:
> >
> > >However, introduction of a abort_synch operator with synchronous
> > >semantics doesn't bring up either of problems 1, 2 or 3, so such a
> > >change would carry much less cost. Still we need to ask ourselves
> > >whether this is what we should put our scant first iteration resourses
> > >on.
> >
> > thus, i am for either leaving things as they are, or introducing a new
> > synchronous abort operator.
> >
> > regards,
> >
> > cindy.
> >
> > --------------------------------------------------------------------
> > Cindy Eisner
> > Formal Methods Group
> > IBM Haifa Research Laboratory
> > Haifa 31905, Israel
> > Tel: +972-4-8296-266
> > Fax: +972-4-8296-114
> > e-mail: eisner@il.ibm.com
> >
>
> --------------------------------------------------------------------------
> Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
> http://www.vhdlcohen.com/ ben@abv-sva.org
> * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
> * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd
> Edition, 2004, ISBN 0-9705394-6-0
> * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> 0-9705394-2-8
> * Component Design by Example ", 2001 isbn 0-9705394-0-1
> * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
> * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
> ---------------------------------------------------------------------------
>

--