RE: [sv-ac] 1420

Hi Doron,

This proposal looks good. One thing which is still an issue is what
happens when all the arguments are same as formal arguments but the
order has changed. Is that legal ? If yes, how do we interpret it. Here
is an example:

property P(a, b)

(a ##1 b) and (1 |=> P(b, a));

endproperty 

Note that argument order has changed in this case. Now it can be
interpretted in two ways:
1. After each recursion, a and b get switched.
2. After first recursion, a and b get switched but after that they
remain the same.

I would prefer if we make it illegal to switch the formal argument order
also.

Thanks.
Manisha

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Doron Bustan
Sent: Monday, August 21, 2006 3:05 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] 1420

All,

we modified the 1420 proposal to deal with the example presented at
17.11.4

I upload it to mantis and also attached it.

Doron