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 Thu Dec 2 12:27:19 2004