RE: Example application of a "forall"

Yes, using an endpoint is a way to do that.
Thanks,
Andrew

________________________________

From: Erich Marschner [mailto:erichm@cadence.com]
Sent: Thursday, December 02, 2004 12:27 PM
To: Seawright, Andrew
Cc: ieee-1850-extensions@eda.org
Subject: RE: Example application of a "forall"

Andrew,
 
Perhaps your example application could be addressed with an endpoint -
e.g.,
 
  endpoint recent (boolean B, const N,M) = {{b within [*M]}; [*N-M]};
  property p = always (a -> recent(b,N,M));
 
where N=number of cycles back to the start of the window, and M=width of
the window in cycles, as in your example.
 
I realize this approach might not work for everything, but it seems to
me that an endpoint might be useful any time you are reasoning about
past behavior.
 
Regards,
 
Erich
 
 

________________________________

        From: owner-ieee-1850-extensions@eda.org
[mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Seawright,
Andrew
        Sent: Wednesday, November 24, 2004 11:51 AM
        To: ieee-1850-extensions@eda.org
        Subject: Example application of a "forall"
        
        
        This is an example application of a forall extension that I ran
across:
         
        property p = always(a -> (prev(b,N) ||
           prev(b,N+1) ||
           prev(b, N+2) ||
             ...
           prev(b, M)));
         
        The user would like to use a forall construct and, make this
into
        a parameterized property and pass in N, M etc.
         
        (I mentioned this example in the extensions meeting yesterday)
Received on Fri Dec 3 16:09:44 2004