Re: Group A - first draft LRM changes

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
---------------------------------------------------------------------------
Received on Sun Dec 19 09:24:33 2004