[sv-ac] OOPS

From: Doron Bustan <dbustan_at_.....>
Date: Wed Jun 28 2006 - 11:35:14 PDT
Somewhere in the transition from 3.1a to ieee2005
the semantics of the recursive properties was lost. We need to add it again.

the proposal is 1518

the missing text at the end of appendix E.5 is :


Let p(X) be an instance of a recursive named property p, where X denotes 
the actual arguments of the instance.
For k > 0, the k-fold approximation to p(X), denoted p[k](X), is an 
instance of a non-recursive property p[k]
defined inductively as follows.
— The declaration of p[0] is obtained from the declaration of p by 
replacing the body property_expr with the
literal 1’b1.
— For k > 0, the declaration of p[k] is obtained from the declaration of 
p by replacing each instance of a recursive
property by its (k – 1)-fold approximation.
The semantics of the instance p(X) is then defined as follows. For any 
word w over \Sigma and local variable context
L, w, L |= p(X) iff for all k > 0, w,L |= p[k](X).


Doron
Received on Wed Jun 28 11:35:26 2006

This archive was generated by hypermail 2.1.8 : Wed Jun 28 2006 - 11:35:47 PDT