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). DoronReceived 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