In reply to dave_59:
thanks Dave.
I’m running the assertions with a formal tool, the first iteration passes (in your example: p(0)) , all other iterations keep the `PATH(0), but change the index in the antecedent (and so assertions fail).
my environment is very similar to your example, except I have a seperate SVA file bind to the ‘top’.
do think that may cause the problem?