RE: [sv-ac] 1668 update

Hi John,



I think that you should be able to prove the expected semantics
of your property using the new flow rules.  I don't think it
is a matter of hinting.

[DB} I don't see how. The flow rules are use to determine the domain of
the context not the values of the local variables. So I agree that the
property is legal, but I am not sure what its semantics is.

You should also consider this example, which is legal today:

sequence r;
logic v;
(1, v = 1) ##1 (v == 1);
endsequence

property p;
logic v;
(1,v = 0) ##1 r ##1 (v ==0);
Endproperty

[DB] The rewrite algorithm makes the names unique, so again it is only a
hint. 

Doron

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.