[sv-ac] recursive properties

Ed,

looking at the current restrictions, it seems that the relevant one is:

RESTRICTION 4: For every recursive instance of property q in the 
declaration of property p, each
actual argument expression e of the instance satisfies at least one of 
the following conditions:
— e is itself a formal argument of p.
— No formal argument of p appears in e.
— e is passed to a formal argument of q that is typed and the set of 
values for the type is bounded.

in this restriction I think that only

— e is passed to a formal argument of q that is typed and the set of 
values for the type is bounded.

may introduce a problem. One way to solve it is to remove this option 
having:

RESTRICTION 4: For every recursive instance of property q in the 
declaration of property p, each
actual argument expression e of the instance satisfies at least one of 
the following conditions:
— e is itself a formal argument of p.
— No formal argument of p appears in e.

Note, that we can still pass a design signal using one of the remaining 
options.

I think that argument that are typed with bounded type, should be 
allowed to be pass by value
(copied to the argument), but I don't think we have that way of passing 
argument in SVA properties.

This can be done using local variables, right?

something like

property p1(int i, j);
int i1;

(1,i1 = i) ##0
(j == 7) or
(
(i > 0) and
((a ##1 b) |-> p1(i1+2, j))
);
endproperty

Doron